Evaluation View: Difference between revisions

This tutorial describes the use of ProB's evaluation view to explore single states of a model. The view shows the details of a particular state during the animation. It can be used to

1. learn about the values of a some variables. This feature is overlapping with the State Properties View in the bottom left section of ProB's main window, but the evaluation view allows to inspect a value in greater detail. In particular the used can inspect the sub-expressions
2. understand the truth value of the invariant and its sub-formulas and the values of the sub-expressions.
3. export the content of variables in a state to use them outside of ProB.

First steps

As an example specification we use the Sieve.mch delivered with the ProB Distribution in the "Less Simple" folder. After opening the model do a couple of animation steps and then open the Evaluation view in the Analyse menu.

Filtering relevant information

Data Extraction