High-level Petri games

A framework for the synthesis of distributed systems modeled with high-level Petri games.

Contains:

• data structures for symmetric Petri games,
• data structures for the corresponding two-player games over a finite graph (cf. Acta'20):
  1. explicit version,
  2. low-level version (exploiting the symmetries of the net),
  3. high-level version (exploiting the symmetries of the net),
  4. bdd version (partially exploiting the symmetries of the net),
• solving algorithms for all the approaches,
• converter to generate a low-level Petri game from a high-level one,
• generators for example high-level Petri games (cf. ArXiv'19).

Integration:

This modules can be used as separate library and

• is integrated in: adam, adamsynt,
• contains the packages: highLevel,
• depends on the repos: libs, framework, synthesizer.

Related Publications:

• Manuel Gieseking, Ernst-Rüdiger Olderog, Nick Würdemann: Solving high-level Petri games. Acta Informatica 57(3-5): 591-626 (2020)
• Manuel Gieseking, Ernst-Rüdiger Olderog: High-Level Representation of Benchmark Families for Petri Games. CoRR abs/1904.05621 (2019)

---

How To Build

A Makefile is located in the main folder. First, pull a local copy of the dependencies with

make pull_dependencies

then build the whole framework with all the dependencies with

make

To build a single dependencies separately, use, e.g,

make tools

To delete the build files and clean-up

make clean

To also delete the files generated by the test and all temporary files use

make clean-all

Some of the algorithms depend on external libraries or tools. To locate them properly create a file in the main folder

touch ADAM.properties

and add the absolute paths of the necessary libraries or tools:

libraryFolder=<path2Repo>/dependencies/libs/
dot=dot
time=/usr/bin/time
buddy=
cudd=
cal=

You may leave some of the properties open if you don't use the corresponding libraries/tools.

Tests

To run all tests for the module, just type

ant test

For testing a specific class use for example

ant test-class -Dclass.name=uniolunisaar.adam.tests.hl.TestGGvsSGG

and for testing a specific method use for example

ant test-method -Dclass.name=uniolunisaar.adam.tests.hl.CompareApproaches -Dmethod.name=testDW