%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% This is the README file for the './agents' directory
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Written by Nardine on 04/09/2007 - modified on 17/09/2007
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The './agents' directory contains all the agents' files.  These are
divided into two categories:
    1- Agents Specification File ('*.kb' files)
    2- Deontic Rules File ('*.dr' files)
In addition to the agents' files, there is also one more file type in
this directory:
    3- Temporal Properties File ('*.mu' files)


KB Files:
=========
Each agent can have only one specification file (of type '*.kb').
This is essentially the agent's knowledge.  If an agent is running
some interaction model, then anything in that interaction model that
requires the agent's knowledge should be defined in this file.

The '*.kb' file essentially contains Prolog facts and rules.



DR Files:
=========
Each agent may also have more than one deontic file ('*.dr').  This is
the set of deontic rules to be verified by the agent against some
interaction model.  The verification takes place before the agent
joins the interaction model.  For each scenario, different deontic
rules apply.  Therefore, an agent may have more than one '*.dr' file,
possibly one for each scenario it joins.

The '*.dr' file contains the specification of deontic rules.  These
define what the agent can or cannot do (i.e. permissions and optional
actions, respectively) and must or must not do (i.e. obligations and
prohibitions, respectively).  
The '*.dr' file is composed of a collection of the following prolog
facts and rules (refer to Section 3.4.2 of the thesis for further
details): 
    - can(RuleID,Agent,Action,+) <- Condition.
    - can(RuleID,Agent,Action,-) <- Condition.
    - must(RuleID,Agent,Action,+) <- Condition.
    - must(RuleID,Agent,Action,-) <- Condition.
where 'RuleID' is a unique identifier for this deontic rule, 'Agent'
is defined in the LCC format of 'a(Role,Id)', and 'Action' could
either be 'in(Message)', 'out(Message)', or 'c(Constraint)'.  Finally,
the 'Condition' could be any term in Prolog syntax.



MU Files:
=========
When verifying interaction models, one may which to verify certain
properties of the interaction.  Tbese may or may not be related to
specific acgents.  For instance, they could be properties that the
protocol engineer wishes to verify.  Since these properties may still
be specified by the agents when necessary, we place these '*.mu' files
in the agent's directory.

The '*.mu' file contans a list of temporal properties specified in the
alternation free mu-calculus.  The syntax is defined as follows:
    Property    := Id += Def.              | 
		   Id -= Def.

    Def         := Def and Def            |
		   Def or  Def            |
		   diam(ActionsList,Def)  |
		   box(ActionsList,Def)   |
		   tt                     |
		   ff                     |
		   Id

    ActionsList := [Action,...]           |
		   -[Action,...]

    Action      := in(Message,Agent)      |
		   out(Message,Agent)     |
		   c(Constraint)

    Agent       := a(Role,AId)

    Id,Message, 
    Constraint,
    Role,AId    := Term

where += and -= represent the mu and nu fixpoint operators,
respectively.  diam(_,_) and box(_,_) represent the <> and [] modal
operators, respectively.  'tt' and 'ff' stand for 'true' and 'false',
respectively.  [X,...] represents a Prolog list which could either be
empty or contains one or more elements of type 'X'.  Finally, 'Term'
is a Prolog term.

Refer to Section 2.3.2 for more information on the semantics of the
mu-calculus.

Note that each '*.mu' file should always contain one predicate of the
form: 'verify([Id,...]).'  This is because one property may be
defined in terms of several sub-properties in the syntax above.
However, only the main property IDs should be called when performing
verification.  These property IDs should be specified in advance in
the 'verify/1' predicate.



Note:
=====
In current simulations, all agents are made to run from the same
machine.  As a result, currently all the agents' files are gathered in
this directory.  This does not necessarily have to be the case.  In
reality, each agent will be running on a different machine.  Note that
the only thing that needs to be synchronised then by all agents is the
contents of the './lcc_engine/server.addr', which is necessary for
communication.
