In this simplified description we have not discussed parameter generation, which
assigns values to the parameters of action methods. Recall that parameter values are
106 Exploring and Analyzing Finite Model Programs
drawn from a set called a domain. In each state, exploration executes each action
method repeatedly, using as many different values as it can from the domains of all
its parameters. Each combination of parameter values defines a different action, so
larger domains result in more actions and more transitions. Enabling conditions can
depend on parameters as well as state variables, so each combination of parameter
values must be checked; some combinations may not be enabled in some states.
6.3 Analysis
It can be helpful to simply view the graph of the FSM, but it is more useful to
investigate particular issues. Exploration can provide the answers to several kinds
of specific questions.
Several statistics are computed during exploration, including the number of states
and transitions found (this is not shown in the algorithm of Figure 6.7). These statistics
can provide useful diagnostic information. For example, they reveal whether
exploration did in fact generate the true FSM. The default for the limit MaxTransitions
is quite small, only 100. If exploration reaches this limit, it does not generate
the true FSM, but only some portion of it.
Pages:
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161