Suppose that a dependent feature called Draw is added to the bag model
program that allows elements to be chosen and removed (drawn) from the bag (see
Figure 16.2).
Advanced Topics 263
0
1
Add("a")
3
Add("b")
8
Draw_Start()
6
Draw_Start()
2
Add("a")
4
Add("b")
10
Draw_Start()
Draw_Finish("a")
Draw_Finish("b")
Draw_Finish("a")
Draw_Finish("b")
0
1
Add("a") Draw() / "a"
3
Add("b") Draw() / "b"
2
Draw() / "a" Add("a")
4
Add("b") Draw() / "b"
(a) (b)
Figure 16.3. Partial exploration of BagModel[Draw]. In (b) passive states are hidden.
The model program has two new actions Draw Start() and Draw Finish(e),
where the first action represents a request to draw and the second action represents
a particular element e that was drawn. This action is nondeterministic because any
element in the bag might be drawn (any element from the domain B might be chosen).
The state variable drawing is used to disable all actions besides Draw Finish until
the draw operation has been completed.
A partial exploration of BagModel[Draw] with mpv is illustrated in Figure 16.3. All
passive states are shown as diamonds in Figure 16.3(a). (The mpv tool can generate
a partial exploration interactively, as described in Chapter 6, Section 6.2.3.) The
nondeterminism is indicated by the two Draw Finish transitions exiting from state 6
in Figure 16.3(a) and the two Draw transitions exiting from state 3 in Figure 16.
Pages:
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347