Reproducibility package for the paper Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking accepted for VMCAI'22. Contains scripts, 64-bit Linux binaries, and the dataset used to run the experiments detailed in the paper, a source code snapshot used to compile those binaries, as well as scripts for processing the results into the tables seen in the paper. The file README.md contains details on running the various parts of the artifacts, assuming a Linux environment.

Reproducibility package for the paper Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking accepted for VMCAI'22. Contains scripts, 64-bit Linux binaries, and the dataset used to run the experiments detailed in the paper, a source code snapshot used to compile those binaries, as well as scripts for processing the results into the tables seen in the paper. The file README.md contains details on running the various parts of the artifacts, assuming a Linux environment.

This is the artefact for the paper "Automatic Synthesis of Transiently Correct Network Updates via Petri Games". Requirements The setup is build for running in an x86_64 architecture running Ubuntu 20.04 with python3 installed with the following pip3-package: networkx. The original experiments were conducted on AMD EPYC 7551 processors with hyperthreading disabled and limited to 25 GB of memory. Setup To create the folder structure needed for running the experiments, please start by running mkdirs.sh. The networkx library can be installed (in user space) by executing:

pip3 install --user networkx

All binaries are included and for repeatability we also include the source-code of the verifypn version used in these experiments. We use the following revision of the verifypn 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 verifypn subfolder Running experiments All models come pre-build, the experiments can be executed sequentially by the following commands:

./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

Memory, time and execution-environment can be set by setting the variables MEMORY, TIME and EXECUTOR variables in bash prior to execution. For instance, to limit each single execution to 60 seconds, 500 MB of memory and run using sbatch the following can be used

export MEMORY=$((5001024)) # 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

It will take more than 24 hours to complete the entire experimental setup with a one-hour timeout on a single core. Data collection After the execution, data can be collected using the ./extract_all.sh script which will generate .csv files for each subfigure of Figure 8 of the paper. The data reported in the .csv-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 .csv files can be turned into the graphs of the paper using the scripts provided in the plot-subfolder. From here, plots can be generated by running plot_all.sh for time-plots, or plot_all_mem.sh for memory-plots (not shown in paper). Notice that Figure 9 from the paper corresponds to (a): cactus-disjoint.pdf, (b) cactus-dependent_single.pdf, (c) cactus-dependen_10.pdf, (d) cactus-dependent_5.pdf, (e) shared-single.pdf and (f) cactus-nested.pdf. 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 data/{synthethic,nested,zoo}_results and the corresponding strategy generated by verifypn can be found in data/{synthethic,nested,zoo}_strategy. The raw result output is postfixed with the engine generating the given result-file. Notice that netsynth provides solutions directly in the output located in the data/{synthethic,nested,zoo}_results/.netsynth files. Lastly, consistency in the answers between netsynth and verifypn on the "nested" experiment can be checked by the consistent.sh 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 Generate_Synthetic.py facilitates the generation of all the synthetic models of the paper. This script will fill the data/synthethic_json folder. The Generate_Nested.py constructs nested topologies from an existing set of .gml-files. Specifically it iterates through the contents of data/gml/ and randomly "subnets" networks into each other. The output is a new set of .gml files located in data/nested_gml/. The Generate_Json.py reads the folders data/gml/ and data/nested_gml/ 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 n times to make harder instances. The value n ranges from 1-5. Notice that Generate_Json.py 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 Generate_Json.py is placed in data/{zoo,nested}json. Notice also that it is not guaranteed that a "sane" update synthesis problem is generated for all input .gml-files . To be a "sane" update synthesis problem, at least one waypoint must exist. Several attempts are made by the Generate_Json.py script to randomly generate such sane problems, however, this process can fail. The last step is translation. The Translate.py script converts json-files into both .pnml-files for verifypn and .ltl-files for netsynth. The results are placed in the data/{synthethic,zoo,nested}{ltl,pn}/ folders.

This is the artefact for the paper "Automatic Synthesis of Transiently Correct Network Updates via Petri Games". Requirements The setup is build for running in an x86_64 architecture running Ubuntu 20.04 with python3 installed with the following pip3-package: networkx. The original experiments were conducted on AMD EPYC 7551 processors with hyperthreading disabled and limited to 25 GB of memory. Setup To create the folder structure needed for running the experiments, please start by running mkdirs.sh. The networkx library can be installed (in user space) by executing:

pip3 install --user networkx

All binaries are included and for repeatability we also include the source-code of the verifypn version used in these experiments. We use the following revision of the verifypn 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 verifypn subfolder Running experiments All models come pre-build, the experiments can be executed sequentially by the following commands:

./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

Memory, time and execution-environment can be set by setting the variables MEMORY, TIME and EXECUTOR variables in bash prior to execution. For instance, to limit each single execution to 60 seconds, 500 MB of memory and run using sbatch the following can be used

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

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. Data collection After the execution, data can be collected using the ./extract_all.sh script which will generate .csv files for each subfigure of Figure 8 of the paper. The data reported in the .csv-files is in milliseconds for time and kilobytes for memory. Notice that the data collection by ./extract_all.sh 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 .csv files can be turned into the graphs of the paper using the scripts provided in the plot-subfolder (this requires that gnuplot is installed). From here, plots can be generated by running plot_all.sh for time-plots, or plot_all_mem.sh for memory-plots (not shown in paper). Notice that Figure 9 from the paper corresponds to (a): cactus-disjoint.pdf, (b) cactus-dependent_single.pdf, (c) cactus-dependent_10.pdf, (d) cactus-dependent_5.pdf, (e) shared-single.pdf and (f) cactus-nested.pdf. 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 .csv files. We used a standard spreadsheet software, e.g. using the COUNTIF and AVERAGEIF-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 netsynth while the sequences for verifypn are currently written to /dev/null as the verbose output format of verifypn make several of the strategies (implicitly update sequences) take up several gigabytes of space. The strategies of verifypn 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 verifypn is fairly straight forward. Lastly, consistency in the answers between netsynth and verifypn on the "nested" experiment can be checked by the consistent.sh 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 Generate_Synthetic.py facilitates the generation of all the synthetic models of the paper. This script will fill the data/synthethic_json folder. The Generate_Nested.py constructs nested topologies from an existing set of .gml-files. Specifically it iterates through the contents of data/gml/ and randomly "subnets" networks into each other. The output is a new set of .gml files located in data/nested_gml/. The Generate_Json.py reads the folders data/gml/ and data/nested_gml/ 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 n times to make harder instances. The value n ranges from 1-5. Notice that Generate_Json.py 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 Generate_Json.py is placed in data/{zoo,nested}json. Notice also that it is not guaranteed that a "sane" update synthesis problem is generated for all input .gml-files . To be a "sane" update synthesis problem, at least one waypoint must exist. Several attempts are made by the Generate_Json.py script to randomly generate such sane problems, however, this process can fail. The last step is translation. The Translate.py script converts json-files into both .pnml-files for verifypn and .ltl-files for netsynth. The results are placed in the data/{synthethic,zoo,nested}{ltl,pn}/ folders.

This is the artefact for the paper "Automatic Synthesis of Transiently Correct Network Updates via Petri Games". Requirements The setup is build for running in an x86_64 architecture running Ubuntu 20.04 with python3 installed with the following pip3-package: networkx. The original experiments were conducted on AMD EPYC 7551 processors with hyperthreading disabled and limited to 25 GB of memory. Setup To create the folder structure needed for running the experiments, please start by running mkdirs.sh. The networkx library can be installed (in user space) by executing:

pip3 install --user networkx

All binaries are included and for repeatability we also include the source-code of the verifypn version used in these experiments. We use the following revision of the verifypn 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 verifypn subfolder Running experiments All models come pre-build, the experiments can be executed sequentially by the following commands:

./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

Memory, time and execution-environment can be set by setting the variables MEMORY, TIME and EXECUTOR variables in bash prior to execution. For instance, to limit each single execution to 60 seconds, 500 MB of memory and run using sbatch the following can be used

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

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. Data collection After the execution, data can be collected using the ./extract_all.sh script which will generate .csv files for each subfigure of Figure 8 of the paper. The data reported in the .csv-files is in milliseconds for time and kilobytes for memory. Notice that the data collection by ./extract_all.sh 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 .csv files can be turned into the graphs of the paper using the scripts provided in the plot-subfolder (this requires that gnuplot is installed). From here, plots can be generated by running plot_all.sh for time-plots, or plot_all_mem.sh for memory-plots (not shown in paper). Notice that Figure 9 from the paper corresponds to (a): cactus-disjoint.pdf, (b) cactus-dependent_single.pdf, (c) cactus-dependent_10.pdf, (d) cactus-dependent_5.pdf, (e) shared-single.pdf and (f) cactus-nested.pdf. 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 .csv files. We used a standard spreadsheet software, e.g. using the COUNTIF and AVERAGEIF-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 netsynth while the sequences for verifypn are currently written to /dev/null as the verbose output format of verifypn make several of the strategies (implicitly update sequences) take up several gigabytes of space. The strategies of verifypn 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 verifypn is fairly straight forward. Lastly, consistency in the answers between netsynth and verifypn on the "nested" experiment can be checked by the consistent.sh 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 Generate_Synthetic.py facilitates the generation of all the synthetic models of the paper. This script will fill the data/synthethic_json folder. The Generate_Nested.py constructs nested topologies from an existing set of .gml-files. Specifically it iterates through the contents of data/gml/ and randomly "subnets" networks into each other. The output is a new set of .gml files located in data/nested_gml/. The Generate_Json.py reads the folders data/gml/ and data/nested_gml/ 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 n times to make harder instances. The value n ranges from 1-5. Notice that Generate_Json.py 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 Generate_Json.py is placed in data/{zoo,nested}json. Notice also that it is not guaranteed that a "sane" update synthesis problem is generated for all input .gml-files . To be a "sane" update synthesis problem, at least one waypoint must exist. Several attempts are made by the Generate_Json.py script to randomly generate such sane problems, however, this process can fail. The last step is translation. The Translate.py script converts json-files into both .pnml-files for verifypn and .ltl-files for netsynth. The results are placed in the data/{synthethic,zoo,nested}{ltl,pn}/ folders.

Prerequisite The conda package manager for python Setup Navigate to ./Platoon and execute following commands

conda env create -n your_env_name -f conda_env.yml conda activate your_env_name pip install -r pip_req.txt

Usage:
Creating an Agent (platoon.py)
First you need to create an environment

gym.make(ENV_NAME, rendermode, numcars, startdist, startspeed, mindist, maxdist, accsteps, rendermode, seed, shield, shield_file)

All of these key word arguments already have default values and can be changed if needed.
rendermode can be set to None, Minimal, Console, Viewer or Console_Viewer. The weigths of the agent get saved in ./Platoon/weigths
and checkpoints can be found in ./Platoon/weigths/checkpoints.
The checkpoints can be disabled by not using a callback for the dqnAgent.

All the agents have been trained by taking some amount of steps, saving the weights, reloading the weights and then start the training again.
The first training session should be between 60.000 and 80.000 steps. (here the load_weigths is not needed)
After that the session can be a larger amount of steps but should not be unreasonably large (80.000 - 200.000).
Larger amount of cars need more training sessions in order to achieve a good performance. Using an Agent (test_agent.py)
the gym should be initialized with the values numcars, mindist, maxdist, accsteps the agent has been trained on
startspeed, startdis can be changed, but might create situations where the agent has no way of preventing a crash
rendermode can be set to None, Minimal, Console, Viewer or Console_Viewer the model, memory and policy need to be set according to the agent
now the weigths of the agent can be loaded

dqn.load_weights('weights/agent_name')

Pre-trained agents from 2 - 10 cars can be found in ./Platoon/weigths Environment
the environment can be found in ./Platoon/custom_gym/envs/custom_env_dir and consists of platooning_env.py and car.py Safestragey Creating a Safe Strategy open UPPAAL and load the ./safe_stragety/cruise.xml file edit it however you want, use these two commands in the Verifier in order to save the strategy

strategy safe = control: A[] distance > 5 saveStrategy("filename.txt", safe)

Parser Usage In safe_strategy/

python parser.py -create in_file_name out_file_name python parser.py -test file_name

Using the safestrategy

gym.make(ENV_NAME, rendermode, numcars, startdist, startspeed, mindist, maxdist, accsteps, rendermode, seed, shield, shield_file)

Enable the shield by setting shield to True
shield_file should be the path to the previously created safestrategy

Prerequisite The conda package manager for python Setup Navigate to ./Platoon and execute following commands

conda env create -n your_env_name -f conda_env.yml conda activate your_env_name pip install -r pip_req.txt

Usage:
Creating an Agent (platoon.py)
First you need to create an environment

gym.make(ENV_NAME, rendermode, numcars, startdist, startspeed, mindist, maxdist, accsteps, rendermode, seed, shield, shield_file)

All of these key word arguments already have default values and can be changed if needed.
rendermode can be set to None, Minimal, Console, Viewer or Console_Viewer. The weigths of the agent get saved in ./Platoon/weigths
and checkpoints can be found in ./Platoon/weigths/checkpoints.
The checkpoints can be disabled by not using a callback for the dqnAgent.

All the agents have been trained by taking some amount of steps, saving the weights, reloading the weights and then start the training again.
The first training session should be between 60.000 and 80.000 steps. (here the load_weigths is not needed)
After that the session can be a larger amount of steps but should not be unreasonably large (80.000 - 200.000).
Larger amount of cars need more training sessions in order to achieve a good performance. Using an Agent (test_agent.py)
the gym should be initialized with the values numcars, mindist, maxdist, accsteps the agent has been trained on
startspeed, startdis can be changed, but might create situations where the agent has no way of preventing a crash
rendermode can be set to None, Minimal, Console, Viewer or Console_Viewer the model, memory and policy need to be set according to the agent
now the weigths of the agent can be loaded

dqn.load_weights('weights/agent_name')

Pre-trained agents from 2 - 10 cars can be found in ./Platoon/weigths Environment
the environment can be found in ./Platoon/custom_gym/envs/custom_env_dir and consists of platooning_env.py and car.py Safestragey Creating a Safe Strategy open UPPAAL and load the ./safe_stragety/cruise.xml file edit it however you want, use these two commands in the Verifier in order to save the strategy

strategy safe = control: A[] distance > 5 saveStrategy("filename.txt", safe)

Parser Usage In safe_strategy/

python parser.py -create in_file_name out_file_name python parser.py -test file_name

Using the safestrategy

gym.make(ENV_NAME, rendermode, numcars, startdist, startspeed, mindist, maxdist, accsteps, rendermode, seed, shield, shield_file)

Enable the shield by setting shield to True
shield_file should be the path to the previously created safestrategy

Prerequisites: A 2020 linux distribution on an x86_64 platform python3 installation with os, sys, json and statistics packages installed for computation of timing statistics pdflatex for visualization of reachability matrices Contents: The bin folder contains the pre-compiled binaries for our tool and the backend verifier for pushdown-systems, moped. The sources folder contains a snapshot of source-code used for producing the tool binary, namely AalWiNes, also found at https://github.com/DEIS-Tools/AalWiNes in release v0.92.J (337f1e4c44f8bce2060897b88e706f7ceca38319) PDAAAL, used for pushdown-system manipulation, also found at https://github.com/DEIS-Tools/PDAAAL in release v0.2.2.J (ed1e7fbb4cacd6ffb240a514cfe8472f83d91f60) The nested folder contains scripts and models for reproducing the results of Table IV The nn-net folder contains scripts and models for constructing reachability-matrices (Table V to Table XII) and operator specific queries Within the nn-net folder, you also find a mapping from alphabetical naming of NORDUnet routers in the paper to numericals (nn-net/index-alpha-map.txt) P-Rex vs HSA (Table IV) We here re-use the HSA-timings computed in https://doi.org/10.1145/3281411.3281432 The timings for our tool can be obtained by the following commands

cd nested ./compute_nested.sh | grep "#"

which should compute a sequence of lines in the terminal equal to

### Running N0 with aalwines ### Memory: 27064 Kb Time 0.02 seconds ### Running N1 with aalwines ### Memory: 37404 Kb Time 0.03 seconds ### Running N2 with aalwines ### Memory: 47704 Kb Time 0.03 seconds ### Running N3 with aalwines ### Memory: 57784 Kb Time 0.04 seconds ### Running N4 with aalwines ### Memory: 68368 Kb Time 0.04 seconds ### Running N5 with aalwines ### Memory: 78468 Kb Time 0.05 seconds ### Running N6 with aalwines ### Memory: 88980 Kb Time 0.06 seconds 

Operator Queries The experiments on the queries of the operators can be computed via the commands

cd nn-net ./compute_operator.sh 

which should complete less than 10 minutes. The traces and timings are outputted directly to the terminal. Reachability Matrices (Table V to Table XII) This package folder comes pre-populated with the raw computation results. Notice that the compute_grid.sh command will invalidate these results. To compute the full set of reachability tables, you can use the following commands

cd nn-net ./make_queries.sh ./compute_grid.sh

Notice, however, that this computation in total takes more than two days to complete on a single core. To reduce the size of the experiment, clear the contents of the query sub-folder an modify the make_queries.sh file by commenting out unwanted queries and parameter-combinations. To obtain a matrix, the command

./make_grid.sh aalwines IP IP 0 > ip_ip.tex pdflatex ip_ip.tex

which generated the IP IP matrix with 0 failures.
For the second argument, the following values are supported IP, MPLS while the third argument can also attain the value of ANY. The fourth argument gives the number of link failures. Timing information for the reachability-matrices can be obtained by

python3 ./timing_stats.py aalwines 3 IP_IP_UNDER_0

where the third argument determines the reduction-type used, and the fourth argument gives the specific query and engine mode used. In the given example we attain the statistics for reduction-mode 3 for the IP-IP matrix using under-approximation on zero link-failures. The pre-reduction and post-reduction elements of the output give the size of the constructed pushdown system before (and after) reduction respectively.

Prerequisites: A 2020 linux distribution on an x86_64 platform python3 installation with os, sys, json and statistics packages installed for computation of timing statistics pdflatex for visualization of reachability matrices Contents: The bin folder contains the pre-compiled binaries for our tool and the backend verifier for pushdown-systems, moped. The sources folder contains a snapshot of source-code used for producing the tool binary, namely AalWiNes, also found at https://github.com/DEIS-Tools/AalWiNes in release v0.92.J (337f1e4c44f8bce2060897b88e706f7ceca38319) PDAAAL, used for pushdown-system manipulation, also found at https://github.com/DEIS-Tools/PDAAAL in release v0.2.2.J (ed1e7fbb4cacd6ffb240a514cfe8472f83d91f60) The nested folder contains scripts and models for reproducing the results of Table IV The nn-net folder contains scripts and models for constructing reachability-matrices (Table V to Table XII) and operator specific queries Within the nn-net folder, you also find a mapping from alphabetical naming of NORDUnet routers in the paper to numericals (nn-net/index-alpha-map.txt) P-Rex vs HSA (Table IV) We here re-use the HSA-timings computed in https://doi.org/10.1145/3281411.3281432 The timings for our tool can be obtained by the following commands

cd nested ./compute_nested.sh | grep "#"

which should compute a sequence of lines in the terminal equal to

### Running N0 with aalwines ### Memory: 27064 Kb Time 0.02 seconds ### Running N1 with aalwines ### Memory: 37404 Kb Time 0.03 seconds ### Running N2 with aalwines ### Memory: 47704 Kb Time 0.03 seconds ### Running N3 with aalwines ### Memory: 57784 Kb Time 0.04 seconds ### Running N4 with aalwines ### Memory: 68368 Kb Time 0.04 seconds ### Running N5 with aalwines ### Memory: 78468 Kb Time 0.05 seconds ### Running N6 with aalwines ### Memory: 88980 Kb Time 0.06 seconds 

Operator Queries The experiments on the queries of the operators can be computed via the commands

cd nn-net ./compute_operator.sh 

which should complete less than 10 minutes. The traces and timings are outputted directly to the terminal. Reachability Matrices (Table V to Table XII) This package folder comes pre-populated with the raw computation results. Notice that the compute_grid.sh command will invalidate these results. To compute the full set of reachability tables, you can use the following commands

cd nn-net ./make_queries.sh ./compute_grid.sh

Notice, however, that this computation in total takes more than two days to complete on a single core. To reduce the size of the experiment, clear the contents of the query sub-folder an modify the make_queries.sh file by commenting out unwanted queries and parameter-combinations. To obtain a matrix, the command

./make_grid.sh aalwines IP IP 0 > ip_ip.tex pdflatex ip_ip.tex

which generated the IP IP matrix with 0 failures.
For the second argument, the following values are supported IP, MPLS while the third argument can also attain the value of ANY. The fourth argument gives the number of link failures. Timing information for the reachability-matrices can be obtained by

python3 ./timing_stats.py aalwines 3 IP_IP_UNDER_0

where the third argument determines the reduction-type used, and the fourth argument gives the specific query and engine mode used. In the given example we attain the statistics for reduction-mode 3 for the IP-IP matrix using under-approximation on zero link-failures. The pre-reduction and post-reduction elements of the output give the size of the constructed pushdown system before (and after) reduction respectively.