Kong is a tool to compute the concurrency relation of a Petri using net reduction. It also permits to compute the dead places and check if a given marking is reachable.
For more information about the usage and the compatible formats please refer to the tool paper published at Petri Nets 2022: Kong: a Tool to Squash Concurrent Places.
- Python >+ 3.5
caesar.bddfrom the CADP Toolbox (only for theconcanddeadsubcommands)siftfrom the TINA Toolbox (only for thereachsubcommand)reduceandndriotools from the TINA Toolbox- (optional) graphviz python package
Run Kong by selecting a subcommand (conc dead, or reach) and indicating the path to the input Petri net (.pnml or .nupn format):
$> ./kong/kong.py {conc, dead, reach} {<path_to_.pnml>, <path_to_.nupn>}
You can list all the subcommands by using the help option:
$> ./kong/kong.py --help
usage: kong.py [-h] [--version] {conc,dead,reach} ...
Koncurrent places Grinder
positional arguments:
{conc,dead,reach} Mode
conc Concurrent places computation
dead Dead places computation
reach Marking reachability decision
options:
-h, --help show this help message and exit
--version show the version number and exit
Similarly, you can list the options of each subcommand.
conc:
$> ./kong/kong.py conc --help
usage: kong.py conc [-h] [-v] [-sk] [-sr | -rn REDUCED_NET] [-t] [-srr] [-se] [-dg] [-nu] [-nr] [-pl] [-sn] [--bdd-timeout BDD_TIMEOUT] [--bdd-iterations BDD_ITERATIONS]
[-rm REDUCED_RESULT] [-srm]
filename
positional arguments:
filename input Petri net (.pnml or .nupn format)
options:
-h, --help show this help message and exit
-v, --verbose increase output verbosity
-sk, --shrink use the Shrink reduction tool
-sr, --save-reduced-net
save the reduced net
-rn REDUCED_NET, --reduced-net REDUCED_NET
specify reduced Petri net (.net format)
-t, --time show the computation time
-srr, --show-reduction-ratio
show the reduction ratio
-se, --show-equations
show the reduction equations
-dg, --draw-graph draw the Token Flow Graph
-nu, --no-units disable units propagation
-nr, --no-rle disable run-length encoding (RLE)
-pl, --place-names show place names
-sn, --show-nupns show the NUPNs
--bdd-timeout BDD_TIMEOUT
set the time limit for marking graph exploration (caesar.bdd)
--bdd-iterations BDD_ITERATIONS
set the limit for number of iterations for marking graph exploration (caesar.bdd)
-rm REDUCED_RESULT, --reduced-matrix REDUCED_RESULT
specify reduced concurrency matrix (or dead places vector) file
-srm, --show-reduced-matrix
show the reduced matrix
dead:
$> ./kong/kong.py dead --help
usage: kong.py dead [-h] [-v] [-sk] [-sr | -rn REDUCED_NET] [-t] [-srr] [-se] [-dg] [-nu] [-nr] [-pl] [-sn] [--bdd-timeout BDD_TIMEOUT] [--bdd-iterations BDD_ITERATIONS]
[-rm REDUCED_RESULT] [-srv]
filename
positional arguments:
filename input Petri net (.pnml or .nupn format)
options:
-h, --help show this help message and exit
-v, --verbose increase output verbosity
-sk, --shrink use the Shrink reduction tool
-sr, --save-reduced-net
save the reduced net
-rn REDUCED_NET, --reduced-net REDUCED_NET
specify reduced Petri net (.net format)
-t, --time show the computation time
-srr, --show-reduction-ratio
show the reduction ratio
-se, --show-equations
show the reduction equations
-dg, --draw-graph draw the Token Flow Graph
-nu, --no-units disable units propagation
-nr, --no-rle disable run-length encoding (RLE)
-pl, --place-names show place names
-sn, --show-nupns show the NUPNs
--bdd-timeout BDD_TIMEOUT
set the time limit for marking graph exploration (caesar.bdd)
--bdd-iterations BDD_ITERATIONS
set the limit for number of iterations for marking graph exploration (caesar.bdd)
-rm REDUCED_RESULT, --reduced-vector REDUCED_RESULT
specify reduced dead places vector file
-srv, --show-reduced-vector
show the reduced vector
reach:
$> ./kong.py reach --help
usage: kong.py reach [-h] [-v] [-sk] [-sr | -rn REDUCED_NET] [-t] [-srr] [-se] [-dg] [-m MARKING] [-sf] filename
positional arguments:
filename input Petri net (.pnml or .net format)
options:
-h, --help show this help message and exit
-v, --verbose increase output verbosity
-sk, --shrink use the Shrink reduction tool
-sr, --save-reduced-net
save the reduced net
-rn REDUCED_NET, --reduced-net REDUCED_NET
specify reduced Petri net (.net format)
-t, --time show the computation time
-srr, --show-reduction-ratio
show the reduction ratio
-se, --show-equations
show the reduction equations
-dg, --draw-graph draw the Token Flow Graph
-m MARKING, --marking MARKING
marking
-sf, --show-projected-marking
show the projected marking
The code repository includes a reproducible performance evaluation in the benchmark/ directory. (Jupyter notebook is required.)
- Amat, N, Bouvier, P, Garavel, H. A Toolchain to Compute Concurrent Places of Petri Nets. Petri Nets and Other Models of Concurrency (ToPNoC), To appear.
- Amat, N, Dal Zilio, S, Le Botlan, D. Leveraging polyhedral reductions for solving Petri net reachability problems. International Journal on Software Tools for Technology Transfer (STTT). 2023.
- Amat, N, Chauvet, L. Kong: A Tool to Squash Concurrent Places. Application and Theory of Petri Nets and Concurrency (Petri Nets). 2022.
- Amat, N, Dal Zilio, S, Le Botlan, D. Accelerating the Computation of Dead and Concurrent Places Using Reductions. Model Checking Software (SPIN). 2021.
The code repository includes a link to models from the Model Checking Contest (MCC) 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 - LAAS/CNRS