TOOLS.MD

Tools to use with Perpetuum

A plethora of Petri-net tools is available, at least in theory. In practice, not all work well. Usually, the subset of features implemented is a less-than-perfect match.

The feature set required for Perpetuum is quite modest:

• Standard Place/Transition Nets with only one extension: Inhibitor Arcs
• We don't really use colour, though we can have many orthogonal instances of one Petri net
• We read Petri nets in the standard PNML notation
• We process Petri nets with pntools

Editors

We tried several, and found most missed certain featuers, which surpised us in light of our modest requirements. Currently, it seems that GreatSPN is the most usable of all.

• GreatSPN Editor is really pleasant to work with, and it can export files in PNML -- they actually added it to our request! GreatSPN is free for research purposes, and paid for commercial use. Its API delivers the best images, mostly thanks to snap-to-grid.
• TAPAAL is another tool we found to be useful. It focusses strongly on timing on arcs, which we don't use, but that is not a problem. It exports PNML that seems to make our conceptual model happy.
• PNeditor does not actually enable the use of inhibitor arcs, but this is on the road map so we hope it will be usable for Perpetuum soonish; its output is encoded in a non-standard manner, and it is not clear yet if it will work. Note: You may need to add the customary xmlns attribute to the <pnml/> root element.
• WOLFGANG works quite nicely, but lacks inhibitor arcs. This means that only very trivial Petri nets for Perpetuum can be edited with it.
• CPN Tools is only kept alive for educational purposes and research at the University, according to its authors; it barely runs on anything but Windows; it is written in a language that is hardly known by anyone. If anyone wants to "rescue" a useful piece of software by moving it over to a language that has stuck around, such as Haskell, then this may be a place that needs you!
• SNAKES was our first attempt at loading PNML files into a conceptual model. It is not the most direct model we could have, and it does not support inhibitor arcs. We will therefore abandon it for pntools.
• pntools with our fixes looks like the most processing approach to PNML files. There is such a vast difference in Petri net models that are assumed by tools, that just parsing a textual format is the easiest to maintain, even if it may mean that we would have to maintain our own fork of this particular tool.

If you tried other tools that we should add, please let us know. If you developed tools to surpass what is reported, we would like to hear about it.

Validation

The ability to validate Petri nets before actually running them is possible thanks to the domain of Model Checking. This is mostly an area of academic research on the edge between computer science and mathematics; its main challenge is that a brute force approach would require an enormous "state space" to represent all possible computations, and techniques are needed to provide certainties without having to resort to that.

There are already many tools to help with problems, and Petri nets have attracted many of these because of their practical uses in so many domains.

The following terms are of interest to the domain of model checking:

• LTL and CTL are "temporal logic" notations, of which CTL is the most expressive. These can be used to test random predicates that range over the time progression of a system. Think AG p to state that property p must hold for all future states, in all runtime variations, from the point in time at which it is activated.

• Standard tests (are currently assumed to) exist to exclude various problematic situations:

  • Deadlock is the situation where processes all wait for others to make the first move, and end up being stuck.
  • Livelock is the situation where processes are running around in circles, trying to do things and continually failing; they are burning computer time without actually achieving some progress. Most of us know people who function like that too...
  • Starvation describes the continued denial of resource access to processes, presumably as a result of locks; it is related to livelock.
  • Boundedness is used to determine how many tokens could at most be present in any place in the Petri net. This can be used to prove that a limited-size integer can carry all the tokens that it might encounter. It is possible to design for boundedness, which may be of interest to embedded designs.
  • Well-formedness helps to describe a Petri net in terms of symbolic notation, which bypasses the state explosion and replaces it with a mathematical derivation technique.
  • Reachability is a very general property, namely being able to reach a certain computational state from a given initial state (or "marking" as it is called in Petri nets). The concept relies heavily on the state space concept, and appears to inherit its scalability issues. If you are looking for generic validation tools, then a symbolic approach such as LTL or CTL is more likely to produce results quickly.

We have not tried any tools yet. If you tried tools that we should add, please let us know. If you developed tools to surpass what is reported, we would like to hear about it.

There are model checking contests to keep developers of model checking software at the peak of their abilities. Lovely, an academic variation of economic principles at work, without the downsides of the market model :-)

A lot is said about LoLa, but it appears to have dropped from the net. Truly a great loss.

We are more than a little interested in PNMC which is founded on libssd documented here and here. PNMC demonstrates impressive performance read more as a result of its symbolic nature, thus evading the state space explosion.