This benchmark provides a set of 3268 random formulas over 10 models extracted from the BEEM benchmark
(http://anna.fi.muni.cz/models/). We
compute formula such that for each models the NDFS of Gaiser and
Schwoon takes 2 hours of
computation for verified formula and 2 hours for violated
formulas. All formulas where selected such that they take between
10 seconds and 30 minutes (for violated formula there exist a
transition ordering that satisfies this constraint).
adding.4.dve
bridge.3.dve
brp.4.dve
collision.4.dve
cyclic_scheduler.3.dve
elevator2.3.dve
elevator.4.dve
exit.3.dve
leader-election.3.dve
production-cell.3.dve
Replay
A README explaining how to launch the setups and interpret results here.
All experiments where performed using a fork of Spot avalaible here.
We postfix algorithm names with _number-of-threads:
dijkstra : for Dijkstra parallel emptiness check
tarjan : for Tarjan parallel emptiness check
mixed : for a combinaison of 2 previous emptiness checks
cndfs : the cndfs emptiness check implemented in LTSmin
owcty : the owcty emptiness check implemented in DiVine
What does the field names stand for?
In the folowing tables we use descriptors that allows to compare each emptiness check
variations.
time: Wall time in milliseconds
violated?: is the property violated?
Tools
Inputs
Cumulative Summary
Each column shows a sum over all inputs processed by one tool. The second column shows the count of inputs processed.
Green and red highlight minimum and maximum values per column.