A Web Interface for the Model Checking and Synthesis of Distributed Systems with Data Flows

This is the web interface for the command-line tools AdamMC and AdamSYNT.

• AdamMC is a model checker for asynchronous distributed systems modeled with Petri nets with transits and specifications given in Flow-LTL.
• AdamSYNT is a synthesizer for asynchronous distributed systems modeled with Petri games.

A deployed version runs here.

Features:

• AdamMC:
  • Modeling, visualization, and simulation of Petri nets with transits
  • Model checking of Petri nets with transits against Flow-LTL
  • Model checking of 1-bounded Petri nets against LTL with places and transitions as atomic propositions
  • Visualization and simulation of counter examples
  • Documentation: https://github.com/adamtool/webinterface/tree/master/doc/mc
  • 
• AdamSYNT:
  • Modeling, visualization, and simulation of Petri games
  • Synthesis of Petri games with one environment player and a bounded number of system players with a local safety objective
  • Interactive visualization of the corresponding two-player game to aid in finding modeling bugs
  • Visualization and simulation of the strategies
  • Documentation: https://github.com/adamtool/webinterface/tree/master/doc/synt
  • 

Dependencies:

This module depends on the

• the repository as submodules: libs, examples, framework, logics, modelchecker, synthesizer, high-level, webinterface-backend.
• the external tools: McHyper, AigerTools, ABC.

Related Publications:

• AdamWEB :
  • Manuel Gieseking, Jesko Hecking-Harbusch, Ann Yanich: A Web Interface for Petri Nets with Transits and Petri Games. TACAS (2) 2021: 381-388
• AdamMC:
  • Flow-LTL : Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog: Model Checking Data Flows in Concurrent Network Updates. ATVA 2019: 515-533 (Full Version).
  • Flow-CTL: Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog: Model Checking Branching Properties on Petri Nets with Transits. ATVA 2020: 394-410 (Full Version).
  • Tool AdamMC : Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog: AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL. CAV (2) 2020: 64-76 (Full Version).
  • AdamSYNT:
  • Theoretical Background: Bernd Finkbeiner, Ernst-Rüdiger Olderog: Petri games: Synthesis of distributed systems with causal memory. Inf. Comput. 253: 181-203 (2017)
  • Tool AdamSYNT : 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

How to Build and Run:

If you have not cloned the repository with the --recursive flag, please first use

git submodule update --init

to get all the code of the backend.

To compile the web interface please use the script

./buildWithBackend.sh

This also generates the corresponding backend jar file of Adam and integrates it. All other dependencies are downloaded by maven. This could take a while. For more details regarding the backend, e.g., how to update to a newer version, please see the ReadMe of the backend.

To start the web interface please use the script

./run.sh

and open localhost:4567 in your browser.

All temporary files created by the web interface or external tools are stored by default in folder ./tmp/ in the server's working directory. This location can be overridden using the command line flag -DADAMWEB_TEMP_DIRECTORY=/path/to/store/temporary/files/.

How to Build the External Tools:

For model checking to work, you have to have the tools abc, aiger, and mchyper, as well as GNU 'time', installed on your system and update the file ADAM.properties to have the correct paths to each one. The source code of each one is in a .tar.gz or a .zip file in this repository. The README for mchyper explains how to compile them.