README for ADAM University of Oldenburg and Saarland University http://www.uni-oldenburg.de/csd/adam manuel.gieseking(at)informatik.uni-oldenburg.de May 2015 ADAM: Causality-Based Synthesis of Distributed Systems ====================================================== ADAM (Analyzer of Distributed Asynchronous Models) is a synthesis tool for reactive systems with multiple independent processes. The systems are modelled as Petri games, games with one environment player and an arbitrary but bounded number of system players described as Petri nets. ADAM synthesis winning strategies of the Petri games by reducing the Petri game to a finite-graph game, solving the graph game and reconstructing the Petri game strategy from the one of the finite-graph game. ADAM is written in Java and uses JavaBDD as library for manipulating BDDs. The APT format is used as input / output format and APT itself is used for parsing / rendering the Petri games and for providing a data structure for Petri nets. For visualizing the finite-graph games, the Petri games, and their strategies, ADAM uses the DOT format of Graphviz. Table of contents: ================== 1. Dependencies 2. Installation 3. Usage 3.1. List of Modules 3.2. Executing the Modules 3.3. Creating your own Input Files 4. Contact 1. Dependencies: ================ The dependencies for using ADAM in the most comfortable way are: * Java in a version greater or equal to 7 is needed. * For saving the games and strategies as a pdf file, dot (Graphviz) has to be installed in a version >= 2.36.0. * Please stick to the documentation of JavaBDD http://javabdd.sourceforge.net/index.html, if you would like to use another library (like BuDDy, CUDD, etc.) for the BDD manipulation than the Java implementation of JavaBDD. The compiled file of such a library has then to be placed on the same level as the jar file of ADAM. The parameter for choosing a different library is applicable from the user interface. By default, ADAM uses BuDDy, if it's accessible, otherwise ADAM falls back to the Java implementation of JavaBDD. 2. Installation: ================ In order to install ADAM, just extract this file. This should create a folder named 'adam' containing the program 'adam.jar', a compiled version of the BDD library BuDDy 'libbuddy.so', this README file and a folder 'examples' containing some Petri games and their strategies. To run ADAM on Linux systems, you can execute the bash script named 'adam.sh', also placed in this folder, or directly use Java. More details on starting and using ADAM, see Section 3.2.. 3. Usage: ========= ADAM has three categories of modules. There are converters from Petri games, defined in the APT file format, to the .dot format or to a pdf document visualized by Graphviz. Then, there are generators for some example Petri games, which are also used within the benchmark suite. Finally, there are modules creating finite graph or Petri game strategies. A more detailed user guide can be found at: http://www.uni-oldenburg.de/fileadmin/user_upload/f2inform-csd/adam/UserGuide.pdf 3.1. List of Available Modules: ------------------------------- This section lists all programs ADAM provides, which can also be printed by executing 'sh adam.sh' or 'java -jar adam.jar'. List of available modules: pg2dot Converts a Petri game in APT format to a dot file. pg2pdf Converts a Petri game in APT format to a pdf file by using Graphviz (dot has to be executable). ---------------------------------------------------------------------------------------- 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_graph Creates a deadlock-avoiding winning strategy (system players) in the finite graph game of 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. win_strat_pg 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. win_strat Creates a deadlock-avoiding winning strategy (system players) in the finite graph game and the Petri game for the in APT format given Petri game if existent. Saves the strategies in the given folder as dot, and if dot is executable, as pdf. Adding '_strat_fg' for the graph and '_strat_pg' for the Petri game strategy to the filename, respectively. Also saves the input Petri game with the partition of the places within the same folder. 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. export Exports some data from ADAM. At the moment only a LaTeX export for the help dialogues is implemented. ---------------------------------------------------------------------------------------- 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. A module can be executed by typing: 'sh adam.sh ' or 'java -jar adam.jar '. This prints a help dialogue how to use this module. 3.2. Executing the Modules: --------------------------- Executing 'sh adam.sh' or 'java -jar adam.jar' prints a list of all possible modules (seen in Section 3.1.). The modules themselves can be started by executing 'sh adam.sh '. This prints a help dialogue stating the usage of this module and the available and necessary parameters. Subsequently, we give some standard calls for ADAM: * 'sh adam.sh pg2pdf -i ./folder/name.apt' : Saves in the same folder the visualisation of the in APT format given Petri game as pdf file. * 'sh adam.sh win_strat -i ./folder/name.apt' : Creates the winning strategies (finite graph and Petri game) if existent and saves them (.dot, .pdf) in the same folder as the in APT format given Petri game. Also saves the visualization of the input Petri game with the used distribution of the places, visualized by different colouring of the places. * 'sh adam.sh gen_workflow2 -m 2 -w 4 -o cw24' : This call generates the Concurrent Machines (CM) examples of the ADAM paper for two machines and four orders. It saves the resulting Petri game as APT, dot and pdf file to the given file name (cw24.apt, cw24.dot, cw24.pdf). Most of the optional parameters are self-explanatory. Thus, we only want to list some special ones. The parameter 'skip' forces ADAM to skip all tests regarding the wellformedness of the Petri game in the input file. That is, it skips the test checking if the underlying Petri net is safe. Other tests, like checking if there is only one environment token, are not yet implemented. The tests of the wellformedness of the Petri net aren't skipped. The parameter 'exp' is a flag, which forces ADAM to use an experimental algorithm. In Section 3.3. we explain the input format of the Petri games which ADAM can use. There is stated that we need to distribute the places of the Petri game in disjunct sets satisfying some properties. This experimental version is much slower, but has the ability to calculate the strategies for a subgroup of underlying Petri nets (concurrency-preserving), without the need of any distribution of the places. The parameters starting with 'lib' concern the BDD library. With them you can exchange the library used for the BDD calculation, if you have compiled C libs in the same folder as ADAM, and set some parameters for the node table and its usage. 3.3. Creating your own input files: ----------------------------------- The data format for modelling a Petri game is described here http://www.uni-oldenburg.de/fileadmin/user_upload/f2inform-csd/adam/format.pdf in detail. There is also a formal grammar for parsing Petri nets given within the document. In the following, we give a quick summary. ADAM works on safe Petri nets. If your net is not safe, you should transform it into a safe net before running ADAM by adding additional places. Another precondition is that you can use an arbitrary (bounded) number of system players, but only one environment player. Thus, you have to make sure that there is no reachable marking in which two environment places are marked at the same time. Furthermore, an environment player cannot convert into a system player or vice versa. Thus, make sure that no environment token can occupy a system place or vice versa. An input file contains of sections for places ('.places'), transitions ('.transitions') and the connections between them ('.flows'). You have to name the Petri game ('.name "my name"') and set its type ('.type LNP'). If you like to, you can give a description of the game with '.description "lorem"'. The section '.initial_marking' contains the initial marking of the Petri game. Please do not use any underscores ('_') within the names of your places while creating your own input file in the APT file format. This causes trouble during calculating the Petri game strategy. For typing a place as an environment place annotate him with '[env="true"]', all other places are automatically typed as belonging to the system players. Do the same for bad places with '[bad="true"]'. The places of the Petri game aren't just divided into environment and system places, but also into groups of places stating these are the places a given token can lie on. Thus, you can annotate the places with the '[token=]' key-value pair, where is the number of the group this place belongs to. You only have to annotate the system places. Environment places are automatically marked as group 0. Thus, the numbers annotated must start from 1 and it is not allowed to omit some natural number between 1 and the maximum number annotated. Be aware that the partition has to be disjunct in the sense that no two places in one group can be marked at the same time. ADAM has a feature to support you by annotating the places or even completely annotate the places on its own. To use this, just don't annotate any places with '[token=]' and use, for example, the 'win_strat' module. If ADAM can annotate the places on its own, you can read the annotation by the colouring of the places in the resulting pdf file of the Petri game. Otherwise, ADAM prints some invariants which should support you by following the token through the net. Here is an example input file: .name "my name" .type LNP .places env1[env="true"] bad0[token=1, bad="true"] bad1[token=2, bad="true"] good[token=2] ... env0[env="true"] .transitions t1 t2 t3 ... .flows t1: {env1} -> {env0} t1: {bad0, bad1} -> {bad0} ... .initial_marking {env1, good} For more examples, see the examples folder in './examples/'. 4. Contact: =========== We appreciate your feedback on ADAM! Please send any bugs, comments, or questions to manuel.gieseking(at)informatik.uni-oldenburg.de Thank you for using ADAM!