MinCoverPetri

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 LIF.

License

MinCoverPetri is free software released under the terms of the GNU General Public License version 3 or later (GPLv3+).

Download

Precompiled executables

Here are the precompiled executables for MinCoverpetri version 1.0.0:

Source code

The source code can be downloaded from the associated GitLab project.

The build instructions are given in the developer documentation.

Example data

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

Documentation

User documentation

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).

Developer documentation

The developer documentation is available here.

Dependencies

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.

Contact

Issues can be reported in the GitLab project or by email to contact.dev@lif.univ-mrs.fr.