ReactICS. Reaction Systems Verification Toolkit

View the Project on GitHub arturmeski/reactics


Reaction Systems Verification Toolkit

The toolkit consists of two separate modules implementing:


Installing everything manually

(to be added)

Virtual Machine

The easiest way to try out ReactICS is to download the VM where everything is alread installed. This a VirtualBox virtual machine. After booting it up, you can log in as reactics with the same password. After logging in, ReactICS is available in the reactics directory:

$ cd reactics

An update and setup needs to be performed before running any type of verification:

$ ./reactics setup

After performing these steps you should be ready to start using ReactICS.


The examples directory contains sample input files.

Multi-agent reaction systems (rsCTLK verification)

To quickly test the BDD module you can perform verification of the TGC controller consiting of three trains:

$ ./reactics bdd -c f1 examples/bdd/

The above command tests the formula labelled f1 in the input file.


To test the SMT module you can perform reachability verification of the scalable chain system:

Running the benchmark without any arguments tells us what parameters are available:

$ ./reactics smt examples/smt/

 -- ReactICS -- Reaction Systems Model Checker --

arguments: <chainLen> <maxConc> <formulaNumber>

We may execute the benchmark for chainLen=2, maxConc=3, and formulaNumber=1 using the following command:

$ ./reactics smt examples/smt/ 2 3 1

rsLTL verification

To test the SMT module for rsLTL verification the scalable chain system benchmark may be used.

$ ./reactics smt examples/smt/ 2 5 1

Reaction synthesis

To test the reaction synthesis approach on a mutual exclution protocol modelling three processes, run the following command (three processes, parametric verification, result optimised with OptSMT):

$ ./reactics smt examples/smt/ 3 p -o

To check the available parameters for the benchmark, we run it with -h:

$ ./reactics smt examples/smt/ -h

 -- ReactICS -- Reaction Systems Model Checker --

usage: [-h] [-v] [-o] scaling {p,np-p,np-np}

positional arguments:
  scaling         scaling parameter value
  {p,np-p,np-np}  Selects the mode: p - parameter synthesis (parametric
                  implementation), np-p - non-parametric with parametric
                  implementation (with the parameters substituted), np-np -
                  non-parametric with non-parametric implementation
                  (parameters substituted)

optional arguments:
  -h, --help      show this help message and exit
  -v, --verbose   turn verbosity on
  -o, --optimise  minimise the parametric computation result