Repository files navigation

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

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

The tool can be installed usingpip:

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

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

$ pip3 install --user wheel

To automatically install dependencies (except Python packages and MiniZinc) youcan run thedependencies/install.sh script.

The typing of the code can be checked usingmypy byrunning:

$ 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 MarkupLanguage) and.net format (textual format for Petrinets described intheTina 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 ofdeadlocked states on modelKanban-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 themcc tool.

The tool supports three main kinds of properties:

• Detection of deadlocks,--deadlock: is there a reachable marking with nooutgoing transitions.
• Quasi-liveness,--quasi-liveness t: is there a reachable marking wheretransitiont can fire. You can check the quasi-liveness of several transitionsat 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 placepis marked (it has at least one token). You can check the reachability of severalplaces at once by passing a comma-separated list of place names:--reachability p1,...,pn.

The tool also supports properties from theMCC properties formatby 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 toautomatically compute the reduction (--auto-reduce) or to provide apre-computed version with option--reduce <path>. It is also possible to savea copy of the reduced net with the option--save-reduced-net <path>.

Some examples of nets with their corresponding reductions are available innets/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 inductiveinvariant. This property iseasy to check, even though interestingproperties are seldom inductive.
• BMC: Bounded Model Checking is an iterative method to explore the statespace of systems by unrolling their transitions. This method is only useful forfinding counterexamples.
• K-INDUCTION: is an extension of BMC that can also prove invariants.
• PDR-COV,PDR-REACH andPDR-REACH-SATURATED: Property DirectedReachability, also known as IC3, is a method to strengthen a property that isnot inductive, into an inductive one. This method can return a verdictcertificate. 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 allpotentially reachable markings (solution of the state equation). Weimplement a refined version that can over-approximate the result with the helpof trap constraints and other structural information, such as NUPNspecifications.
• WALK: relies on simulation tools to quickly find counterexamples. Wecurrently usewalk that is distributed with theTinatoolbox.
• SMT andCP: are methods specific to SMPT in the case where nets arefully reducible (the reduced net has only one marking). In this case,reachable markings are exactly the solution of the reduction equations andverdicts 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 thelist of markings into the.aut format) perform anexhaustive 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 incompetition mode

You can list all the options by using thehelp option:

$ python3 -m smpt --helpusage: __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 Netoptional 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 theTool 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 allthe material to install the tool and reproduce the experiments:

• SMPT_TACAS_2022.zip

SMPT, won a bronze medal in the “reachability” category of the Model CheckingContest 2023, an international competition of model checking tools for theverification of concurrent systems.

SMPT, won a bronze medal in the “reachability” category of the Model CheckingContest 2022. It also obtained the 100% confidence award.

• Amat, N, Berthomieu, B, Dal Zilio, S.A Polyhedral Abstraction for Petri Netsand its Application to SMT-Based ModelChecking.Fundamenta Informaticae (FI). 2022.
• Amat, N, Dal Zilio, S.SMPT: A Testbed for Reachability Methods inGeneralized Petri Nets.FormalMethods (FM 2023).
• Amat, N, Dal Zilio, S, Hujsa, T.Property Directed Reachability forGeneralized Petri Nets.Toolsand Algorithms for the Construction and Analysis of Systems (TACAS). 2022.
• Amat, N, Berthomieu, B, Dal Zilio, S.On the Combination of PolyhedralAbstraction and SMT-Based Model Checking for PetriNets.Application and Theory ofPetri Nets and Concurrency (Petri Nets). 2021.
• F. Kordon and P. Bouvier and H. Garavel and F. Hulin-Hubard and N. Amat. andE. 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. andE. 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 andY. Thierry-Mieg.Complete Results for the 2022 Edition of the Model CheckingContest. 2022.
• F. Kordon and P. Bouvier and H. Garavel and L. M. Hillah and F. Hulin-Hubardand N. Amat. and E. Amparore and B. Berthomieu and S. Biswal and D. Donatelliand F. Galla and and S. Dal Zilio and P. G. Jensen and C. He and D. Le Botlanand 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 theMCC Petri NetsRepository located inside foldernets/.

This software is distributed under theGPLv3 license.A copy of the license agreement is found in theLICENSE 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 makingMCC'2021oracles available, and to themembers of the Model Checking Contest committees.