In this case the bag implementation
stepper needs to be modified to deal with CheckView actions. This can be done as
follows. An exception is thrown if the view of the model state is not consistent with
the view of the implementation state. Note that the first (and only) argument of a
CheckView action is a term that represents a set of strings. In order to convert that
term into a value, the term is interpreted as a compound value that is then cast to a
set of strings.
212 Testing Systems with Complex State
switch (a.FunctionSymbol.Name)
{
case ("CheckView") :
Set
modelView =
(Set)CompoundValue.InterpretTerm(a.Arguments[0]);
Set implView = new Set(bag.table.Keys);
if (!modelView.Equals(implView))
throw new Exception("Inconsistent views of state: model:" +
modelView + " iut:" + implView);
return null;
case ...
}
Scenarios. Probes are usually checked more frequently than other actions. For
the bag model, we can express this using an FSM scenario called ProbeScenario.
It requires that each Add action and each Delete action must be followed by a
CheckView action. In the same scenario we also disable all lookup and count actions.
FSM(0,AcceptingStates(0),
Transitions(t(0,Add(),1),t(0,Delete(),1),t(1,CheckView(),0)),
Vocabulary("Lookup_Start","Count_Start"))
The following additional FSM scenario called AddDeleteScenario requires that
all Add actions happen before all Delete actions:
FSM(0,AcceptingStates(0,1),
Transitions(t(0,Add(),0),t(0,Delete(),1),t(1,Delete(),1)))
In general, it may be useful to have a whole collection of FSM scenarios stored
in separate files and experiment with various combinations of them using the fsm
option of ct, without having to create factory methods for all of the combinations.
Pages:
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286