PyCheck is a tool for
- STL/STREL monitoring
- Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models (TACAS18)
and other stuff related to the work of
- Simone Silvetti, Esteco Spa.
- Laura Nenzi, University of Trieste & TU Wien.
- Luca Bortolussi, University of Trieste.
PyCheck ia a partial fork of the project U-Check, plus a conversion from Java to Python.
The reference class for the TACAS paper is BenchMarks.py which is contained in the package pycheck/tesselation/. To run it, you need to install python>=3.6 and the following libraries:
- numpy:1.13
- scipy:0.19
- matplotlib:2.0.2
- numba:0.35
- scikit-learn:0.19
- pyDOE: 0.3.8
(the last versions should be ok. In any case we have speciefied the version we used)
In BenchMarks.py you can find several methods which are reffered to the article. Please recall them in the main method at the end of BenchMarks.py (just comment/uncomment them).
See some examples in this notebook