About

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.

Requirements

• Python >+ 3.5
• caesar.bdd from the CADP Toolbox (only for the conc and dead subcommands)
• sift from the TINA Toolbox (only for the reach subcommand)
• reduce and ndrio tools from the TINA Toolbox
• (optional) graphviz python package

Running the Tool

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

Performance Evaluation

The code repository includes a reproducible performance evaluation in the benchmark/ directory. (Jupyter notebook is required.)

References

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

Dependencies

The code repository includes a link to models from the Model Checking Contest (MCC) used for benchmarking and continuous testing.

License

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

Authors

• Nicolas AMAT - LAAS/CNRS