(This simplified version
is not the actual code used by the mpv tool.) The frontier is the collection of states
that have been reached but whose enabled transitions have not yet been executed.
(In Figure 6.5, states 1 and 2 are on the frontier; in Figure 6.6, states 1, 3, and 4
are on the frontier.) When exploration begins, only the initial state is on the frontier.
Exploration proceeds by executing transitions that are enabled on the frontier.
When executing, a transition reaches a state that has not already been reached, that
state is added to the frontier. When all of the transitions that are enabled in a state
have been executed, that state is removed from the frontier and added to the collection
of explored states. (In Figure 6.5, state 0 has been explored; in Figure 6.6,
Systems with Finite Models 105
states 0 and 2 have been explored.) The algorithm terminates when the frontier is
empty.
If the model program is finite, this algorithm always terminates. When it does,
the collection of transitions is the true FSM. Variations are possible. In Figure 6.7
the frontier is a sequence and new states are appended to the tail. This results in
breadth-first exploration of the graph of the FSM. If new states were pushed on the
head, depth-first exploration would occur instead. When exploration is exhaustive,
as it is here, the final result is the same; otherwise, the two strategies explore different
subsets of the true FSM.
Pages:
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159