artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Readme update

Browse Source
This commit is contained in:
Artur Meski
2019-09-29 15:49:11 +01:00
parent 38b84bdc22
commit 39761502d0
1 changed files with 19 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

32
README.md
View File

@@ -24,19 +24,7 @@ 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
```
### rsLTL verification
To test the SMT module for rsLTL verification with the scalable chain system, the following command may be used:
```
./reactics smt examples/smt/scalable_chain.py 2 5 1
```
Running the benchmark without any arguments tells us what parameters can be used:
Running the benchmark without any arguments tells us what parameters are available:
```
./reactics smt examples/smt/scalable_chain.py
@@ -48,6 +36,24 @@ Running the benchmark without any arguments tells us what parameters can be used
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: