This directory contains Prolog code for a simple CTR interpreter and a
number of simple CTR transaction bases.  It was designed to run on
XSB, but can be ported to other Prologs without difficulty.  The
interpreter assumes that the transaction base consists of
concurrent-Horn rules, and that the database consists of Prolog rules
and facts (ie, Horn rules and atoms).

To run the interpreter, enter XSB and consult the two files ctr.pl and
updates.pl.  The former is the ctr interpreter, and the latter
provides backtrackable updates.  The remaining files in the directory
are examples of ctr programs.  They must be dynamically loaded.  e.g.,
the command load_dyn('synchro.pl') will load the synchronization
example.  Thus, the following commands will load the interpreter and a
sample ctr program:

	consult('ctr.pl').
	consult('updates.pl').
	load_dyn('synchro.pl').

To avoid naming conflicts, don't load more than one CTR program at a
time.


Syntax:
------
We are working on a parser for CTR syntax.  However, until it is
developed, CTR programs must be written using the internal
representaion of the CTR interpreter.

The interpreter uses function terms to represent logical connectives
in CTR.  Specifically,

	seq(phi,psi)  represents  phi x phi
	conc(phi,psi)  represents  phi | psi
	or(phi,psi)  represents  phi \/ psi
	isolate(phi)  means execute phi in isolation

Thus the term seq(A,seq(B,C)) represents the transaction formula
AxBxC.  Some special connectives are also provided:

	conc0(phi,psi) is an efficient form of conc(phi,psi) for cases
	when phi and psi commute.  In such situations, if one
	interleaving of phi and psi fails, then they will all fail, so
	don't bother trying them all.

	monitor(Task) prints messages on the screen during execution
	and backtracking.  It is useful for monitoring the execution
	of a transaction program.

See the documentation in file ctr.pl for more details.

Rules in the transaction base are represented by Prolog rules of the
form trans(head) :- body.  For instance, the following CTR rule

	p <- q x (r | t)

is represented by the following Prolog rule:

	trans(p) :- seq(q,conc(r,t)).


Additional Requirements:
-----------------------
Certain other rules must also be added to the Prolog rulebase.
Eventully these will all be generated automatically from CTR code, but
for now they must be created manually.  All the example CTR files
include these rules.

(1) If the transaction base contains the rule p <- body, then the
following rule must be added to the Prolog rulebase:

	p :- fail.

This rule simply tells Prolog that the predicate p is defined.
(Without it, XSB will sometimes give the error "p is undefined".)


(2) A CTR database may contain Prolog rules and atoms.  Only the atoms
can be updated by CTR programs.  Moreover, if p(X,Y) is an updatable
atom, then the following rule must be added to the Prolog rulebase:

	p(X,Y) :- db(p(X,Y)).

Updatable atoms are not actually stored in the database.  Instead
insert and delete tags are.  (See the file updates.pl for details.)
The above rule examines the insert and delete tags for atom p(x,y) to
determine whether p(x,y) is true in the current database state.