Artefact for: Automatic Synthesis of Transiently Correct Network Updates via Petri Games

This is the artefact for the paper "Automatic Synthesis of Transiently Correct Network Updates via Petri Games". <strong>Requirements</strong> The setup is build for running in an <code>x86_64</code> architecture running Ubuntu 20.04 with python3 installed with the following pip3-package: <code>networkx</code>. The original experiments were conducted on AMD EPYC 7551 processors with hyperthreading disabled and limited to 25 GB of memory. <strong>Setup</strong> To create the folder structure needed for running the experiments, please start by running <code>mkdirs.sh</code>. The <code>networkx</code> library can be installed (in user space) by executing: <pre><code>pip3 install --user networkx</code></pre> All binaries are included and for repeatability we also include the source-code of the <code>verifypn</code> version used in these experiments. We use the following revision of the <code>verifypn</code> tool: https://bazaar.launchpad.net/~verifypn-cpn/verifypn/verifypn-games/revision/269 The source code of the revision 269 which is used for these experiments is located in the <code>verifypn</code> subfolder Running experiments All models come pre-build, the experiments can be executed sequentially by the following commands: <pre><code>./solve_zoo.sh # experiments on the original, none-nested zoo-topologies ./solve_nested.sh # nested zoo topology experiments ./solve_synthetic.sh # experiments on synthetic networks</code></pre> Memory, time and execution-environment can be set by setting the variables <code>MEMORY</code>, <code>TIME</code> and <code>EXECUTOR</code> variables in bash prior to execution. For instance, to limit each single execution to 60 seconds, 500 MB of memory and run using <code>sbatch</code> the following can be used <pre><code>export MEMORY=$((500*1024)) # memory in KB export TIME=60 # time in seconds export EXECUTOR=sbatch # to run on a slurm-enabled cluster ./solve_zoo.sh # experiments on the original, none-nested zoo-topologies ./solve_nested.sh # nested zoo topology experiments ./solve_synthethic.sh # experiments on synthetic networks</code></pre> It will take more than 24 hours to complete the entire experimental setup with a one-hour timeout on a single core. <strong>Data collection</strong> After the execution, data can be collected using the <code>./extract_all.sh</code> script which will generate <code>.csv</code> files for each subfigure of Figure 8 of the paper. The data reported in the <code>.csv</code>-files is in milliseconds for time and kilobytes for memory. Notice that the data-folder is pre-populated with the results from the paper - these will be overwritten by a subsequent execution. These <code>.csv</code> files can be turned into the graphs of the paper using the scripts provided in the <code>plot</code>-subfolder. From here, plots can be generated by running <code>plot_all.sh</code> for time-plots, or <code>plot_all_mem.sh</code> for memory-plots (not shown in paper). Notice that Figure 9 from the paper corresponds to (a): <code>cactus-disjoint.pdf</code>, (b) <code>cactus-dependent_single.pdf</code>, (c) <code>cactus-dependen_10.pdf</code>, (d) <code>cactus-dependent_5.pdf</code>, (e) <code>shared-single.pdf</code> and (f) <code>cactus-nested.pdf</code>. The remaining plots are from experiments not presented in the paper as they show similar trends to those incloded in the paper. The raw results can be found in <code>data/{synthethic,nested,zoo}_results</code> and the corresponding strategy generated by <code>verifypn</code> can be found in <code>data/{synthethic,nested,zoo}_strategy</code>. The raw result output is postfixed with the engine generating the given result-file. Notice that <code>netsynth</code> provides solutions directly in the output located in the <code>data/{synthethic,nested,zoo}_results/*.netsynth</code> files. Lastly, consistency in the answers between <code>netsynth</code> and <code>verifypn</code> on the "nested" experiment can be checked by the <code>consistent.sh</code> script. Modifying the experiments Several parts of the experiments can be modified by changing the values of the generators. Notice that the artefact comes pre-loaded with a pre-generated set of models - so this step is optional. The <code>Generate_Synthetic.py</code> facilitates the generation of all the synthetic models of the paper. This script will fill the <code>data/synthethic_json</code> folder. The <code>Generate_Nested.py</code> constructs nested topologies from an existing set of <code>.gml</code>-files. Specifically it iterates through the contents of <code>data/gml/</code> and randomly "subnets" networks into each other. The output is a new set of <code>.gml</code> files located in <code>data/nested_gml/</code>. The <code>Generate_Json.py</code> reads the folders <code>data/gml/</code> and <code>data/nested_gml/</code> and creates (by random) a set of synthesis-problems based on the input topologies. By default the "source" and "target"-routes generated are appended up to <code>n</code> times to make harder instances. The value <code>n</code> ranges from 1-5. Notice that <code>Generate_Json.py</code> can take more than a day to execute, given the rather brute-force nature of the optimization-problem solved for generating the random examples. The results of <code>Generate_Json.py</code> is placed in <code>data/{zoo,nested}_json</code>. Notice also that it is not guaranteed that a "sane" update synthesis problem is generated for all input <code>.gml</code>-files . To be a "sane" update synthesis problem, at least one waypoint must exist. Several attempts are made by the <code>Generate_Json.py</code> script to randomly generate such sane problems, however, this process can fail. The last step is translation. The <code>Translate.py</code> script converts json-files into both <code>.pnml</code>-files for <code>verifypn</code> and <code>.ltl</code>-files for <code>netsynth</code>. The results are placed in the <code>data/{synthethic,zoo,nested}_{ltl,pn}/</code> folders.