SM(P/)T - Satisfiability Modulo Petri Nets

About

SMPT is an SMT-based model-checker for Petri nets that takes advantage of net reductions.

Requirements

Running the model-checker

(Optional) The tool can be freezed into executables using cx_Freeze by running:

python3 setup.py build

The tool takes as input descriptions in the .net format, a textual format for Petri nets described in the Tina man pages. To convert .pnml nets to .net format use ndrio.

SMPT supports the verification of several kind of reachability properties on Petri net. For instance, the following call can be used to check for the existence of deadlocked states on model Kanban-00002.net.

$> smpt --deadlock nets/Kanban/Kanban-00002.net

The tool support three main kind of properties:

  • Detection of deadlocks, --deadlock: is there a reachable marking with no outgoing transitions
  • Quasi-liveness, --quasi-liveness t: is there a reachable marking where transition t can fire. You can check the quasi-liveness of several transitions at the same time by passing a comma-separated list of transition names: --liveness t1,...,tn
  • Reachability: --reachability p: is there a reachable marking where place p is marked (it has at least one token). You can check the reachability of several places at once by passing a comma-separated list of place names: --reachability p1,...,pn

The tool also support properties from the MCC properties format by using the option --xml and indicating the path to the .xml properties file. At this time, the support is restricted to:

  • --xml GlobalProperties.xml
  • --xml ReachabilityCardinality.xml
  • --xml ReachabilityFireability.xml

To take advantage of possible reductions in the Petri net, you can use option --reduce <path_to_reduced_net>. For example:

$> smpt Kanban-00002.net --reduced Kanban-00002_reduced.net --deadlock

Option --auto-reduce requires the installation of the reduce tool, that is currently developped by the Vertics team at LAAS-CNRS. The regular distribution of TINA does not contain this tool yet.

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

$> smpt --help
usage: smpt [-h] [--version] [-v] [--debug]
            [--xml PATH_PROPERTIES | --deadlock | --quasi-liveness QUASI_LIVE_TRANSITIONS | --reachability REACHABLE_PLACES]
            [--auto-reduce | --reduced PATH_PTNET_REDUCED]
            [--save-reduced-net]
            [--no-bmc | --no-ic3 | --auto-enumerative | --enumerative PATH_MARKINGS]
            [--timeout TIMEOUT] [--skip-non-monotonic] [--display-method]
            [--display-model] [--display-time] [--display-reduction-ratio]
            ptnet

SMPT: Satisfiability Modulo Petri Net

positional arguments:
  ptnet                 path to Petri Net (.net format)

optional arguments:
  -h, --help            show this help message and exit
  --version             show the version number and exit
  -v, --verbose         increase output verbosity
  --debug               print the SMT-LIB input/ouput
  --xml PATH_PROPERTIES
                        use XML format for properties
  --deadlock            deadlock analysis
  --quasi-liveness QUASI_LIVE_TRANSITIONS
                        liveness analysis (comma separated list of transition
                        names)
  --reachability REACHABLE_PLACES
                        reachibility analysis (comma separated list of place
                        names)
  --auto-reduce         reduce automatically the Petri Net (using `reduce`)
  --reduced PATH_PTNET_REDUCED
                        path to reduced Petri Net (.net format)
  --save-reduced-net    save the reduced net
  --no-bmc              disable BMC method
  --no-ic3              disable IC3 method
  --auto-enumerative    enumerate automatically the states (using `tina`)
  --enumerative PATH_MARKINGS
                        path to the state-space (.aut format)
  --timeout TIMEOUT     a limit on execution time
  --skip-non-monotonic  skip non-monotonic properties
  --display-method      display the method returning the result
  --display-model       display a counterexample if there is one
  --display-time        display execution times
  --display-reduction-ratio
                        display the reduction ratio

Dependencies

The code repository includes copies of models taken from the MCC Petri Nets Repository located inside folder ./nets.

License

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

Authors

We are grateful to Yann THIERRY-MIEG for making MCC'2020 oracles available.

Nicolas Amat
Nicolas Amat
PhD Student in Model Checking

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