Artifact for "Partial Order Reduction for Reachability Games"
Creators: name: Bønneland, Frederik Meyer
name: Jensen, Peter Gjøl
name: Larsen, Kim Guldstrand
name: Mũniz, Marco
name: Jiri Srba
Publisher: name: Zenodo
Year: 2020

description: An updated artifact for the paper "Partial Order Reduction for Reachability Games", accepted at CONCUR'19 with the corrections, models and modifications added for the later LMCS journal version.<br> <br> The source-code for the engine is found in the "verifypn-games.zip" file while the experiments and scripts to execute those are found in "reproducability.zip".<br> <br> <strong>Code</strong><br> The implementation reuses the general framework of partial order reduction applied in https://doi.org/10.1016/j.jlamp.2018.09.002 The core reduction algorithm is implemented in a (semantically equivalent and) efficient manner in PetriEngine/ReducingSuccessorGenerator.cpp<br> Here the "prepare"-method implements the equivalent of the "St"-function of the paper (Algorithm 2), the "closure"-method implements the "Saturate"-function (Algorithm 3). <strong>Repeatability</strong><br> The repeatability-package is only available on Linux. To run the experiments as per the paper, run: ./run_POR.sh games-260 ; ./run_NPOR.sh games-260 Outputs will be generated in the "outputs" folder, and a Tex-table can be outputted by ./extract.sh games-260 Notice that we have pre-populated the outputs-folder with the results reported in the paper.<br> The execution-scripts will <strong>NOT</strong> overwrite existing output files, and thus the outputs folder should be purged prior to a re-run of the experiments. To use a different executor (for instance sbatch on a slurm-enabled cluster for concurrent execution of the experiments), the run-commands can be prefixed as such: EXECUTOR=sbatch ./run_POR.sh games-260 The included binary is revision 260 of https://code.launchpad.net/~verifypn-cpn/verifypn/verifypn-games To limit the memory-consumption of each experiment, modify "run.sh" and change the "ulimit" memory-bound to the desired value.<br> A "timeout"-command can also be added here to introduce a time-limit of the execution (we utilize slurm for this purpose). Notice that we measure and report the computation time excluding parsing; i.e. we report the fix-point computation-time as computed by the engine directly. <strong>Changes</strong> Since the conference version (https://doi.org/10.5281/zenodo.3252104), the following changes have been made. Models:<br> - FMS-{D,C,N} have been added<br> - Unneeded files have been removed Data Collection<br> - Fixed collection of measures Engine (r.260, originally r.247):<br> - Fixed uninitialized variable, leading to non-deterministic heuristic of stubborn set<br> - Removed redundant cycle-detection<br> - Fixed output of measures to correspond with normal interpretation (Stored markings are now reported and collected)<br> - Fixed wrong assignment in dependency-graph<br> - Added patch for theoretical issue with POR-reduction The prepopulated results have been recomputed since https://zenodo.org/record/3574262 as the original prepopulated results were conducted, in few and isolated experiments, on different models than those included in the package.