This paper is an extension of our previous TACAS paper. Detailled results about this paper can be found [here]. Since this page only meant to present new experiments, the interested reader will refer this previous page to understand the whole setup for the comparison with other tools such as DiVine (owcty) or LTSmin (cndfs).
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).
Warning! We plan to integrate all these algorithms into the latest version of Spot. Before downloading and using this fork, checkout if there is a more recent version of Spot that integrates all these algorithms.
The fork of Spot used to develop these parallel emptiness checks [here].
The CSV can can be found [here].
The full logs can be found [here].