Alongside the main conferences there will be a tool exhibition and demonstration from Wednesday until Friday in the same room as the coffee breaks. The tool exhibition will be opened as part of the tools session of the main conference on wednesday afternoon combined with a light serving of finger-food and drinks.
The following tools will be part of the tool exhibition
Franck Pommereau, IBISC, Univ. Évry, Univ. Paris-Saclay
ecco is a Jupyter library dedicated to the formal modelling and analysis of ecosystems in an interactive and incremental way, inspired from data analysis. It’s central feature is an semi-symbolic representation of a model’s state space as an explicit graph of symbolic sets of states, linked by the transitions allowing to reach one from another. Such so called “component graphs” can be refined by splitting their nodes with respect to various properties, in particular CTL formulas. The main input language consists of if/then rules on Boolean variables with a Petri nets semantics. ecco also features tools to graphically represent models specified with this language, and to perform static analysis.
Robin Bergenthum, Jakub Kovář, FernUni in Hagen, Germany
https://www.fernuni-hagen.de/ilovepetrinets
I ❤ Petri Nets is a web tool kit implementing a neat collection of Petri net algorithms. One of the algorithms is a synthesis algorithm using Petri net regions. Just click the 🐴 button! Petri net regions will be presented at the ATAED 2022 workshop. The related paper is called A First Glimpse at Petri Net Regions by Robin and Jakub.
Ekkart Kindler, Technical University of Denmark, DTU Compute
http://www2.compute.dtu.dk/~ekki/projects/ePNK
The Petri Net Markup Language (PNML) is an XML-based interchange format for Petri nets, which is an International Standard (ISO/IEC 15909-2). The standard focuses on PNML as an interchange format for high-level Petri nets. PNML, however, is more general and allows exchanging all kinds of Petri nets. To this end, PNML introduced the concept of Petri Net Type Definitions (PNTDs).
There are many tools supporting one form of PNML or another, supporting some fixed PNTDs. The ePNK was the first tool that allowed new PNTDs to be plugged in, basically, by adding a meta-model defining its features. The ePNK is then able to load and save these new net types, and allows end-users to edit these new net types in a graphical editor. In addition, the ePNK allows developers of new net types to customize the graphical representation of their net type, and to define own extensions and applications that can be plugged in to the ePNK.
Primarily, the ePNK was meant to be a platform for easily implementing own Petri net types and own functions and applications for Petri nets. But, the ePNK comes with some additional applications for simulating high-level Petri nets and with some simple model checker for P/T-nets. Moreover, there are different simple and more sophisticated extensions for generating Java code from Petri nets.
The newest features of the ePNK are its application interface and the possibility of plugging in new Petri types nets without any programming. The ePNK application interface allows developers to implement applications for simulation and analysis of Petri nets that have a graphical user interface for visualizing the results on top of the underlying graphical presentation of the Petri net. Moreover, the application interface of the ePNK provides means for the application to interact with the end-user via this interface.
The ePNK is based on Eclipse and the Eclipse Modeling Framework (EMF), and is implemented as a collection of plugin for Eclipse.
Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan, and Francois Vernadat, CNRS
TINA (the TIme petri Net Analyzer) is a toolbox for the edition and analysis of Petri Nets and its extensions: inhibitor and read arcs; Time Petri Nets; priorities and stopwatches; and an extension of Time Petri Nets with data handling called Time Transition Systems.
Elvio Amparore, Università di Torino
https://github.com/greatspn/SOURCES
GreatSPN (GRaphical Editor and Analyzer for Timed and Stochastic Petri Nets) is a software package for the modeling, validation, and performance evaluation of distributed systems using Generalized Stochastic Petri Nets and their colored extension, Stochastic Well-formed Nets. The tool provides a friendly framework to experiment with timed Petri net based modeling techniques. It implements efficient analysis algorithms to allow its use on rather complex applications.
Elena Gómez, José Ignacio Requeno, Universidad Autónoma de Madrid, Universidad Complutense de Madrid
https://github.com/antoniogarmendia/titan
Titan is an Eclipse plug-in for Petri net Product Lines (PNPL). It allows the graphical definition of a PNPLs and the analysis of the following structural properties: state-machine, marked-graph, (extended) free-choice, and P- and T-invariants.
Titan is built on top of Eclipse platform and Eclipse Modeling Framework (EMF). Its core components are the Petri nets Sirius Editor, based on Sirius, which integrates FeatureIDE to specify Feature Models. Titan internally uses the JaCoP Java library as CP solver for invariant analysis and Sat4J solver for the analysis of state-machine, marked-graph, and (extended) free-choice.
We also include a transformation of PNPL into CPN to analyse behavioural properties.
Luis Gomes, NOVA University Lisbon, Portugal
https://gres.uninova.pt/IOPT-Tools/
The IOPT-Tools cloud-based tool-chain offers a complete set of tools supporting design automation for embedded controller’s development, benefiting from adopting a model-driven development attitude. The tools are freely available online at http://gres.uninova.pt/IOPT-Tools/. The tool-chain relies on IOPT nets (Input-Output Place-Transition nets) to describe the controller behavior, allowing an explicit representation of constraints on input and output signals and events, which is necessary for the development of controllers. The IOPT-Tools tool-chain includes tools for interactive graphical IOPT nets models editing, simulation and test (token-player, timing diagram, remote debugging), as well as a state-space generator, state-space visualization, and a query system for properties verification. The tool-chain also supports the automatic generation of execution code to be directly deployed in the controllers' implementation platforms, such as FPGA boards, as well as Arduino, Raspberry, and other Linux-based boards. Most notably, it is possible to obtain C code and VHDL code to be directly deployed into the referred boards without writing/changing a line in the generated code. The tool-chain uses the PNML format for storing the models and can import PNML models generated by other frameworks, automatically generating, if necessary, an associated graphical representation. After, it is possible to add input and output signals and events to create controller models. IOPT-Tools also supports net operations, namely net addition, allowing composition of sub-models, and net splitting, which in conjunction with the use of clock domains and dedicated communication channels support the development of distributed controllers.