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:43:44 +01:00
parent e2561014c6
commit 1a49abea23
1 changed files with 12 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
README.md
View File

@@ -10,12 +10,16 @@ The toolkit consists of two separate modules implementing:
The `examples` directory contains sample input files. 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: 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 $ ./reactics bdd -c f1 examples/bdd/tgc.rs
``` ```
### Reachability
The above command tests the formula labelled `f1` in the input file. 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: To test the SMT module you can perform reachability verification of the scalable chain system:
@@ -24,6 +28,14 @@ To test the SMT module you can perform reachability verification of the scalable
$ ./reactics smt examples/smt/chain_reaction.py 2 3 1 $ ./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 you need, the following command may be used:
```
./reactics smt examples/smt/scalable_chain.py 2 5 1
```
### Reaction synthesis ### Reaction synthesis
To test the reaction synthesis approach on a mutual exclution protocol modelling three processes, run the following command: To test the reaction synthesis approach on a mutual exclution protocol modelling three processes, run the following command: