Request("Setup", (int)a[0], (int)a[1]);
return null;
case ("ReqWork"):
server.Request("Work", (int)a[0], (int)a[1]);
return null;
default: throw new Exception("Unknown action: " + a);
}
}
public void Reset()
{ if (server.IsBusy) throw new Exception("Server is busy"); }
public static IAsyncStepper Make() { return new Stepper(); }
}
}
Figure 16.5. Asynchronous stepper of an SP server.
Advanced Topics 267
condition can be relaxed when the model program is used for on-the-fly testing with
observable actions.
Given a set of action symbols A, a model program is explorable for A if the
parameters of all the actions in A have finite domains in all states. For on-the-fly
testing with observable actions, the model program does not need to be explorable
for observable actions. The reason is that the arguments for the observable actions
are provided by the stepper. Recall that the fundamental property of model program
exploration is that it is lazy. During on-the-fly testing, an observable action is
executed in the model program only when it has occurred in the implementation, at
which point all the parameters have been provided.
Consider the model program SP[Credits,Commands,Setup] with the three included
features from Chapter 14. Notice that Cancel is not in the action vocabulary
of that model progam. Let us add another feature to SP that restricts the parameters
of all the request actions so that each request asks for 3 credits and the requests use
ids from the window of allowed message ids.
Pages:
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351