SM(P/)T - Satisfiability Modulo Petri Net

<br /> <p align="center"> <a href="https://github.com/nicolasAmat/SMPT"> <img src="pics/logo.png" alt="Logo" width="512" height="305"> </a> </p>

About

SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).

Installation

Requirements

• Python >= 3.7
  • (Optional) mypy - static type checker
  • (Optional) sphinx - Python documentation generator
• z3 - SMT solver
• Tina toolbox - Friend tools
  • (Optional) ndrio - Petri net converter (.pnml to .net)
  • (Optional) reduce - Petri net reducer
    • struct
    • 4ti2 or LattE integrale
  • (Optional) walk - Random state space explorer
  • (Optional) tina - State space generator
  • (Optional) play - Stepper simulator
  • (Optional) mcc - Petri net unfolder
• (Optional) Octant - Quantifier eliminator for polyhedral reductions
• (Optional) MiniZinc - Constraint programming solver

Commands

The tool can be installed using pip:

$ python setup.py bdist_wheel
$ python -m pip install --user dist/smpt-5.0-py3-none-any.whl

Note that the wheel package is required, you can install it using:

$ pip3 install --user wheel

To automatically install dependencies (except Python packages and MiniZinc) you can run the dependencies/install.sh script.

Type checking

The typing of the code can be checked using mypy by running:

$ mypy smpt --no-strict-optional

Documentation generation

The html documentation can be generated using the sphinx generator by running:

$ cd docs
$ make html

Running the model checker

Input formats

The tool takes as input descriptions in .pnml (Petri Net Markup Language) and .net format (textual format for Petri nets described in the Tina man pages).

The path to the input Petri net must be specified using the -n <path> option.

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

$ python3 -m smpt -n nets/Kanban/Kanban-00002.net --deadlock --methods BMC

The tools also supports colored Petri nets. In this case, use the option --colored and install the mcc tool.

The tool supports three main kinds 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: --quasi-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 supports 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

Polyhedral reductions

For methods that relies on polyhedral reductions, it is possible to automatically compute the reduction (--auto-reduce) or to provide a pre-computed version with option --reduce <path>. It is also possible to save a copy of the reduced net with the option --save-reduced-net <path>.

Some examples of nets with their corresponding reductions are available in nets/E-Abstraction/.

Output format

Results are printed in the text format required by the Model Checking Contest (MCC) which is of the form:

FORMULA <id> (TRUE/FALSE)

Some options permits to obtain more information:

• --verbose or -v: evolution of the methods
• --debug: input/output SMT-LIB exchanged with the SMT solver
• --show-techniques: returns the methods that successfully computed a verdict
• --show-time: print the execution time per property
• --show-reduction-ratio: get the reduction ratio
• --show-model: print the counterexample if it exists
• --check-proof: check the certificate of invariance (if we have one)
• --export-proof: export verdict certificates (inductive invariants (SMT-LIB), trace leading to counterexamples (.scn format), etc.)

Verification methods

The tool is composed of different methods:

• INDUCTION: a basic method that checks if a property is an inductive invariant. This property is easy to check, even though interesting properties are seldom inductive.
• BMC: Bounded Model Checking is an iterative method to explore the state space of systems by unrolling their transitions. This method is only useful for finding counterexamples.
• K-INDUCTION: is an extension of BMC that can also prove invariants.
• PDR-COV, PDR-REACH and PDR-REACH-SATURATED: Property Directed Reachability, also known as IC3, is a method to strengthen a property that is not inductive, into an inductive one. This method can return a verdict certificate. We provide three different methods of increasing complexity (cf. [TACAS2022]) (one for coverability and two for general reachability).
• STATE-EQUATION: is a method for checking that a property is true for all potentially reachable markings (solution of the state equation). We implement a refined version that can over-approximate the result with the help of trap constraints and other structural information, such as NUPN specifications.
• WALK: relies on simulation tools to quickly find counterexamples. We currently use walk that is distributed with the Tina toolbox.
• SMT and CP: are methods specific to SMPT in the case where nets are fully reducible (the reduced net has only one marking). In this case, reachable markings are exactly the solution of the reduction equations and verdicts are computed by solving linear system of equations.

Depending on the input net, SMPT runs a subset of these methods in parallel.
You can restrict the choice of the verification methods with --methods <method_1> ... <methods_n>.

The --auto-enumerative and --enumerative <path> (where the path leads to the list of markings into the .aut format) perform an exhaustive exploration of the state space.

Tweaking options

We provide a set of options to control the behavior of our verification jobs scheduler such as:

• --global-timeout <int>: add a timeout
• --timeout <int>: add a timeout per property
• --mcc: puts the tool in competition mode

Usage

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

$ python3 -m smpt --help
usage: __main__.py [-h] [--version] [-v] [--debug] -n ptnet [--colored]
                   [--xml PATH_PROPERTIES | --ltl-file PATH_LTL_FORMULA | --ltl LTL_FORMULA | --deadlock | --quasi-liveness QUASI_LIVE_TRANSITIONS | --reachability REACHABLE_PLACES]
                   [--select-queries QUERIES]
                   [--auto-reduce | --reduced PATH_PTNET_REDUCED]
                   [--save-reduced-net]
                   (--methods [{WALK,STATE-EQUATION,INDUCTION,BMC,K-INDUCTION,PDR-COV,PDR-REACH,PDR-REACH-SATURATED,SMT,CP,DUMMY} [{WALK,STATE-EQUATION,INDUCTION,BMC,K-INDUCTION,PDR-COV,PDR-REACH,PDR-REACH-SATURATED,SMT,CP,DUMMY} ...]] | --auto-enumerative | --enumerative PATH_MARKINGS)
                   [--project] [--show-projection]
                   [--save-projection PATH_PROJECTION_DIRECTORY]
                   [--timeout TIMEOUT | --global-timeout GLOBAL_TIMEOUT]
                   [--skip-non-monotonic] [--show-techniques] [--show-time]
                   [--show-reduction-ratio] [--show-shadow-completeness]
                   [--show-model] [--check-proof] [--export-proof PATH_PROOF]
                   [--mcc] [--fireability]

SMPT: Satisfiability Modulo Petri Net

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/output
  -n ptnet, --net ptnet
                        path to Petri Net (.net or .pnml format)
  --colored             colored input Petri net
  --xml PATH_PROPERTIES
                        path to reachability formulas (.xml format)
  --ltl-file PATH_LTL_FORMULA
                        path to reachability formula (.ltl format)
  --ltl LTL_FORMULA     reachability formula (.ltl format)
  --deadlock            deadlock analysis
  --quasi-liveness QUASI_LIVE_TRANSITIONS
                        liveness analysis (comma separated list of transition
                        names)
  --reachability REACHABLE_PLACES
                        reachability analysis (comma separated list of place
                        names)
  --select-queries QUERIES
                        verify queries