The artifacts represent evaluation results of real world networks having more than 40 nodes from Network Topology Zoo. The applied topologies are listed in following table, sorted in descending order by diameter (d) and nodal degree fluctuation (σ^2)).

    Topology
    |V|
    |E|

    σ^2
    d




    Chinanet
    42
    66
    1.5
    10.52
    4


    Litnet
    43
    43
    0.98
    5.04
    4


    Cernet
    41
    58
    1.32
    5.6 |
    5 |


    Ntt
    32
    65
    1.48
    7.07
    6


    Cesnet200706
    44
    51
    1.16
    6.27
    6


    Carnet
    44
    43
    0.98
    5.48
    6


    Dfn
    50
    78
    1.77
    5.31
    6


    Telcove
    71
    70
    1.59
    9.13
    7


    Forthnet
    62
    62
    1.41
    7.72
    7


    Bellsouth
    51
    66
    1.5 |
    7.55 |
    7 |


    Garr200902
    54
    68
    1.55
    5.13
    7


    Arnes
    41
    57
    1.3 |
    4.53 |
    7 |


    BeyondTheNetwork
    53
    65
    1.48
    3.98
    7


    Uunet
    49
    84
    1.91
    7.38
    8


    Tw
    71
    115
    2.61
    | 5.58
    | 8


    Uninett
    71
    97
    2.2
    3.12
    9


    Renater2010
    43
    56
    1.27
    3.08
    9


    Surfnet
    50
    68
    1.55
    3.36
    11


    Iris
    51
    64
    1.45
    2.16
    11


    Palmetto
    45
    64
    1.45
    2.57
    12


    BtLatinAmerica
    45
    50
    1.14
    1.87
    12


    Bellcanada
    48
    64
    1.45
    2.59
    13


    Sanet
    43
    45
    1.02
    1.66
    13


    LambdaNet
    42
    46
    1.05
    1.57
    13


    HiberniaGlobal
    55
    81
    1.84
    2.72
    16


    Ntelos
    47
    58
    1.32
    1.92
    17


    RedBestel
    84
    93
    2.11
    0.85
    28


    VtlWavenet2008
    88
    92
    2.09
    0.11
    31

The evaluation results consist of three major parts:

Raw Data: Configuration and results of all simulation experiments as CSV files.

Strategy Results: Visualization of the test results for each topology.

Best Strategies: Highlighting of the best strategies across all topologies.

Therein, the "Raw Data" comprise the configuration of or simulation experiments and the simulation results. Each line stands for a single simulation run.

"Strategy Results" and "Best Strategies" accompany the results presented in the paper. Result plots in the paper are excerpts from the plots in this repository. See below for further details.

Raw Data

Both, the configuration of a run and its results correspond to one line within a CSV file in subfolder ./raw. Each file comprises the results of a replication.

raw ├── results_0.csv ├── results_1.csv ├── ... └── results_9.csv

The raw data of a CSV file is structured as follows.

    Column
    Description




    topo
    Topology name.


    peers
    Number of nodes.


    edges
    Number of links.


    p_publishers
    Proportion of nodes acting as publisher (15% - 45%).


    p_subscriber
    Proportion of nodes acting as subscriber (15% - 45%).


    n_rules
    Number of allowed rules per switch.


    distances
    Flag for consideration of geographical distances (currently not used).


    strategy
    Applied virtual tree strategy.


    distribution
    Distribution method for client (uniform, distant, nearby)


    n_cluster
    Number of simulated clusters within the topology.


    p_change
    Churn rate of clients (0% - 100%).


    pub_change
    Flag for publisher migration (currently not used).


    tree_count
    Number of virtual trees installed in the network.


    selected_subscribers
    Avg. number of subscribers addressed by a publisher


    init_cost
    Avg. number of entries of a non-optimized distribution tree (per notification)


    trees
    Avg. proportion of tree entries per notification.


    stops
    Avg. proportion of stop entries per notification.


    hops
    Avg. proportion of hop entries per notification.


    final_cost
    Aggregated proportions (trees + stops + hops).


    datetime
    Timestamp of the simulation run.

Result Charts

The simulation results are visualized in plots.md or plots.html, ordered according above topology table.

Each topology accompanys following: - Topology figures with the computed Clusters therein. - Line charts outlining the behavior of the strategies over changing Number of Flow Rules. - Bar charts outlining the strategies' performance for different Migration Scenarios.

Details of the figures and diagrams are described next.

Clusters: Visualization of exemplary groups within the topology, computed by clusters and partitions strategy. The clusters strategy assigns 60% of a network's nodes to cluster groups; the partition strategy, in contrast, assigns all nodes to groups. Both strategies are described in Sec. III.

Number of Flow Rules: Results for varying number of rules (from 5 to 40) per switch, as described in Sec. IV. The charts are organized in a 3 x 3 matrix. A row of the matrix corresponds to different proportions of subscribers per publisher (15%, 30%, and 45%); a column corresponds to different distributions of clients (uniform, nearby and distant).

Migration Scenarios: Results for different migration scenarios with a fixed number of rules (40 rules per switch), as described in Sec. V. Each bar group stands for a strategy and reflects the results of different migration rates (0%, 30%, 50%, 70%, 100%).

Best Strategies

Scatter plots in subfolder ./fluctuation visualize the most efficient strategies for different migration scenarios by considering different proportions of subscribers per publisher (15%, 30%, and 45%). The plots show the results for a fixed number of subscribers (30% per publisher) and a churn rate of 100%. The strategies therein require the fewest labels in the header stack to encode a notification distribution tree, represented by the strategy's dot size

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.

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.

Networks from SNAP (Stanford Network Analysis Platform) Network Data Sets, Jure Leskovec http://snap.stanford.edu/data/index.html email jure at cs.stanford.edu

Citation for the SNAP collection:

@misc{snapnets, author = {Jure Leskovec and Andrej Krevl}, title = {{SNAP Datasets}: {Stanford} Large Network Dataset Collection}, howpublished = {\url{http://snap.stanford.edu/data}}, month = jun, year = 2014 }

The following matrices/graphs were added to the collection in June 2010 by Tim Davis (problem id and name):

2284 SNAP/soc-Epinions1 who-trusts-whom network of Epinions.com 2285 SNAP/soc-LiveJournal1 LiveJournal social network 2286 SNAP/soc-Slashdot0811 Slashdot social network, Nov 2008 2287 SNAP/soc-Slashdot0902 Slashdot social network, Feb 2009 2288 SNAP/wiki-Vote Wikipedia who-votes-on-whom network 2289 SNAP/email-EuAll Email network from a EU research institution 2290 SNAP/email-Enron Email communication network from Enron 2291 SNAP/wiki-Talk Wikipedia talk (communication) network 2292 SNAP/cit-HepPh Arxiv High Energy Physics paper citation network 2293 SNAP/cit-HepTh Arxiv High Energy Physics paper citation network 2294 SNAP/cit-Patents Citation network among US Patents 2295 SNAP/ca-AstroPh Collaboration network of Arxiv Astro Physics 2296 SNAP/ca-CondMat Collaboration network of Arxiv Condensed Matter 2297 SNAP/ca-GrQc Collaboration network of Arxiv General Relativity 2298 SNAP/ca-HepPh Collaboration network of Arxiv High Energy Physics 2299 SNAP/ca-HepTh Collaboration network of Arxiv High Energy Physics Theory 2300 SNAP/web-BerkStan Web graph of Berkeley and Stanford 2301 SNAP/web-Google Web graph from Google 2302 SNAP/web-NotreDame Web graph of Notre Dame 2303 SNAP/web-Stanford Web graph of Stanford.edu 2304 SNAP/amazon0302 Amazon product co-purchasing network from March 2 2003 2305 SNAP/amazon0312 Amazon product co-purchasing network from March 12 2003 2306 SNAP/amazon0505 Amazon product co-purchasing network from May 5 2003 2307 SNAP/amazon0601 Amazon product co-purchasing network from June 1 2003 2308 SNAP/p2p-Gnutella04 Gnutella peer to peer network from August 4 2002 2309 SNAP/p2p-Gnutella05 Gnutella peer to peer network from August 5 2002 2310 SNAP/p2p-Gnutella06 Gnutella peer to peer network from August 6 2002 2311 SNAP/p2p-Gnutella08 Gnutella peer to peer network from August 8 2002 2312 SNAP/p2p-Gnutella09 Gnutella peer to peer network from August 9 2002 2313 SNAP/p2p-Gnutella24 Gnutella peer to peer network from August 24 2002 2314 SNAP/p2p-Gnutella25 Gnutella peer to peer network from August 25 2002 2315 SNAP/p2p-Gnutella30 Gnutella peer to peer network from August 30 2002 2316 SNAP/p2p-Gnutella31 Gnutella peer to peer network from August 31 2002 2317 SNAP/roadNet-CA Road network of California 2318 SNAP/roadNet-PA Road network of Pennsylvania 2319 SNAP/roadNet-TX Road network of Texas 2320 SNAP/as-735 733 daily instances(graphs) from November 8 1997 to January 2 2000 2321 SNAP/as-Skitter Internet topology graph, from traceroutes run daily in 2005 2322 SNAP/as-caida The CAIDA AS Relationships Datasets, from January 2004 to November 2007 2323 SNAP/Oregon-1 AS peering information inferred from Oregon route-views between March 31 and May 26 2001 2324 SNAP/Oregon-2 AS peering information inferred from Oregon route-views between March 31 and May 26 2001 2325 SNAP/soc-sign-epinions Epinions signed social network 2326 SNAP/soc-sign-Slashdot081106 Slashdot Zoo signed social network from November 6 2008 2327 SNAP/soc-sign-Slashdot090216 Slashdot Zoo signed social network from February 16 2009 2328 SNAP/soc-sign-Slashdot090221 Slashdot Zoo signed social network from February 21 2009

Then the following problems were added in July 2018. All data and metadata from the SNAP data set was imported into the SuiteSparse Matrix Collection.

2777 SNAP/CollegeMsg Messages on a Facebook-like platform at UC-Irvine 2778 SNAP/com-Amazon Amazon product network 2779 SNAP/com-DBLP DBLP collaboration network 2780 SNAP/com-Friendster Friendster online social network 2781 SNAP/com-LiveJournal LiveJournal online social network 2782 SNAP/com-Orkut Orkut online social network 2783 SNAP/com-Youtube Youtube online social network 2784 SNAP/email-Eu-core E-mail network 2785 SNAP/email-Eu-core-temporal E-mails between users at a research institution 2786 SNAP/higgs-twitter twitter messages re: Higgs boson on 4th July 2012. 2787 SNAP/loc-Brightkite Brightkite location based online social network 2788 SNAP/loc-Gowalla Gowalla location based online social network 2789 SNAP/soc-Pokec Pokec online social network 2790 SNAP/soc-sign-bitcoin-alpha Bitcoin Alpha web of trust network 2791 SNAP/soc-sign-bitcoin-otc Bitcoin OTC web of trust network 2792 SNAP/sx-askubuntu Comments, questions, and answers on Ask Ubuntu 2793 SNAP/sx-mathoverflow Comments, questions, and answers on Math Overflow 2794 SNAP/sx-stackoverflow Comments, questions, and answers on Stack Overflow 2795 SNAP/sx-superuser Comments, questions, and answers on Super User 2796 SNAP/twitter7 A collection of 476 million tweets collected between June-Dec 2009 2797 SNAP/wiki-RfA Wikipedia Requests for Adminship (with text) 2798 SNAP/wiki-talk-temporal Users editing talk pages on Wikipedia 2799 SNAP/wiki-topcats Wikipedia hyperlinks (with communities)

The following 13 graphs/networks were in the SNAP data set in July 2018 but have not yet been imported into the SuiteSparse Matrix Collection. They may be added in the future:

amazon-meta ego-Facebook ego-Gplus ego-Twitter gemsec-Deezer gemsec-Facebook ksc-time-series memetracker9 web-flickr web-Reddit web-RedditPizzaRequests wiki-Elec wiki-meta wikispeedia

The 2010 description of the SNAP data set gave these categories:

• Social networks: online social networks, edges represent interactions between people

• Communication networks: email communication networks with edges representing communication

• Citation networks: nodes represent papers, edges represent citations

• Collaboration networks: nodes represent scientists, edges represent collaborations (co-authoring a paper)

• Web graphs: nodes represent webpages and edges are hyperlinks

• Blog and Memetracker graphs: nodes represent time stamped blog posts, edges are hyperlinks [revised below]

• Amazon networks : nodes represent products and edges link commonly co-purchased products

• Internet networks : nodes represent computers and edges communication

• Road networks : nodes represent intersections and edges roads connecting the intersections

• Autonomous systems : graphs of the internet

• Signed networks : networks with positive and negative edges (friend/foe, trust/distrust)

By July 2018, the following categories had been added:

• Networks with ground-truth communities : ground-truth network communities in social and information networks

• Location-based online social networks : Social networks with geographic check-ins

• Wikipedia networks, articles, and metadata : Talk, editing, voting, and article data from Wikipedia

• Temporal networks : networks where edges have timestamps

• Twitter and Memetracker : Memetracker phrases, links and 467 million Tweets

• Online communities : Data from online communities such as Reddit and Flickr

• Online reviews : Data from online review systems such as BeerAdvocate and Amazon

https://sparse.tamu.edu/SNAP