moves-rwth / prophesy

Parameter Synthesis in Markov Models
https://moves-rwth.github.io/prophesy/
GNU General Public License v3.0
6 stars 3 forks source link
markov-chain model-checking parameters research

Prophesy

Prophesy is a tool set for parameter synthesis of parametric Markov models, developed between 2015 and 2019. Please notice that prophesy is academic software, and mostly meant as a sandbox for developing new algorithms. Prophesy is no longer actively developed.

The so-far final release of Prophesy is accompanied by an overview paper.

Installation

We advise users to follow this guide.

Then:

python setup.py develop

installs the required dependencies and prophesy.

It will create prophesy/prophesy.cfg and prophesy/dependencies.cfg which you might want to extend.

Running:

python -m pytest tests
python -m pytest scripts/tests

executes varying tests. Any occurrences of s show that your support currently does not contain some optional dependencies.

Getting Started

The command line tools are available in the scripts folder.

Examples

The directory examples contains parametric models which can be used as input for Prophesy. The directory benchmark_files contains additional parametric models which have been used as benchmarks in the overview paper.

Authors

Prophesy was mainly developed at RWTH Aachen University by:

Prophesy received notable contributions from:

We would like to thank Christian Hensel and Tim Quatmann for their contributions in the Storm backend, Murat Cubuktepe for his support in developing the QCQP-driven feasibility sampling, and Gereon Kremer for his support of CArL. Prophesy is developed in close cooperation with Nils Jansen, Joost-Pieter Katoen, and Erika Abraham.