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].
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]
All previous pictueres and scatter plot can be regenerated using the two R-scripts [here] and [here].
This benchmark uses 38 models extracted from the BEEM benchmark that can be downloaded [Here]. For each model, we generate 100 variations such that:
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:
Proviso name (in the paper) | directory name(aka options separated with __ and prefixed by opt) |
Full | opt-T__-sm__-por=all |
None | opt-T__-sm__-por=none |
Source | opt-T__-sm__-por=source |
CondSource | opt-T__-sm__-b__-por=source |
CondSourceKnown | opt-T__-sm__-b__-a__-por=source |
WeightedSource | opt-T__-sm__-l__-por=source |
WeightedSourceKnown | opt-T__-sm__-a__-l__-por=source |
WeightedSourceScan | opt-T__-sm__-c__-l__-por=source |
WeightedSourceKnownScan | opt-T__-sm__-a__-c__-l__-por=source |
Dest | opt-T__-sm__-por=destination |
CondDest | opt-T__-sm__-b__-por=destination |
CondDestUnknown | opt-T__-sm__-b__-r__-por=destination |
ColoredDest | opt-T__-sm__-b__-del__-por=destination |
ColoredDestUnknown | opt-T__-sm__-r__-b__-del__-por=destination |
WeightedDest | opt-T__-sm__-por=delexp |
WeightedDestUnknwon | opt-T__-sm__-r__-por=delexp |
WeightedDestScan | opt-T__-sm__-c__-por=delexp |
WeightedDestUnknownScan | opt-T__-sm__-c__-r__-por=delexp |
DeepestDest | opt-T__-sm__-por=delexp-sum |
DeepestDestUnknwon | opt-T__-sm__-r__-por=delexp-sum |
DeepestDestScan | opt-T__-sm__-c__-por=delexp-sum |
DeepestDestUnknownScan | opt-T__-sm__-c__-r__-por=delexp-sum |
DeadWeightedDest | opt-T__-sm__-scc__-por=delexp |
DeadWeigthedDestUnknown | opt-T__-sm__-scc__-r__-por=delexp |
DeadWeightedScan | opt-T__-sm__-scc__-c__-por=delexp |
DeadWeightedUnknownScan | opt-T__-sm__-scc__-c__-r__-por=delexp |
DeadDeepestDest | opt-T__-sm__-scc__-por=delexp-sum |
DeadDeepestDestUnknown | opt-T__-sm__-scc__-r__-por=delexp-sum |
DeadDeepestDestScan | opt-T__-sm__-scc__-c__-por=delexp-sum |
DeadDeepestDestUnknownScan | opt-T__-sm__-scc__-c__-r__-por=delexp-sum |
DeadColoredDestUnknown | opt-T__-sm__-scc__-r__-b__-del__-por=destination |
HighlinkWeightedDest | opt-T__-sm__-scc__-highlink__-por=delexp |
HighlinkWeightedDestUnknown | opt-T__-sm__-scc__-highlink__-r__-por=delexp |
HighlinkWeightedDestScan | opt-T__-sm__-scc__-highlink__-c__-por=delexp |
HighlinkWeightedDestUnknownScan | opt-T__-sm__-scc__-highlink__-c__-r__-por=delexp |
HighlinkDeepestDest | opt-T__-sm__-scc__-highlink__-por=delexp-sum |
HighlinkDeepestDestUnknown | opt-T__-sm__-scc__-highlink__-r__-por=delexp-sum |
HighlinkDeepestDestScan | opt-T__-sm__-scc__-highlink__-c__-por=delexp-sum |
HighlinkDeepestDestUnknownScan | opt-T__-sm__-scc__-highlink__-c__-r__-por=delexp-sum |
DeadColoredDest | opt-T__-sm__-scc__-b__-del__-por=destination |
DeadWeightedSourceKnown | opt-T__-sm__-scc__-a__-l__-por=source |
DeadWeightedSourceKnownScan | opt-T__-sm__-scc__-a__-c__-l__-por=source |
HighlinkWeightedSourceKnown | opt-T__-sm__-scc__-highlink__-a__-l__-por=source |
HighlinkWeightedSourceKnownScan | opt-T__-sm__-scc__-highlink__-a__-c__-l__-por=source |