Heuristics for checking Liveness Properties with Partial Order Reduction

Description of this page

This page presents the benchmark used in our paper.

You can download the fork of Spot we use for our experiments [here].

You can download the CSV containing all our experiments [here].

You can download the normalized-CSV (in term of states) containing all our experiments [here].

Benchmark Analysis

You can find a fine-grain analysis of the (raw) benchmark presented in the paper [here]. Notice that this page may be long to load since it aggregates all data and visualisation tools. If you try to open this page you might encounter some trouble saying that some script does not reply. Just press wait (possibly many times) or instead to use another web-browers.

You can also find a fine-grain analysis of the (normalized) benchmark presented in the paper [here]. (This page may also claims no-reply messages)

You can find an high-level analysis of the data through the following picture or by dowloading a fine grain analysis [here]

States Comparison (normalized) --
Fig1. - Variations in term of states (data have been normalized).

States Comparison (normalized)
Fig2. - Variations in term of transitions (data have been normalized).

States Comparison (normalized)
Fig3. - Variations in term of walltime millisec (data have been normalized).
Throughput Comparison (normalized)
Fig4. - Variations in term of throughput (here, best is at the top).

Standard Score Comparison (normalized)
Fig5. - Comparison of Mean Standard Score for states, transitions, and computation time.

All previous pictueres and scatter plot can be regenerated using the two R-scripts [here] and [here].

Benchmark Description

This benchmark uses 38 models extracted from the BEEM benchmark that can be downloaded [Here]. For each model, we generate 100 variations such that:

The benchmark is composed of the following models

Replay Benchmark

Before installing Spot, you need to install the DiVine tool patched by the LTSmin Team, since we rely on it to generate the state space of each model. You just have to follow instructions given in section 10 of [LTSmin Homepage].

Download and install our fork of Spot thought classic steps:

Once all previous steps have been done, you should find a binary file modelcheck in the spot/iface/ltsmin directory. This is the binary file we use for our experiments.

A lot of options can be combined for this binary file, so the best way to reproduce our benchmark is to download the following file [Ref.tgz]. Once the file downloaded, you can do tar xzvf REF.tgz to uncompress the directory that contains all the benchmark. In the resulting REF directory you will find: