Kong - Koncurrent Places Grinder


Kong is a tool to compute the concurrency relation of a Petri using net reduction.


Running the Tool

Before running the tool you need to export the PNML2NUPN environment variable to indicate the path to the PNML2NUPN Java Archive:

$> export PNML2NUPN=<path_to_.jar>

Run Kong by indicating the path to the input Petri net (.pnml format):

$> ./kong.py <path_to_.pnml>

You can list all the options by using the help option:

$> ./kong.py --help
usage: kong.py [-h] [--version] [-v] [--save-reduced | --reduced REDUCED_NET]
               [--timeout TIMEOUT] [-pl] [-t] [--reduction-ratio]
               [--show-equations] [--draw-graph] [--show-reduced-matrix]

Koncurrent places Grinder

positional arguments:
  filename              input Petri net (.pnml format)

optional arguments:
  -h, --help            show this help message and exit
  --version             show the version number and exit
  -v, --verbose         increase output verbosity
  --save-reduced, -sr   save the reduced net
                        reduced Petri Net (.net format)
  --timeout TIMEOUT     set time limit for the BDD-based exploration
  -pl, --place-names    show place names
  -t, --time            show the computation time
  --reduction-ratio     show the reduction ratio
  --show-equations      show the reduction equations
  --draw-graph          draw the Token Flow Graph
                        show the reduced matrix

Performance Evaluation

The code repository includes a reproducible performance evaluation in the benchmark/ directory.
Jupyter is needed to run the code.


The code repository includes a link to models from the MCC Petri Nets Repository used for benchmarking and continuous testing.


This software is distributed under the GPLv3 license. A copy of the license agreement is found in the LICENSE file.


Nicolas Amat
Nicolas Amat
PhD Student in Model Checking

My research interests include model checking, Petri nets and SMT solving.