dcreager / hst
watch download tarball
public
Forks2Right
Watchers1Right
Fork of hst/hst
Description: An open-source refinement checker for the CSP process algebra
Homepage: http://hst.github.com/
Clone URL: git://github.com/dcreager/hst.git
hst /
name age
history
message
file .gitignore Wed Feb 20 16:41:13 -0800 2008 Improvements to build infrastructure The build... [Douglas Creager]
file AUTHORS Sat Jan 19 04:47:38 -0800 2008 C++ implementation of integer sets This is an ... [Douglas Creager]
file CMakeLists.txt Mon Apr 20 19:39:57 -0700 2009 Eliminating CMake warnings This patch fixes th... [Douglas Creager]
file COPYING Sat Feb 23 14:11:47 -0800 2008 Fixes to basic documentation set I've made som... [Douglas Creager]
file INSTALL Tue Feb 10 15:34:00 -0800 2009 Using Markdown for documentation This patch mo... [Douglas Creager]
file NEWS Sat Jan 19 04:47:38 -0800 2008 C++ implementation of integer sets This is an ... [Douglas Creager]
file README.md Tue Feb 10 15:34:00 -0800 2009 Using Markdown for documentation This patch mo... [Douglas Creager]
file TODO Fri Apr 25 21:00:53 -0700 2008 Adding comments to CSP₀ scripts This patch add... [Douglas Creager]
directory build-scripts/ Tue Feb 10 16:23:14 -0800 2009 Include error messages in expected CSP₀ test ou... [Douglas Creager]
directory cmake/ Sat May 31 10:25:02 -0700 2008 Replacing custom proxy_iterator with Boost's tr... [Douglas Creager]
directory cspm/ Mon Mar 23 15:43:49 -0700 2009 Complex channels This patch introduces support... [Douglas Creager]
directory doc/ Tue Feb 10 16:31:54 -0800 2009 Replicated internal choice This patch introduc... [Douglas Creager]
file graffle Sat Jan 19 04:47:38 -0800 2008 C++ implementation of integer sets This is an ... [Douglas Creager]
directory include/ Fri Sep 11 06:07:18 -0700 2009 Use std:: namespace prefix in header files In ... [Douglas Creager]
directory libs/ Tue Jan 29 14:40:54 -0800 2008 Using cmake for the build system This patch re... [Douglas Creager]
directory packaging/ Mon Feb 09 19:39:05 -0800 2009 Remove tabs from source files [Douglas Creager]
file scratch.py Sun Apr 27 16:38:47 -0700 2008 Current “interrupt” operator is actually “timeo... [Douglas Creager]
directory src/ Mon Mar 02 13:14:27 -0800 2009 Fixed column numbers when using Bison 2.3 Biso... [Douglas Creager]
directory tests/ Mon Apr 20 19:39:57 -0700 2009 Eliminating CMake warnings This patch fixes th... [Douglas Creager]
README.md

% 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/>