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 class="language-bash">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 <strong>Running experiments</strong> All models come pre-build, the experiments can be executed sequentially by the following commands: <pre><code class="language-bash">./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 class="language-bash">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. Using a 10 second timeout, a substantial portion of the experiments can be repeated within a few hours. <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 collection by <code>./extract_all.sh</code> can take a few minutes to complete. 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 (this requires that <code>gnuplot</code> is installed). 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-dependent_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 included in the paper. Notice that the conrete values given in the paper were found by manual inspection of the generated <code>.csv</code> files. We used a standard spreadsheet software, e.g. using the <code>COUNTIF</code> and <code>AVERAGEIF</code>-functions of libreoffice calc to help with this task. The raw result output is postfixed with the engine generating the given result-file. Computed update sequences can be found directly in these raw ouputs for <code>netsynth</code> while the sequences for <code>verifypn</code> are currently written to <code>/dev/null</code> as the verbose output format of <code>verifypn</code> make several of the strategies (implicitly update sequences) take up several gigabytes of space. The strategies of <code>verifypn</code> are still constructed and converted into textual representation and the overhead of doing so is included in the reported runtimes. Notice that there is no uniform output format of the update sequence provided at the moment. However, providing an API for communicating directly with <code>verifypn</code> is fairly straight forward. 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. <strong>Modifying the experiments</strong> 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.