No edit summary |
|||
Line 1: | Line 1: | ||
__NOTOC__ | |||
This tutorial describes the use of ProB's evaluation view to explore single states of a model. | 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 | The view shows the details of a particular state during the animation. It can be used to |
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
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. You should get window that looks similar to the following screenshot:
You can now expand each of the three sections to investigate the current state of the machine. For instance if we expand the Variables section we will get the following:
The tree shows values for each variable in the same way as the State Properties view. The value of the variable numbers in our example tell us that card(numbers) = 2288 and it shows the first and last entries. In contrast to the State Properties View you can see all values by doubleclicking an entry as shown in the next screenshot.
The save button can be used to save the value of the variable (as a B-Expression) to a file. You can also save the values of multiple variables (we will cover this later).