But, like any interactive procedure, it is not fully automated
so it can be time-consuming and difficult to repeat. In Chapter 7 we describe another,
3 In mpv, select the initial node with the mouse, press the Delete key to hide all the other states
and transitions, press Enter to display the enabled transitions, press n (next) and p (previous) to
select another node, and so on.
Systems with Finite Models 103
more automatic way that uses composition to check whether a run is allowed, which
is still simpler than writing a unit test.
6.2.4 An exploration algorithm
In this subsection we explain how exploration works by presenting an exploration
algorithm. You do not need to understand the algorithm in order to use the mpv
tool to analyze finite model programs. But to analyze infinite model programs,
you must provide additional information to guide exploration (Chapter 11). Then it
becomes necessary to understand how exploration works. We prepare for that now
by considering exhaustive exploration, which is the simplest case.
Exploration generates an FSM from a model program. It executes the model
program, automatically selecting actions to execute, monitoring, and recording each
state transition as it occurs, building a data structure that contains all the information
shown in state transition tables or diagrams (Table 6.2, Figure 6.2).
Recall that we prepare for exploration by providing a factory method that creates
a LibraryModelProgram object from the compiled model program assembly
(Section 6.
Pages:
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156