Documentation - Modest Toolset

The Modest Markov Automata Tutorial provides an introduction to modelling with Modest and using the Modest Toolset for checking Markov automata models. All command-line tools print detailed usage information when invoked with parameter --help. Online documentation of the Modest language and the Modest Toolset's individual tools is available on following pages:

Please submit bug reports and feature suggestions to our issue tracker. We are grateful for every bug report. Every crash of any of the Modest Toolset's tools is a bug.

System Requirements

The Modest Toolset is implemented in C# and uses the .NET runtime. We provide self-contained binary downloads for supported versions of Linux, Windows, and macOS running on x86-64 and ARM-64 processors. Running an x86-64 version of the Modest Toolset in a Docker container on an ARM-64 host system (or in any other QEMU-based environment) is not supported.

Installation

Download the zipped package and extract it to a destination of your choice. Then start any of the tools from the command line via the modest command, e.g. by running ./modest mcsta -?.

External Tools and Libraries

Some of the tools of the Modest Toolset require external tools and libraries for full functionality:

mcsta includes linear programming (LP) as one of the available solution methods, using various LP solvers. The GLOP solver (default, available on all platforms except ARM-64 Windows), part of the Google OR Tools, HiGHS (available on all platforms except ARM-64 Windows), and lp_solve 5.5 (available on x86-64 Linux and Windows) are part of the Modest Toolset download. All other supported solvers (COPT, IBM CPLEX 22.1.1, Gurobi 11.0, and Mosek 10.2) need to be separately obtained (and, where applicable, licensed) by the user for mcsta to be able to use them. mcsta tries to find the respective libraries automatically, and reports an error if this fails. In that case, the paths to the .dll respectively .so files need to be provided manually in the configuration file Externals.defaults.

mosta needs Graphviz dot to automatically generate image files visualising the symbolic semantics of a model. mosta tries to automatically find the required executable file, and reports an error if this fails. In that case, the path to dot needs to be provided manually in the configuration file Externals.defaults.

prohver requires the modified PHAVer executable phaver-64 from the original ProHVer tool. prohver expects to find phaver-64 in the same folder where the main executable (modest on Linux and macOS, modest.exe on Windows) is located. On Windows, prohver requires a working installation of the Windows Subsystem for Linux (WSL) to run phaver-64.

An example of contents of the Externals.defaults configuration file on Windows could be as follows; in any case, the paths need to be adapted to the specific system setup:

{
  "dot-path": "C:\\Program Files\\Graphviz2.26.3\\bin\\dot.exe",
  "copt-path": "",
  "cplex-path": "C:\\Program Files\\IBM\\ILOG\\CPLEX_Studio221\\cplex\\bin\\x64_win64",
  "gurobi-path": "C:\\gurobi1102\\win64\\bin\\",
  "mosek-path": "C:\\Program Files\\Mosek\\10.2\\tools\\platform\\win64x86\\bin"
}

In this example, the paths to dot as well as the CPLEX, Gurobi, and Mosek LP solver libraries are specified explicitly, while mcsta is instructed to try to automatically find the COPT LP solver library (or the user does not plan to use it).