Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).
- Python >= 3.7
- z3 - SMT solver
- Tina toolbox - Friend tools
- (Optional) Octant - Quantifier eliminator for polyhedral reductions
- (Optional) MiniZinc - Constraint programming solver
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.
The typing of the code can be checked using mypy by running:
$ mypy smpt --no-strict-optional
The html documentation can be generated using the sphinx generator by running:
$ cd docs $ make html
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
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/.
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.)
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.
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
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 of a given comma-separated list
--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
--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} ...]]
enable methods among WALK STATE-EQUATION INDUCTION BMC
K-INDUCTION PDR-COV PDR-REACH PDR-REACH-SATURATED SMT
CP DUMMY
--auto-enumerative enumerate automatically the states (using `tina`)
--enumerative PATH_MARKINGS
path to the state-space (.aut format)
--project Use TFG projection for WALK, BMC, K-INDUCTION, PDR,
STATE-EQUATION
--show-projection Show projected formulas
--save-projection PATH_PROJECTION_DIRECTORY
Save projected formulas
--timeout TIMEOUT a limit per property on execution time
--global-timeout GLOBAL_TIMEOUT
a limit on execution time
--skip-non-monotonic skip non-monotonic properties
--show-techniques show the method returning the result
--show-time show the execution time
--show-reduction-ratio
show the reduction ratio
--show-shadow-completeness
show the shadow completeness
--show-model show a counterexample if there is one
--check-proof check and show the certificate of invariance if there
is one
--export-proof PATH_PROOF
export the proof of invariance if there is one
--mcc Model Checking Contest mode
--fireability Reachability Fireability mode (Cardinality by default) Model Checking Contest mode
Complete installations of SMPT can be found in the MCC disk images (see the Tool Submission Kit for more information):
- MCC'2023: smpt-2023.tar.gz
- MCC'2022: smpt-2022.tar.gz
- MCC'2021: smpt-2021.vmdk.tar.gz
You can also download the artifact of our [TACAS2022] paper that contains all the material to install the tool and reproduce the experiments:
SMPT, won a bronze medal in the “reachability” category of the Model Checking Contest 2023, an international competition of model checking tools for the verification of concurrent systems.
SMPT, won a bronze medal in the “reachability” category of the Model Checking Contest 2022. It also obtained the 100% confidence award.
- Amat, N, Berthomieu, B, Dal Zilio, S. A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking. Fundamenta Informaticae (FI). 2022.
- Amat, N, Dal Zilio, S. SMPT: A Testbed for Reachability Methods in Generalized Petri Nets. Formal Methods (FM 2023).
- Amat, N, Dal Zilio, S, Hujsa, T. Property Directed Reachability for Generalized Petri Nets. Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2022.
- Amat, N, Berthomieu, B, Dal Zilio, S. On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets. Application and Theory of Petri Nets and Concurrency (Petri Nets). 2021.
- F. Kordon and P. Bouvier and H. Garavel and F. Hulin-Hubard and N. Amat. and E. Amparore and B. Berthomieu and D Donatelli and S. Dal Zilio and P. G. Jensen and L. Jezequel and E. Paviot-Adet and J. Srba and Y. Thierry-Mieg. Complete Results for the 2023 Edition of the Model Checking Contest. 2023.
- F. Kordon and P. Bouvier and H. Garavel and F. Hulin-Hubard and N. Amat. and E. Amparore and B. Berthomieu and D. Donatelli and S. Dal Zilio and P. G. Jensen and L. Jezequel and C. He and S. Li and E. Paviot-Adet and J. Srba and Y. Thierry-Mieg. Complete Results for the 2022 Edition of the Model Checking Contest. 2022.
- F. Kordon and P. Bouvier and H. Garavel and L. M. Hillah and F. Hulin-Hubard and N. Amat. and E. Amparore and B. Berthomieu and S. Biswal and D. Donatelli and F. Galla and and S. Dal Zilio and P. G. Jensen and C. He and D. Le Botlan and S. Li and and J. Srba and . Thierry-Mieg and A. Walner and K. Wolf, Complete Results for the 2021 Edition of the Model Checking Contest. 2021.
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.
- Nicolas AMAT - LAAS/CNRS
- Bernard BERTHOMIEU - LAAS/CNRS
- Silvano DAL ZILIO - LAAS/CNRS
- Didier LE BOTLAN - LAAS/CNRS
We are grateful to Yann THIERRY-MIEG for making MCC'2021 oracles available, and to the members of the Model Checking Contest committees.