BDD-Based Module

Dependencies

A C++14 compiler, GNU make, Bison, and flex are required. The parser was originally developed against Bison 2.5, but more recent versions (tested up to 3.8.2) build without changes.

On macOS, if you have MacPorts installed, it should be sufficient to just run:

% sudo port install bison

On FreeBSD you may need to install GNU make:

# pkg install gmake

On Arch Linux all required tools are typically already present via base-devel. If not, install them with:

# pacman -S --needed base-devel bison flex

On Debian/Ubuntu:

# apt install build-essential bison flex

Build

Clone the ReactICS’s repository and run the build procedure:

% git clone https://codeberg.org/arturmeski/reactics.git
% cd reactics
% ./reactics setup

Examples

The examples directory contains sample input files specified using RSSL.

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.drs

The above should print:

 ------------------------------------------------
 -- ReactICS -- Reaction Systems Model Checker --
 ------------------------------------------------

Using BDD-based Bounded Model Checking
Formula ((EF(E< proc0.allowed >X(proc0.in)) AND EF(E< proc1.allowed >X(proc1.in))) AND EF(E< proc2.allowed >X(proc2.in))) holds

SMT-Based Module

Installation

Python 3 with the Z3 module installed should be sufficient to run the SMT-based module of ReactICS.

On Arch Linux, install the system Z3 package (which provides the Python bindings):

# pacman -S z3

On Debian/Ubuntu:

# apt install python3-z3

Alternatively, on any platform, install via pip:

$ pip install z3-solver

Usage & Examples

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/scalable_chain.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 exclusion 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