The scenario model produced by
CreateScenario is still infinite because the size of the bag is unbounded. However,
unlike the Contract model program, the model program created by CreateScenario
is explorable because all parameter domains are finite.
Often it is useful to identify a particular set of states of a model program or
a restricted model program as accepting states. A legal run must terminate in an
accepting state. What states are considered as accepting states may depend on what
features are considered. The feature in Figure 12.3 defines that the accepting state
condition for this feature is that the bag is empty; thus, the initial state is the only
accepting state in this case. If no accepting state condition is provided then all
states are considered as accepting states. If multiple features are considered then
the accepting state condition is the conjunction of all the accepting state conditions
present in the included features.
12.2.3 Stepping the implementation
Recall that an IUT is exposed through a stepper (Section 8.3). The stepper ???steps???
through the IUT one action at a time. It has a current state that corresponds to the
current state of the IUT. Initially, the stepper??™s current state corresponds to the IUT??™s
initial state.
When the stepper performs an action, it calls the IUT with the corresponding input
arguments. The inputs encoded in the action are abstract and are not necessarily the
concrete values required by the IUT.
Pages:
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268