SM(P/)T - Satisfiability Modulo Petri Nets


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


Running the model-checker

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

python3 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

$> smpt --deadlock nets/Kanban/

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 --reduced --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]
            [--no-bmc | --no-ic3 | --auto-enumerative | --enumerative PATH_MARKINGS]
            [--timeout TIMEOUT] [--skip-non-monotonic] [--display-method]
            [--display-model] [--display-time] [--display-reduction-ratio]

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
                        use XML format for properties
  --deadlock            deadlock analysis
  --quasi-liveness QUASI_LIVE_TRANSITIONS
                        liveness analysis (comma separated list of transition
  --reachability REACHABLE_PLACES
                        reachibility analysis (comma separated list of place
  --auto-reduce         reduce automatically the Petri Net (using `reduce`)
                        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 the reduction ratio


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


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


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.