This file gives instructions for installing and running the prototype
implementation of the view abstraction checker.  Please mail me at
gavin.lowe@cs.ox.ac.uk if you have difficulties. 

Installation
------------

These instructions assume you already have scala, java and FDR4 installed. 

1. Unpack util.zip somewhere convenient; this will give the ox.gavin package.

2. Update the makefile so that the first few lines give the locations of the
ox.gavin package (the directory containing ox), the base of the FDR
installation (directory including lib), and the base of the Scala installation
(directory containing lib).

3. "make" should now compile all the files.

Please contact me if this doesn't work.

Scripts
-------

The script should include annotations, defining the families of components and
the servers.  For example

-- @VA component process = FreeNode
-- @VA component alphabet = alphaNode
-- @VA component identity type = NodeID
-- @VA component process = Thread
-- @VA component alphabet = alphaThread
-- @VA component identity type = ThreadID
-- @VA servers = ServerSet

This defines a family of components FreeNode, with alphabets given by
alphaNode, and indexed by NodeID.  The types should be

FreeNode :: (NodeIDType) -> Proc
alphaNode :: (NodeIDType) -> {Event}

where NodeIDType is the type that includes NodeID (plus maybe distinguished
values).

Likewise, the above defines a family of components Thread, with alphabets
given by alphaThread, and indexed by ThreadID.

Finally, the servers are defined by ServerSet, or type

ServerSet :: <(Proc, {Event})>

each pair in the sequence representing one server and its alphabet.

Usage
-----

Example:

scala -cp .:/users/gavinl/Scala/Util:/users/gavinl/bin/FDR4/fdr/lib/fdr.jar ViewAbstraction.VA CSP/TreiberStack.csp --shape 1 2 --shape 2 1 --shape 3 0

The classpath must include the location of the ox.gavin package, and the FDR
jar file.  This example will run on the file CSP/TreiberStack.csp.  It will
use abstraction set
  (Node:1, Thread:2) U (Node:2, Thread:1) U (Node:3, Thread:0).

Optional command-line arguments:

* --shape n1 n2 ... nk: includes a shape (F1:n1, ..., Fk:nk) in the
  abstraction set, where the families of components are F1, ..., Fk, listed in
  that order in the annotations of the input file.

* -k k: set the abstraction set to be all views of size k; this abbreviates a
   sequence of --shape arguments. 

* --checkDeadlock: include a check for deadlock freedom.

* --significancePath f1 f2 ... fk: include a chain <f1, ..., fk> indicating
  significant components, as described in Section 8 of the paper; to be
  including when checking for deadlock freedom. 

* --bound b: limit the search to a depth of b.

* --profile t: run profiling, sampling every t ms, and giving tree output.

* --profileFlat t: run profiling, sampling every t ms, and giving flat
  output. 

Other programs
--------------

Experiment.scala corresponds to the experiments reported in the paper.  It
will be necessary to edit the "classpath" variable in this file for it to
run. 

Instrumentation.java performs memory profiling.  Read the instructions in the
file (but the framework this uses is a pig to get to work).