107 lines
3.2 KiB
Markdown
107 lines
3.2 KiB
Markdown
# ReactICS
|
|
|
|
Reaction Systems Verification Toolkit
|
|
|
|
The toolkit consists of two separate modules implementing:
|
|
* Methods implemented using binary decision diagrams (BDD) for storing and manipulating the state space of the verified system.
|
|
* Methods translating the verification problems into satisfiability modulo theories (SMT).
|
|
|
|
# Installation
|
|
|
|
The easiest way to try out ReactICS is to download [http://reactionsystems.org/ReactICS.zip](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.
|
|
|
|
## Examples
|
|
|
|
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/tgc.rs
|
|
```
|
|
|
|
The above command tests the formula labelled `f1` in the input file.
|
|
|
|
### Reachability
|
|
|
|
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/scalable_chain.py
|
|
|
|
------------------------------------------------
|
|
-- 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/chain_reaction.py 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/scalable_chain.py 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/mutex_param.py 3 p -o
|
|
```
|
|
|
|
To check the available parameters for the benchmark, we run it with `-h`:
|
|
|
|
```
|
|
$ ./reactics smt examples/smt/mutex_param.py -h
|
|
|
|
------------------------------------------------
|
|
-- ReactICS -- Reaction Systems Model Checker --
|
|
------------------------------------------------
|
|
|
|
usage: mutex_param.py [-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
|
|
```
|
|
|
|
|