Formal Approaches to Decision-Making under Uncertainty
Course at the Rio 2023 Summer School by Arnd Hartmanns
The Modest Toolset
(just download and unzip, remember the location)
Visual Studio Code
(optional, but recommended; otherwise, it is also possible to write models in any text editor and run the Modest Toolset from the command line)
(on Windows, we recommend to install GraphViz in its default location so that the Modest Toolset will most likely find it automatically)
(we need version 3.7 or newer)
Do the following steps to configure all the tools to work together:
In Visual Studio Code, install the Modest extension by the Modest Extension Team.
Configure the path to the modest executable from the unzipped Modest Toolset folder in the extension's settings.
Patch a bug in the extension by downloading file main.js and placing it into the modestextensionteam.modestextension-0.0.9/media subfolder inside folder
%USERPROFILE%\.vscode\extensions on Windows or ~/.vscode/extensions on Linux and macOS,
replacing the existing file of the same name.
Open a terminal in the Modest folder in the location where you unzipped the Modest Toolset and run the following command:
modest mosta qcomp://brp -E "N=16,MAX=2" -O brp.dot --dot png brp.png --open-output --delete-output -Y
If it does not run without errors and (ideally) open some image file, then manually configure the location of the dot executable of GraphViz as described at the end of the Modest installation instructions.
Set up an environment for programming in Python that you like.
For example, in Visual Studio code, install the Python extension pack.
The Quantitative Verification Benchmark Set contains many examples and case studies using DTMCs, MDPs, and other formalisms to model various kinds of systems.
All models are available in the JANI format that the Modest Toolset supports, and many of them were originally written in Modest.
The PRISM probabilistic model checker supports more complex properties than Modest, has a nice GUI, and extensive documentation.
Its input language however is more basic, and it does not have advanced statistical model checking methods or support for continuous-stochastic models like Markov automata.
The probabilistic model checker Storm is the fastest in most benchmarks, but a little more complex to set up.
It can process Modest models via the JANI intermediate format, to which Modest models can be converted with the moconv tool of the Modest Toolset.