www.prismmodelchecker.org

PRISM Benchmark Suite

Because there are a large number of PRISM models available, spread across the tool distribution, the case study repository, related publications and elsewhere, it can be difficult to put to put together a good set of examples for the purposes of benchmarking or testing a probabilistic new model checking implementation or technique. Here, we provide a set of PRISM models and properties, grouped by type, to make this process easier.

For details of the models and the properties in the benchmark suite, follow the links below.

The benchmarks themselves are now hosted on GitHub:

From there, you can browse individual files, or download a zip containing all files.

You can also find links to the directory for each benchmark in the tables the pages above.

Here is a useful script for automation of test/benchmark runs. See the top of the file for brief usage instruction:

Don't forget that PRISM can export models in various formats.

Comments or suggestions regarding this benchmark set, as well as contributed models, are welcome.

To cite the PRISM benchmark suite, please use:

Benchmarks