SPEC with reduced semantics

This version of SPEC implements the reduced semantics from the paper by Baelde, Delaune and Hirschi, and an adapted constraint resolution procedure. It should only be used on simple processes, for which bisimulation and trace equivalence coincide. Further, the tool currently only supports processes whose basic processes are sequences of blocks composed of one input, at most one test, and one output. The original version of SPEC due to Alwen Tiu has been firstly presented in [1].


You can download the git repository of the project with:

    git clone http://www.lsv.ens-cachan.fr/~hirschi/spec.git

The repository contains several branches, one for each level of optimization. The command # git branch -r lists them all.

Compiling SPEC

Below we assume the directory is called 'spec' in the user's home directory. SPEC, and the Bedwyr engine it relies on, are implemented using the Ocaml language, so you will need to have Ocaml installed to compile SPEC. The script that calls spec in a more convenient way requires Python.

To compile the system, use the following commands:

Running SPEC

The produced binary is src/spec and can be used like the original spec with # src/spec Tests are available in the "examples/" directory. The examples of the benchmark are in "examples/tests_h.spi". To automatically run tests (with timing, and validity checking), go to the corresponding branch (e.g., "optim") and run: # cd bench_test; python test_valid.py. Optionally, append the option " -d hard" to run the examples from the benchmark. You could also write your own tests in "examples/tests.spi" before the first one.

About LSV