content; } }
static bool drawing = false;
[Action]
static void Draw_Start() { drawing = true; }
static bool Draw_StartEnabled() { return !drawing && !B.IsEmpty; }
[Action]
static void Draw_Finish([Domain("B")]string e)
{ drawing = false; Contract.content = B.Remove(e); }
static bool Draw_FinishEnabled(string e)
{ return drawing && B.Contains(e); }
[Action("Add"), Action("Delete")]
[Action("Lookup_Start"), Action("Lookup_Finish")]
[Action("Count_Start"), Action("Count_Finish")]
static void Other() { }
static bool OtherEnabled() { return !drawing; }
}
}
Figure 16.2. A dependent Draw feature for BagModel in Figure 12.2.
stepping. In other words, queueing of obsevable actions is not needed. In this case,
nondeterminism is resolved immediately when it occurs. Synchronous stepping, as
discussed in Section 12.2.3, is then an adequate solution to harness the IUT for
testing.
Shallow nondeterminism. In some cases, nondeterminism arises only because of
multiple possible outputs to some inputs. In particular, all states of the model program
are such that either all enabled actions in a state are controllable or all enabled actions
in a state are observable. Say a state is active in the first case and passive in the
second case. Moreover, a transition from a passive state leads to an active state.
To illustrate this case on a concrete example, recall the bag example from Chapter
12.
Pages:
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346