832 B
832 B
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
# EOF