This tutorial describes the use of ProB's evaluation view to explore single states of a model.
The evaluation view shows the details of a particular state during the animation. It can be used to 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. Also the view shows the truth value of the invariant and its sub-formulas and sub-expressions.