HST
===

HST is a library and set of command-line programs for processing CSP
scripts.  The goal for the 1.0 release is to support refinement
checking in the traces (T), stable failures (F), and
failures-divergences (N) semantic models, all of which are described
in [1].

[1] A. W. Roscoe.  /The theory and practice of concurrency/.  Prentice
    Hall, 1998.  ISBN 0-13-6774409-5.
    http://web.comlab.ox.ac.uk/oucl/publications/books/concurrency/

HST is divided into two major sections: the CSP₀ library, written in
C++, and the CSPM libary, written in Haskell.  C++ was chosen for
speed, since all LTS generation and refinement checking happens in the
CSP₀ library.  Haskell was chosen since CSPM is a lazy, functional
lanaguage — this us allows to use the same features of Haskell and not
have to implement a lazy functional interpreter ourselves.

For installation instructions, please see the INSTALL file.  There are
currently two command-line programs — “cspm” and “csp0”.  The first
allows you evaluate expressions in a CSPM script, and to compile CSPM
process expressions into the corresponding CSP₀.  The second allows
you to perform refinement checks on these compiled CSP₀ scripts.  Each
program is self-documented; run “csp0 help” or “cspm help” for usage
details.  The CSP₀ language is described in the csp0.html file, which
should be installed as part of the standard installation process.  The
most recent (and complete) description of the CSPM language can be
found in the FDR2 reference manual [2].

[2] Formal Systems (Europe) Ltd.  /Failures-Divergence Refinement:
    FDR2 Manual/.  2005.
    http://www.fsel.com/