Petri Net plugin

This plugin is intended for capturing, simulation and verification of Petri net models.

In order to create a Petri net work choose File→Create work… menu item and in the New work dialogue select Petri Net as the model type.

A Petri net model can be captured by dropping places and transitions onto the editor panel and connecting them with the producing and consuming arcs.

With the place generator or transition generator activated you can create a series of places or transition respectively, by clicking the editor panel in the position you want a new node to appear.

When the connection tool is active you can connect places and transitions with arcs by first click the source node and then the destination node. If you hold Ctrl then the destination node becomes a source for the next arc making it easier to form a sequence of connected nodes. Note that places can only be connected to transitions and transitions can only be connected to places. If you attempt to connect two nodes of the same type, then a warning will be issued that connections is not valid.

For editing the model activate the selection tool . All the standard editing features (select, drag-and-drop, delete, copy, undo, group, etc.) work the same - see generic help on Selection controls and Property editor for details.

The only new editing feature is double clicking on a place:

• Double-click on an empty place to mark it with a token.
• Double-click a place marked with a token to remove the token.
• If a place has more than one token then double-clicking does not have any effect.

Similar to all the other plugins, textual comments can be created by activating the tool and clicking the editor panel in the position you want to put the text. Double-click on the note box to edit its text label in-place or do it through the property editor panel when the note is selected.

For simulation of a Petri net model activate the simulation tool . The enabled transitions are highlighted and can be fired by clicking them. The Tool controls panel of the simulation tool provides the means for analysis and navigation through the simulation trace, see generic help on Simulation controls for details.

A Petri net can be verified for deadlocks via Verification→Deadlock [MPSat] menu. Custom properties can be verified by formulating a reachability analysis problem in Reach language. This is done a specialised MPSat configuration window accessible via Verification→Custom properties [MPSat]… menu.

If the verified property is not satisfied, then a trace (or several traces) leading to the violation is reported. The trace can be passed to the the simulation tool (by clicking the  Play  button) for playback and analysis of the reasons leading to the violation.