A library providing a parser, type checker and evaluator for CSPM.

Latest on Hackage:1.0.0

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow to host generated Haddocks.

BSD3 licensed and maintained by Thomas Gibson-Robinson


This library provides a FDR-compliant parser, type checker and (experimental) evaluator for machine CSP files.

There is also a program, cspmchecker, that makes use of this library to provide command line type checking.

Build Status


The simplest method is to install via Hackage. cabal install cspmchecker will install cspmchecker and its dependencies.

Otherwise, if you obtain a source distribution then the following commands will install libcspm.

cabal configure
cabal build
cabal install

To install cspmchecker, firstly install libcspm as above, then change directory to cspmchecker and run the following commands.

cabal configure
cabal build
cabal install

This should make cspmchecker available from your command line shell (if not check that the location cabal installs binaries to is on your $PATH).

Usage of cspmchecker

From a command line shell simply do cspmchecker file.csp to type check the files. Any error messages will be printed out. For example:

$ cspmchecker ucsexamples/chapter04/abp.csp 
Checking ucsexamples/chapter04/abp.csp.....
    Couldn't match expected type Int.Int with actual type Int
    In the expression: bit
    In the expression: ack == bit
    In the expression: (ack == bit)

Documentation of the type system is forthcoming.

Usage of libcspm

See for documentation.


To test libcspm run the following commands.

cabal configure --enable-tests
cabal build
cabal test

Bug Reports

Please files bug reports at Please provide a minimal example script that exhibits the error (if possible).


1.0.0 Thomas Gibson-Robinson <> 2013-10-11
This is a major release that delivers a fully functional evaluator that
is both efficient and compatible with FDR2. This is the library used by FDR3
(available from for parsing and
manipulating CSPm.

* Changes to the evaluator included:
* Major efficiency and memory improvements. In particular, when a
pattern binds to a process, the entire tree of operator applications
is not saved in the environment, meaning that memory usage is
minimised. This should have no noticeable performance impact.
* Fixed the naming of processes within let expressions.
* The ability to handle all processes.
* Misc fixes with dot handling, including within prefixes.
* Improvements to the handling of infinite sets.
* An error is thrown when a datatype is not rectangular.
* Events is now available.
* An error is thrown when an invalid event or datatype is constructed
(e.g. when c.1 is constructed, if c is a channel allowing only 0 as
its first field).
* The pretty printing structure has been overhauled to make it possible to
have side effects. This permits more attractive pretty printing of values.
* Added Hashable instances for many of the built in datatypes.
* Fixed many small incompatibilites in the parser.
* Fixed a bug that prevented multiple assertions from being included.
* Enhanced the renamer to produce better errors.
* Add full support for modules, including parameterised modules.
* Fixed many small bugs in the evaluator.

0.2.1 Thomas Gibson-Robinson <> 2012-01-18
* Fixed a bug in the typechecker that prevented certain (uncommon)
functions that took function arguments that were polymorphic in dot from
being type checked.
* Exposed ErrorMessages to allow clients to present them more usefully.
* Added location information to renamer errors.
* Made compatible with GHC 7.0.4.

0.2.0 Thomas Gibson-Robinson <> 2012-01-04
* Enhanced the evaluator:
* Dot is not handled correctly;
* More versions of infinite sets are allowed;
* Add experimental and partial support of $ in prefixes.
This should mean that the evaluator has feature parity with FDR2,
although it does lack testing.
* Added a renamer that renames all variables in a file or expression to
ensure that they do not clash.
* Enhanced the parser to be more compatible with FDR2 with regard to the
ambiguity with > and end of sequence. See the comment in
* Fixed a bug in the typechecker where it would incorrectly allow yield
types to be chosen in prefixes. For example, given c?x?y:{0,1} where
c is a channel that has only one field, of type A, the typechecker would
assign a type of Int=>A for x, which does not match the evaluator which
would assign x to the whole A. To fix this a new type constraint was
added, Inputable, that any type other than yield satisfies.
* Added a lot more documentation, particularly on the abstract syntax tree
and how to use the library.

0.1.2 Thomas Gibson-Robinson <> 2011-11-04
* Fix building with GHC 7.2 and Alex 3.
* Remove the last few remaining mentions to sfdr (the old name for

0.1.1 Thomas Gibson-Robinson <> 2011-11-03
* Fix the build of cspmchecker.

0.1 Thomas Gibson-Robinson <> 2011-11-03
* Initial Release.
comments powered byDisqus