ReactICS

Reaction Systems Verification Toolkit

The toolkit consists of two separate modules implementing:

• BDD-based methods
• SMT-based methods

Examples

The examples directory contains sample input files.

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

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

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:

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

Reaction synthesis

To test the reaction synthesis approach on a mutual exclution protocol modelling three processes, run the following command:

./reactics smt examples/smt/mutex_param.py -n 3 -s 1 -o