MinCoverPetri is a command-line application for the fast computation of the minimal coverability set of place/transition (P/T) Petri nets.
It can process P/T Petri nets stored in the Petri Net Markup Language (PNML)
file format defined by the standard ISO/IEC 15909 Part 2.
See pnml.org for details about this format.
It uses the monotone pruning algorithm proposed in the article:
Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning.
P.-A. Reynier and F. Servais.
In Fundamenta Informaticae, vol. 122, no. 1-2, pp. 1-30, IOS Press,2013.
DOI: 10.3233/FI-2013-781
MinCoverPetri is developed in C++ by the development team of the LIS.
MinCoverPetri is free software released under the terms of the GNU General Public License version 3 or later (GPLv3+).
Here are the precompiled executables for MinCoverpetri version 1.0.3:
The source code can be downloaded from the associated GitLab project.
The build instructions are given in the developer documentation.
The following sample PNML file representing the Petri net of Figure 7 in the reference article cited above is available: figure_7.pnml.
To test MinCoverPetri using this data, simply run:
./mincoverpetri figure_7.pnml
The help of the application is available from the command line using the -h
option, simply run:
./mincoverpetri -h
which gives:
Usage: mincoverpetri {OPTIONS} [filename] Compute the minimal coverability set of a Petri net OPTIONS: -h, --help Display this help menu -v, --version Display the version number of the executable -t, --time Display the computation time -s, --stats Display the algorithm stats -o[filename], --output=[filename] Store the computed minimal coverability set in an XML file instead of outputting it to stdout -c, --check Perform sanity check on the result Traversal: -b, --bfs Breadth-first traversal (default) -d, --dfs Depth-first traversal accelerate(): --acc Use OrderedTuples to implement accelerate() --no_acc Don't use OrderedTuples to implement accelerate() (default) is_dominated(): --isdom Use OrderedTuples to implement is_dominated() (default) --no_isdom Don't use OrderedTuples to implement is_dominated() prune(): --prune Use OrderedTuples to implement prune() (default) --no_prune Don't use OrderedTuples to implement prune() filename filename of the input P/T Petri net (PNML file) This application performs the fast computation of the minimal coverability set of Petri nets using the monotone pruning algorithm proposed in the article: | Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with | Pruning. | P.-A. Reynier and F. Servais. | In Fundamenta Informaticae, vol. 122, no. 1-2, pp. 1-30, IOS Press, 2013. | DOI: 10.3233/FI-2013-781. The input files must be place/transition (P/T) Petri nets stored in the Petri Net Markup Language (PNML) file format defined by the standard ISO/IEC 15909 Part 2. See http://www.pnml.org for details about the format. By default, the computed minimal coverability set is outputted to stdout in a text format where each line represents one of the omega-markings of the set. For each omega-marking, the line gives the values of the number of tokens in every places of the Petri net seperated by spaces, using the same order for places as the one used in the input PNML file. The letter w represents the value omega. Alternatively, using the -o option, the result can been stored in a chosen XML file. As an improvement over the original monotone pruning algorithm proposed in the paper cited above, this implementation can use a datastructure called OrderedTuples that is taylored to speed-up the computation of some key steps of the algorithm. Its use can be turned on or off for the different steps that it can handle using the corresponding options. The number of tokens is internaly represented as 8 bits signed integers and the value omega is represented as the maximal available value (ie. 127). When reading the input PNML file, any initial marking in a place that is greater than or equal to 127 is considered to be omega. If this is too limitating for your use, you can recompile the application with an appropriate type for the number of tokens (see the file marking.hpp) and an adapted limit value representing omega in the PNML file reader (see the file pnmlreader.hpp).
The developer documentation is available here.
The code of MinCoverPetri uses the following third party libraries:
The code of the tests uses the Catch framework released under the Boost Software License 1.0.
Issues can be reported in the
GitLab project or by email
to contact.dev
@lis-lab.fr
.