# Documentation

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.

## System Requirements

The Modest Toolset is implemented in C# and uses the .NET Core runtime. We provide self-contained binary downloads for supported versions of 64-bit Linux, Windows, and macOS.

## 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

The following external tools are required for full functionality:

prohver expects to find phaver-64 in the same folder where prohver.dll is located. mosta tries to automatically find the required executable file, and reports an error if this fails. In that case, you need to provide the path to dot manually in the configuration file Externals.defaults. Typical contents of this file on Windows look like the following (you need to adapt this to your specific system setup):

{
"dot-path": "C:\\Program Files\\Graphviz2.26.3\\bin\\dot.exe"
}