Benchmark for symbolic model checking using TGTA versus TGBA
Description:
This benchmark provides a set of 3200 random formulas over 16 models extracted from the BEEM benchmark (available at http://anna.fi.muni.cz/models/) which classifies all models into five categories (see Web Portal for Benchmarking Explicit Model Checker):
- Mutual exclusion
- Communication protocol
- Leader election algorithm
- Controller
- Puzzle, planning, scheduling
For all above models there are 100 verifed formulas and 100 violated ones.
| Model | Type | Short Description |
| at.5.dve | Mutual exclusion | Alur-Taubenfeld mutual exclusion algorithm |
| bakery.4.dve | Mutual exclusion | Bakery mutual exclusion algorithm |
| bopdp.3.dve | Controller | Audio/Video Power Controller |
| brp2.3.dve | Communication protocol | Bounded retransmission protocol |
| elevator.4.dve | Controller | Elevator controller |
| fischer.5.dve | Mutual exclusion | Fisher's mutual exclusion algorithm |
| lamport_nonatomic.5.dve | Mutual exclusion | Lamport mutual exclusion protocol with nonatomic operations |
| lamport.7.dve | Mutual exclusion | Lamport's fast mutual exclusion algorithm |
| lann.6.dve | Leader election algorihtm | Lann leader election algorithm for token ring |
| lann.7.dve | Leader election algorihtm | Lann leader election algorithm for token ring |
| lifts.7.dve | Controller | Distributed system for lifting trucks |
| peterson.5.dve | Mutual exclusion | Peterson's mutual exclusion protocol for N processes |
| pgm_protocol.8.dve | Communication protocol | Bounded retransmission protocol |
| phils.8.dve | Mutual exclusion | Dining philosophers problem |
| production-cell.6.dve | Controller | Production cell case study |
| reader_writer.3.dve | Other protocol | Readers-writers problem |
Sumup results
The resulting CSV of this experiment can be found here.
How to replay the benchmark?
Download models (.etf files) and formulas (.ltl files):
download the following archive : benchmark.tar.gz
Download and install the tools:
The benchmark can be replayed using the tools avalaible at: Spot and Ltl-Its (Skip the step "3. install of ITS CTL checker") ).
Reproducing using TGBA:
To run symbolic model checking using TGBA (-SFSOWCTY option):
$SDD_HOME/ltl/src/its-ltl -SFSOWCTY -ltl '[the LTL formula]' -t ETF -i [the ETF Model file (.etf)] -c -x
Example: $SDD_HOME/ltl/src/its-ltl -SFSOWCTY -ltl 'GF ("P_0.k=1")' -t ETF -i peterson.4.dve.etf -c -x
Reproducing using TGTA:
To run symbolic model checking using TGTA (-SFSOWCTY-TGTA option):
$SDD_HOME/ltl/src/its-ltl -SFSOWCTY-TGTA -ltl '[the LTL formula]' -t ETF -i [the ETF Model file (.etf)] -c -x
Example: $SDD_HOME/ltl/src/its-ltl -SFSOWCTY-TGTA -ltl 'GF ("P_0.k=1")' -t ETF -i peterson.4.dve.etf -c -x