Interactive exploration works almost the same way. Instead of working through
the frontier sequentially until it is empty, interactive exploration allows the user
to choose elements from the frontier in any order, and to exit at any time. Where
exhaustive exploration has this:
while (!frontier.IsEmpty)
{
State current = frontier.Head; // choose first element of frontier
frontier = frontier.Tail; // all but first element of frontier
...
Interactive exploration has something like this:
while (!frontier.IsEmpty && still_interested)
{
State current = frontier.Choose(i); // choose an element of frontier
frontier = frontier.Remove(current); // remove that element
...
This same algorithm can be easily extended to explore infinite model programs,
because it is lazy: it delays computing each next state until it is needed, growing
the FSM on the frontier as it goes, always adding to an incomplete subset of the
true FSM. To limit exploration it is only necessary to add a stopping rule to exit
before the frontier is empty. In fact, the mpv tool already provides one stopping rule:
exploration stops after a certain number of transitions, MaxTransitions, has been
found. It could be coded this way:
while (!frontier.IsEmpty && transitions.Count < MaxTransitions)
...
In mpv, MaxTransitions can be set on the command line, in a configuration file, or
in the graphical user interface.
Pages:
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160