This benchmark provides a set of 860 random formulas over 8 models extracted from the BEEM benchmark
(http://anna.fi.muni.cz/models/)
at.4.dve
bakery.4.dve
bopdp.3.dve
elevator.4.dve
elevator2.3.dve
leader-election.3.dve
lifts.4.dve
production-cell.3.dve
Replay
A README explaining how to launch the set up and interpret results [Here].
All experiment where performed using a fork of Spot avalaible [Here].
The full archive of models and formulas can be downloaded [Here].
The resulting CSV and Excel analysis can be found [Here].
How to interpret this page
We use shorthand for algorithms name :
dc13 : for Dijkstra emptiness check
lc13 : for Tarjan emptiness check
uc13 : for Gabow emptiness check
All these names can be postfixed by
"-cs" : Do not use the stack compression technique proposed in the paper
"+cs" : Use the stack compression technique proposed in the paper
"-ds" : Do not use a store for DEAD states
"+ds" : Use a store for DEAD states
What does the fields names stand for?
In the folowing tables we use descriptors that allows to compare each emptiness check
variations.
time (walltime): Wall time in milliseconds
time (user): User time
time (system): System time
dfs peak: the dfs peak observed
roots peak: the roots peak observed for Dijkstra and Gabow only
live peak: the live peak observed (for Gabow Union Find peak)
dead peak: the dead peak observed
Update calls: number of call of Update
Loops Update: number of loop inside Update (Dijkstra and Gabow only)
roots popped: number of roots popped
visited transitions: the number of transitions visited by the algorithm
visited states: the number of states visited by the algorithm
cost function peak: memory peak observed (in words)
trivial popped: number of trivial roots popped (for Gabow and Tarjan only)
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.