The enumerator, on the
other hand, has a more limited interface that does not support querying for the
number of elements or for random access. Instead, the enumerator allows you to get
the first element in the enumeration and each successive element in turn. There is
no requirement that the number of elements in the enumerator be finite.
Similarly, a data structure for an FSM provides operations that allow you to query
for the number of states and transitions. A model program, in contrast, has a more
Systems with Complex State 157
limited interface. The model program allows you to get the initial state and produce
transitions that take you to subsequent states. Like an enumerator, you can??™t find out
how many states a model program has without exploring it step by step.
Model programs with large numbers of states and transitions are not just a
theoretical curiosity. Using values with large domains like strings and integers turns
out to be very useful for modeling realworld systems. Data types like int and string
provide descriptive power. We??™ll see this with an example later in this chapter. For
now, let??™s review the kinds of data types that can be used in writing model programs.
10.2 Types for model programs
You may only use certain types for state variables and action parameters in model
programs that work with the tools we describe.1 This is necessary because exploration
using these tools can only determine whether two states are equal when the
state variables belong to these types.
Pages:
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223