This provides a more convenient way to simulate
particular runs than coding and executing main methods or unit tests, as we did in
Chapter 5, Section 5.5
Figures 6.5 and 6.6 show the interactive exploration of the first run we tested in
Chapter 5. At first, only the initial state appears. At our command, mpv shows all the
actions enabled in the initial state. We select ShowTitles by selecting its next state
(Figure 6.5). Then we command mpv to show all the transitions enabled in that state,
102 Exploring and Analyzing Finite Model Programs
0
1
SelectMessages()
2
ShowTitles()
Figure 6.5. Simulation by interactive exploration (1).
0
2
ShowTitles()
1
SelectMessages() ShowText()
3
SelectMessages()
4
SortByFirst()
Figure 6.6. Simulation by interactive exploration (2).
and select SortByFirst by selecting its next state (Figure 6.5). Proceeding in this
way, we can simulate the entire run.3
Interactive exploration can also show that a run is not allowed. If we attempt
to explore the second run that we tested in Chapter 5, we find that after the first
SortByFirst transition, the second SortByFirst transition is not enabled, so it is not
possible to execute that run.
It is not always obvious whether or not a particular run (that you might write down)
is allowed by a model program. As we have shown here, interactive exploration is one
way to determine this.
Pages:
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155