Artifact for "Partial Order Reduction for Reachability Games"
| Main Authors: | Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Mũniz, Jiri Srba |
|---|---|
| Format: | info Lainnya eJournal |
| Terbitan: |
, 2019
|
| Online Access: |
https://zenodo.org/record/3574262 |
Daftar Isi:
- 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. 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". Code 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 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) and computeFinite, computeSCC, computeStaticCycles being responsible for the cycle-detection (Algorithm 1). Repeatability The repeatability-package is only available on Linux. To run the experiments as per the paper, run: ./run_POR.sh games-258 ; ./run_NPOR.sh games-258 Outputs will be generated in the "outputs" folder, and a Tex-table can be outputted by ./extract.sh games-258 Notice that we have pre-populated the outputs-folder with the results reported in the paper. The execution-scripts will NOT 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-258 The included binary is revision 258 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. 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. Changes Since the conference version (https://doi.org/10.5281/zenodo.3252104), the following changes have been made. Models: - FMS-{D,C,N} have been added - Unneeded files have been removed Data Collection - Fixed collection of measures Engine (r.258, originally r.247): - Fixed output of measures to correspond with normal interpretation (Stored markings are now reported and collected) - Fixed wrong assignment in dependency-graph - Added patch for theoretical issue with POR-reduction