Combining Parallel Emptiness Checks with Partial Order Reductions

Description of this page

This page presents the benchmark used in our paper.

• Section "Replay Benchmark" details how to replay the benchmark (for a Dockerfile or for a raw installation)

• The CSV (time and states) of the benchmark can be found [here]

• You can download the models we used for our experiments [here]

• You can download the fork of Spot we used for our experiments [here]

Replay Benchmark

The easiest way to install a working environement is to use Docker which is available on both Linux, MacOS and Windows. If you want to perform a raw installation, only follows the instructions [here] . Note the specials steps to run it on a MacOS.

Once you have installed Docker, only follows the following steps (for Linux and MacOS). Notice that it can takes a while.

• mkdir replay
• cd replay
• wget https://www.lrde.epita.fr/~renault/benchs/ICFEM-2019/Dockerfile
• docker build --no-cache -t icfem2019/paper3 .
• docker run -it icfem2019/paper3

Once all previous steps have been done, you should find:

• a binary file /build/spot-2.7.1.dev/tests/ltsmin/modelcheck. This is the binary file we use for our experiments.
• a directory /build/models that contains all the models we used for the benchmark

You can can then launch algorithms from the paper with NTH threads on model MODEL (model it a *.dve file):

• lw14-live: modelcheck --laarman_source --csv --selfloopize=false -P -t -p NTH -m --MODEL
• dfs-pr19-live: modelcheck --cond_dest_liveness --csv --selfloopize=false -P -t -p NTH -m --MODEL
• ws-pr19-live: modelcheck --bloemen --csv --selfloopize=false -P -t -p NTH -m --MODEL
• lw14-safe: modelcheck --laarman_safety --csv --selfloopize=false -P -t -p NTH -m --MODEL
• dfs-pr19-safe: modelcheck --cond_dest_safety --csv --selfloopize=false -P -t -p NTH -m --MODEL
• scc-pr19-safe: modelcheck --rsscc --csv --selfloopize=false -P -t -p NTH -m --MODEL
• ws-pr19-safe: modelcheck --bloemen_safety --csv --selfloopize=false -P -t -p NTH -m --MODEL

Note that removing -P will run the algorithm without partial order reductions