A framework for the synthesis of distributed systems modeled with Petri games with transits. This module is the model and controller part of AdamSYNT.
- data structures for
- Petri games (cf. Inf. Comp. 17)
- the corresponding two-player game (cf. Inf. Comp. 17)
- Petri games with transits
- a general structure for easily integrating solvers for Petri games with transits
- heuristics to partition the places of a Petri net in disjunctive sets regarding their occurrence in reachable markings
- algorithms for solving Petri games with one environment and an arbitrary number of system players with a local safety objective by using BDDs (cf. CAV'15, SYNT@CAV'17)
- renderer for Petri games with transits and the two-player game into the dot format
- parser for Petri nets games with transits
- generators for examples of Petri games with transits
This modules can be used as separate library and
- is integrated in: adam
- contains the packages: petrigames, bddapproach, mtbddapproach,
- depends on the repos: libs, framework.
The theoretical background for Petri games and the decision procedure for one environment and a bounded number of system players:
- Bernd Finkbeiner, Ernst-Rüdiger Olderog: Petri games: Synthesis of distributed systems with causal memory. Inf. Comput. 253: 181-203 (2017)
The practical parts and the BDD approach for the algorithms to solve Petri games with one environment and a bounded number of system players:
- Bernd Finkbeiner, Manuel Gieseking, Ernst-Rüdiger Olderog:
Adam: Causality-Based Synthesis of Distributed Systems. CAV (1) 2015: 433-439
- Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog: Symbolic vs. Bounded Synthesis for Petri Games. SYNT@CAV 2017: 23-43
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.
Both modules contain tests. You can run the tests by entering the corresponding folder, e.g.,
cd petriGames
and run all tests for the module by just typing
ant test
For testing a specific class in the package bddapproach (in ./symbolicalgorithms/bddapproach/ ) use for example
ant test-class -Dclass.name=uniolunisaar.adam.tests.synthesis.symbolic.bddapproach.distrsys.graph.TestStepwiseGraphBuilder
and for testing a specific method use for example
ant test-method -Dclass.name=uniolunisaar.adam.tests.synthesis.symbolic.bddapproach.distrsys.safety.TestingSomeFiles -Dmethod.name=testBurglar