Tools

CLP - Linear programming model checker. It uses a finite complete prefix of a Petri net and can check deadlock freeness, reachability or coverability of a marking, or performs an extended reachability analysis, i.e. checks if there exists a marking satisfying the given predicate. You can use the PUNF tool for generating a finite and complete prefix of a safe Petri net. CLP can be used both as a separate utility or as a part of the PEP tool.
PUNF - Petri net unfolder. PUNF builds a finite and complete prefix of a safe Petri net. It can be used both as a separate utility or as a part of the PEP tool. The prefixes generated by PUNF can be passed as an input to the CLP model checker.
PCOMP - A utility for computing the parallel composition of STGs.
WEASELOID - A simple tool demonstrating the detrimental impact of irreducible complexities on the performance of genetic algorithms.