6. Model Analysis¶
After constructing and validating the model, we can now harvest the benefits of formal modeling by handing it over to an analysis tool.
Momba provides interfaces to state-of-the-art model analysis tools such as Storm and the Modest Toolset.
For this tutorial, we will be using the Modest Toolset, in particular, the probabilistic model checker mcsta.
Using mcsta you will be plotting the optimal winning probability as a function of the failure probability for different tracks such as in Fig. 6.1.
Fig. 6.1 Optimal winning probability as a function of the failure probability for different tracks.¶
First, we have to install Matplotlib, a plotting package for Python:
poetry add matplotlib
Exercise
The file fmracer/analysis.py provides a skeleton for the analysis tool which you have to complete by filling in the gaps.
Again, each gap comes with detailed instructions and hints what you need to do.
To run the analysis, the virtual environment needs to be active (see Model Validation). Having activated the virtual environment, you start the analysis with:
fmracer analyze tracks/simple.txt tracks/large.txt
This will run the analysis using the tracks defined in tracks/simple.txt and tracks/large.txt.
The result of the analysis will be written to the file results.pdf in the current working directory.
The file solutions/analysis.py contains a possible solution.