====== Petri Net plugin ======

{{page>..:core:familiarise_hint&inline}}

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

===== Capturing =====
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 {{..:core:editor_tools-place.png?nolink|[P] Place}} or transition generator {{..:core:editor_tools-transition.png?nolink|[T] Transition}} 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 {{..:core:editor_tools-connect.png?nolink|[C] Connect}} is active you can connect places and transitions with arcs by first click the source node and then the destination node. If you hold <key>Ctrl</key> 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. 

{{ invalid_connection.png?nolink |Connecting Petri net nodes}}

===== Editing =====
For editing the model activate the selection tool {{..:core:editor_tools-select.png?nolink|[S] Select}}. All the standard editing features (select, drag-and-drop, delete, copy, undo, group, etc.) work the same - see generic help on [[..:core:tool_controls#Selection controls|Selection controls]] and [[..:core:property_editor|Property editor]] for details. 

{{ editing.png?nolink |Editing Petri net nodes}}

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 {{..:core:editor_tools-text_note.png?nolink|[N] Text Note}} 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.

===== Simulation =====
For simulation of a Petri net model activate the simulation tool {{..:core:editor_tools-simulate.png?nolink|[M] Simulate}}. 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 [[..:core:tool_controls#Simulation controls]] for details.

{{ simulation.png?nolink |Simulating Petri net}}


===== Verification =====
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|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 <key>''\ Play\ ''</key> button) for playback and analysis of the reasons leading to the violation.

{{ verification.png?nolink |Verification for deadlock}}