#### APT ####

APT is a command line tool that can be used to run various analysis methods on Petri nets. It can be found at https://github.com/CvO-Theory/apt. To install APT, you can either download the pre-built jar or build it yourself by following the instructions at https://github.com/CvO-Theory/apt/blob/master/doc/obtaining.md. APT can then be used by calling:

  chmod +x apt.jar   # only once
  java -jar apt.jar

A list of modules will be displayed. For example:

  java -jar apt.jar bounded petrinet.apt         # Tests whether the Petri net is bounded
  java -jar apt.jar strongly_live petrinet.apt   # Tests whether the Petri net is live
  java -jar apt.jar strongly_live petrinet.apt t # Tests whether transition t is live
  java -jar apt.jar weakly_live petrinet.apt t   # Tests whether transition t can be fired at least once

APT can also build the reachability graph and coverability graph of a bounded Petri net:

  java -jar apt.jar reachability_graph petrinet.apt
  java -jar apt.jar coverability_graph petrinet.apt

The result is returned as a labelled transition system which can be drawn using dot. For example, the reachability graph can be visualized by opening petrinet.ps using a PDF viewer after executing:

  java -jar apt.jar reachability_graph petrinet.apt petrinet.lts
  java -jar apt.jar draw petrinet.lts petrinet.dot
  dot -Tps lamport.dot -o petrinet.ps

Note that the graph does not display markings associated to nodes.


#### LoLA ####

LoLA is a Petri nets model-checking tool. To install LoLA, download lola-2.0.tar.gz from http://home.gna.org/service-tech/lola/index.html and extract it. You will need a working C++ compiler such as GCC or Clang. On Linux and OS X, LoLA can be compiled with ./configure and make. On Windows, you might need a Unix-like environment via Cygwin.

LoLA can answer reachability queries using the flag '-f' followed by 'REACHABLE' and a formula, e.g.:

  lola petrinet.lola -f "REACHABLE DEADLOCK"             # Tests whether a dead marking can be reached
  lola petrinet.lola -f "REACHABLE (p = 1 AND q > 2)"    # Tests whether a marking M such that
                                                         #  M(p) = 1 and M(q) > 2 can be reached
  lola petrinet.lola -f "REACHABLE (p + q = 1 OR r > 2)" # Tests whether a marking M such that
                                                         #  M(p) + M(q) = 1 or M(r) > 2 can be reached
  lola petrinet.lola -f "REACHABLE FIREABLE(t)"          # Tests whether it is possible to reach a marking
                                                         #  at which t is fireable

Positive reachability queries can be witnessed by a state and a path using flags -s and -p respectively.

The tool documentation can be found at http://download.gna.org/service-tech/lola/lola.pdf.


#### PIPE ####

PIPE can be used to simulate Petri nets graphically. It can also perform basic analyses such as testing boundedness and deadlock-freedom. PIPE can build the reachability graph of a Petri net, but it sometimes display incorrect labels.

To install PIPE, download the zip file from https://sourceforge.net/projects/pipe2/ and extract it. You can start PIPE by executing launch.sh (Linux/OS X) or launch.bat (Windows), e.g., on Linux:

  chmod +x launch.sh  # only once
  ./launch.sh

The animation mode can be toggled in the top menu. Enabled transitions appear in red and can be fired by clicking on them. Transitions can also be fired randomly by pressing '5'. To test for boundedness and deadlock-freedom, click on "State Space Analysis" on the left menu.