CIA: A CSP Interpreter and Animator
--------------------------------------------
Preliminary Release

(C) 2000-2003 Michael Leuschel, DSSE, University of Southampton
All rights reserved.
Free for academic or non-commercial use.

CIA uses state-of-the-art Prolog technology (co-routining, finite
domain constraint solvers,...) to achieve symbolic debugging, model-based
and temporal-logic based model checking.
The tool is being developed within the EPSRC grants iMoc and ABCD.

Development, Copyright and Intellectual Property Rights:
Interpreter & Animator:
	Michael Leuschel 
TCL/TK Interface:
	Laksono Adhianto, Michael Leuschel

Open a .csp file to start.
The animator will start the process called 'MAIN'.

=============
RELEASE NOTES
=============

* supported syntax is not (yet) FDR compatible:
	- variables should start with an underscore
        - only prefix notation is supported for operators
           (e.g., use +(_x,1) instead of _x + 1)
        - no expressions are allowed within tests (you have to
           use let expressions for that), but expressions are
           allowed for agent calls
	- ; semicolon terminates process definitions
	- sequential composition is denoted by ->>
	- lists or sets are still represented by cons(,) and nil
	- there is no support yet for CLP over finite domains or over reals or 
	rationals (the interpreter just uses co-routining via the when directive)
	- the treatment of suspended/delayed goals within the interpreter is not 
	yet fully sound (the animator assumes all delayed goals can be satisfied,
        when delayed goals exists the animator adds *** to the operation)
	- the parser is a hack, with bad error recovery and bad error messages,
          and operator priority has not been implemented (use parentheses 
          as much as possible !)


* TO DO:
	- re-write negation (for if-then-else or constrained prefix) so that it 
	correctly deals with suspended/delayed goals (SICStus Prolog does not 
	handle them as I initially thought !!)
	- allow for constrained variables (FD, Real, Bool, Rational,...), similar 
	to the B animator, maybe also allow for sets, relations,...
	- BTA a (simplified) version of the interpreter so that it can be fed into 
	LOGEN (done)