A command-line tool for model checking asynchronous distributed systems modeled with Petri nets with transits against Flow-LTL and Flow-CTL and for the synthesis of asynchronous distributed systems modeled with Petri games with transits. It combines the tools AdamMC and AdamSYNT.
In order to compile the tool, you have to check out Adam with all submodules:
git clone --recursive [email protected]:adamtool/adam.git <foldername>
If you already have cloned the repository without the --recursive parameter, you have to first execute
git submodule update --init
to get all the code of the dependencies from the other adam repositories.
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
aigertools=
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.
A Makefile is located in the main folder. You can build the tool Adam with
make
which creates a folder deploy containing the necessary files for running Adam.
To only deploy AdamMC or AdamSYNT you can use make mc_deploy or make synt_deploy, respectively.
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
After creating the ADAM.properties file and building the tool you find all necessary files in the deploy folder. You can call the tool with
./adam <module>
``
or directly with
java -DPROPERTY_FILE=./ADAM.properties -jar adam.jar
Available modules:
pn2pdf Converts a Petri net to a pdf file by using Graphviz (dot has
to be executable).
pn2unfolding Creates the unfolding of the given net for a maximal number
of occuring transitions. Saves the unfolding and the original
net to a pdf file by using Graphviz (dot has to be
executable).
pnwt2dot Converts a Petri net with transits to a dot file.
pg2dot Converts a Petri game in APT format to a dot file.
sdn2dot Converts a Software Defined Networks topology (with an
concurrent update) to a Petri net with transits and saves
this to a dot file.
pnwt2pdf Converts a Petri net with transits to a pdf file by using
Graphviz (dot has to be executable).
pg2pdf Converts a Petri game in APT format to a pdf file by using
Graphviz (dot has to be executable).
sdn2pdf Converts a Software Defined Networks topology (with an
concurrent update) to a Petri net with transits and saves
this to a pdf file by using Graphviz (dot has to be
executable).
pg2tikz Converts a Petri game in APT format to a tikz file.
ex_win_strat Returns true if there is a deadlock-avoiding winning strategy
(system players) for the in APT format given Petri game.
win_strat Creates a deadlock-avoiding winning strategy (system players)
for the in APT format given Petri game if existent. Saves the
strategy in the given folder as dot, and if dot is
executable, as pdf.
mc_pn Modelchecking 1-bounded Petri nets with inhibitor arcs
against LTL.
mc_pnwt Modelchecking Petri nets with transits against FlowLTL or
LTL.
mc_sdn Modelchecking Software Defined Networks with concurrent
updates.
bench Just for benchmark purposes. Does not check any preconditions
of the Petri game. Tests existence of strategy, calculates
graph and Petri game strategy, saves Petri game strategy as
dot without rendering it to a pdf file.
benchSynt Just for benchmark purposes. Does not check any preconditions
of the Petri game. Tests existence of strategy, calculates
graph and Petri game strategy, saves Petri game strategy as
dot without rendering it to a pdf file.
benchTacas2018 Just for benchmark purposes. Model checks nets and formulas
for tacas 2018.
benchCAV2019 Just for benchmark purposes. Model checks nets and formulas
for CAV 2019.
benchHL2019 Just for benchmark purposes. Does not check any preconditions
of the Petri game. Tests existence of strategy, calculates
graph and Petri game strategy, saves Petri game strategy as
dot without rendering it to a pdf file.
benchRvG2019 Just for benchmark purposes. Does not check any preconditions
of the Petri game. Only prints the sizes of the low-level
graph game and the corresponding symbolic graph game.
export Exports some data of the tool.
gen_phil Generates the philosopher problem for the given number of
philosophers and saves the resulting net in the APT and dot
format and, if dot is executable, as pdf.
gen_clerks Generates the given number of clerks signing a document and
saves the resulting net in APT and dot format and, if dot is
executable, as pdf. This module generates the Document
Workflow examples of the ADAM paper.
gen_workflow Generates the workflow examples. Saves the resulting net in
APT and dot format and, if dot is executable, as pdf. This
module generates the Job Processing example of the ADAM
paper.
gen_robots Generates the self-organizing robots examples. Saves the
resulting net in APT and dot format and, if dot is
executable, as pdf. This module generates the
Self-reconfiguring Robots example of the ADAM paper.
gen_workflow2 Generates the workflow2 examples. Saves the resulting net in
APT and dot format and, if dot is executable, as pdf. This
module generates the Concurrent Machines example of the ADAM
paper.
gen_watchdog Generates the watchdog examples. Saves the resulting net in
APT and dot format and, if dot is executable, as pdf. Without
partial observation: ============================ The
enviroment set
one machine of the n machines on fire. A smoke detector
sounds the alarm. The
watchdog can asked the smoke detector where the fire started
and have to
extinguish the right machine.
With partial observation: ========================= Same
scenario as above,
but in this case the smoke detector do not reveal where the
fire started.
Thus the watchdog has to go to each machine and take a look
if it was set on
fire. Still the goal is to extinguish the right machine.
gen_securitySystem Generates the security system examples. Saves the resulting
net in APT and dot format and, if dot is executable, as pdf.
(systems = 2 it is the burglar example)
A burglar (env) decides to break into some of the
'nb_systems' locations. the intruded system has to inform the
other so that all systems can set up the alarm. No false
alarm, or not informing the other should occure.
gen_containerTerminal Generates the container terminal examples (synt2017). Saves
the resulting net in APT and dot format and, if dot is
executable, as pdf.
Two robots should repetitively transport containers to
specified container places (the parameter 'cps') while
avoiding an empty battery.
gen_emergencyBreakdown Generates TODO the security system examples. Saves the
resulting net in APT and dot format and, if dot is
executable, as pdf. (systems = 2 it is the burglar example)
A burglar (env) decides to break into some of the
'nb_systems' locations. the intruded system has to inform the
other so that all systems can set up the alarm. No false
alarm, or not informing the other should occure.
gen_mc_rm_node_update Generates a network which has an update function to detour
exactly one node (the node is chosen randomly). Saves the
resulting net in APT and, if dot is executable, as pdf.
gen_mc_redundant_flow_network Generates a network which has two ways to the output. A
update function can block one of the ways. This can be done
in correct or incorrect ways. Saves the resulting net in APT
and, if dot is executable, as pdf.
gen_topologie_zoo Generates a network from the topology given by the input
file. Saves the resulting net in APT and, if dot is
executable, as pdf.
gen_mc_smart_factory Generates a smart factory which can create 'nb_products'
products. There
are 'nb_shared_machines' machines which are shared by all
products, and
'nb_special_machines' machines which are just responsable for
the
creation of one type of product. Saves the resulting net in
APT and, if dot is executable, as pdf.
How To Develop
--------------
The submodules are all checked out with a detached head, so if you want to change s.th. in the dependencies
you can use
```make checkout_branch_all```
or
```git submodule foreach --recursive git checkout master```
to set all submodules (and the main repository) to the default branch.
Tests
-----
You can run all tests for any submodule by just navigating into the corresponding folder and typing
ant test
For testing a specific class use for example (for the module _modelchecker_)
ant test-class -Dclass.name=uniolunisaar.adam.tests.mc.circuits.TestingIngoingLTL
and for testing a specific method use for example (for the module _modelchecker_)
ant test-method -Dclass.name=uniolunisaar.adam.tests.mc.circuits.TestingModelcheckingFlowLTLParallel -Dmethod.name=exampleToolPaper
Dependencies:
-------------
This module depends on the
- the repository as submodules: [libs](https://github.com/adamtool/libs), [examples](https://github.com/adamtool/examples), [framework](https://github.com/adamtool/framework), [logics](https://github.com/adamtool/logics), [modelchecker](https://github.com/adamtool/modelchecker), [adammc](https://github.com/adamtool/adammc), [synthesizer](https://github.com/adamtool/synthesizer), [boundedSynthesis](https://github.com/adamtool/boundedsynthesis), [synthesisDistrEnv](https://github.com/adamtool/synthesisDistrEnv), [high-level](https://github.com/adamtool/high-level), [adamsynt](https://github.com/adamtool/adamsynt), [server-command-line](https://github.com/adamtool/server-command-line), [server-command-protocol](https://github.com/adamtool/server-command-line-protocol), [webinterface-backend](https://github.com/adamtool/webinterface-backend), [ui](https://github.com/adamtool/ui).
- the external tools: [McHyper](https://github.com/reactive-systems/MCHyper), [AigerTools](http://fmv.jku.at/aiger/), [ABC](https://people.eecs.berkeley.edu/~alanmi/abc/).
It uses
[McHyper](https://github.com/reactive-systems/MCHyper) for generating a circuit from a circuit for the system and an LTL formula and
[ABC](https://people.eecs.berkeley.edu/~alanmi/abc/) for model checking the resulting circuit.
Related Publications:
---------------------
For Flow-LTL
- _Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog:_
[Model Checking Data Flows in Concurrent Network Updates](https://doi.org/10.1007/978-3-030-31784-3_30). ATVA 2019: 515-533 [(Full Version)](http://arxiv.org/abs/1907.11061).
For Flow-CTL
- _Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog:_
[Model Checking Branching Properties on Petri Nets with Transits](
https://doi.org/10.1007/978-3-030-59152-6_22). ATVA 2020: 394-410 [(Full Version)](https://arxiv.org/abs/2007.07235).
AdamMC:
- _Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog:_
[AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL](https://doi.org/10.1007/978-3-030-53291-8_5). CAV (2) 2020: 64-76 [(Full Version)](https://arxiv.org/abs/2005.07130).
------------------------------------