%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% This is the README file for the automated LCC-MCID model checker
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Written by Nardine on 04/09/2007 - modified on 17/09/2007
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Document Outline:
    - Overview
    - Installing LCC-MCID
    - Files and Folders
    - Using the LCC-MCID System
    - Copyright Notice



Overview
========

The LCC-MCID system is a logic based automated model checking system
for distributed open systems.  It allows agents with predefined goals
to automatically search for appropriate interaction models, verify
that the selected interaction models do not violate the agent's
predefined deontic (and possibly) temporal constraints, and eventually
run the selected interaction model.  This entire process may be fully
automated.  However, the model checker may also be manually invoked
when needed.

We note that in this beta version, the LCC engine, which originally
ran over SICStus, still does so.  However, the MCID model checker is
built upon XSB tabled Prolog.  Therefore, LCC-MCID currently requires
both SICStus and XSB to be installed.  We plan to address this issue
in later versions.



Installing LCC-MCID:
====================

1- Install XSB:
   The MCID model checker is built on XSB tabled Prolog.  Therefore,
   to be able to run MCID, XSB should first be installed.  XSB is
   available for free from http://xsb.sourceforge.net/

2- After installing XSB, download the LCC-MCID tarball from
   http://homepages.inf.ed.ac.uk/s0233771/mcid and unpack it:
      $ tar zxvf lcc_mcid.tar.gz

3- Go to the newly created 'lcc_mcid/' directory:
      $ cd lcc_mcid

4- Run the installation script:
      $ ./install.sh
   During installation, you will be asked to provide the full path
   name of the XSB executable (Example: /usr/local/bin/xsb). So make
   sure you have installed XSB first.



Files and Folders:
==================

The 'lcc_mcid' directory contains 2 files:
    - 'install.sh':	    the shell script for installing the
			    LCC-MCID system
    - 'readme.txt':         this file	    

and 5 directories:
    - 'agents':		    contains all the agents files, i.e. their
			    knowledge base and deontic and temporal
			    properties
    - 'interaction_models': contains all interaction models in
			    addition to the 'im.db' file, which
			    provides a summary of available
			    interaction models
    - 'lcc_engine':	    contains the LCC engine, required for
			    agents to execute LCC interactions
    - 'mcid':		    contains the model checker, required for
			    verifying whether deontic and temporal
			    rules hold in a given interaction model
    - 'xamples':	    contains some examples with results



Using the LCC-MCID System:
==========================

1- After installation, go to the 'lcc_mcid/mcid/bin' directory:
      $ cd lcc_mcid/mcid/bin

2- Start the 'mcid' model checker:
      $ ./mcid

3- To manually verify an interaction model file IM against the deontic
   file D and temporal file T, run the following command:
      |?- verify(IM,D,T).

   Note that the file IM's location would be
   './interaction_models/IM.lcc', the files D and T's locations would
   be './agents/D.dr' and './agents/T.mu', respectively.
   Note that manual verification might invoke the automatic
   verification of other interaction models.



Copyright © 2008 Nardine Z. Osman
=================================

Permission granted for personal and educational use only.  Commercial
copying, hiring, lending is prohibited.  This notice must remain
intact.

For any additional information, please send an email to
nardine@gmail.com.