On this page, you can find supplementary material for the paper “Riding the Storm in a Probabilistic Model Checking Landscape”.

For each example, we provide Jupyter notebooks which contain the model(s) and the corresponding analysis. All notebooks are available in the stormpyter repository in the directory festschrift_storm. We refer to the README for instructions on how to run the Juypter notebooks with Docker.

The Random Chili Peppers

The folder random_pepper contains the Jupyter notebook and model for the music shuffle example of Section 2.

Enjoyable Road Biking

The folder bikeriding contains the Jupyter notebook and model for the bikeriding example of Section 3.

Scouting for Coffee Supply

The folder coffeescout contains the Jupyter notebook and model for coffee scouting example of Section 4.

The Elfstedentocht Problem

The folder elfstedentocht contains the model, analysis script and results for the Elfstedentocht ice skating example of Section 5.