QCover is a Python implementation of a decision procedure for the Petri net coverability problem that is based on applying reachability in continuous Petri nets as a pruning criterion inside a backward-coverability framework. The heart of the approach is a sophisticated encoding of reachability in continuous Petri nets into SMT which then enables QCover to use the SMT solver Z3 in order to decide such reachability problems. QCover can also be used to decide reachability and coverability in continuous Petri nets.
QCover does not require any installation. However, Python 2.7 must be installed with the following additional packages:
- NumPy ≥1.8.2 (e.g. on Debian-based Linux distributions:
sudo apt-get install python-numpy), - SciPy ≥0.13.3 (e.g. on Debian-based Linux distributions:
sudo apt-get install python-scipy), - Z3 ≥4.4.0: follow installation instructions for Python bindings.
QCover can be executed by simply entering python main.py file_to_verify. For example, the Petri net given here for Lamport's mutual exclusion algorithm can be proven safe as follows:
> python main.py ../examples/lamport/model.spec
Safe
QCover has an experimental parallel mode that can be activated by switching parallel to True in config.py.
QCover supports a strict subset of the .spec format from mist described here. QCover loads .spec files as Petri nets and executes the backward coverability algorithm based on continuous reachability pruning described in [BFHH16, BFHH17] and [Blo16, Chap. 5] (see references below).
The new version of QCover also supports the .tts format from Bfc described here. Currently, QCover loads .tts files as vector addition systems with states (VASS) and executes a backward coverability algorithm with ℤ-VASS reachability pruning. This feature is experimental and is not described in [BFHH16, BFHH17].
Both input file formats can be translated to the other format using, e.g., ttstrans and spec2tts.
The version found under ./stable/ is the original TACAS'16 version. This version contains the benchmarking infrastructure and should be used for comparison with other tools. A new version in development can be found under ./dev/. Its code has been improved for adaptability and extendability.
For any question concerning QCover, contact Michael Blondin or Christoph Haase.
[BFHH16] Michael Blondin, Alain Finkel, Christoph Haase and Serge Haddad. Approaching the Coverability Problem Continuously. Proc. 22nd International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer, 2016. Available online here.
[BFHH17] Michael Blondin, Alain Finkel, Christoph Haase and Serge Haddad. The Logical View on Continuous Petri Nets. Invited submission to the special issue of selected TACAS'16 papers, ACM Transactions on Computational Logic (TOCL), 2017. Available online here.
[Blo16] Michael Blondin. Algorithmique et complexité des systèmes à compteurs. Ph.D. thesis, Université de Montréal & ENS Cachan – Université Paris-Saclay, 2016. Available online here.