mode[m] == Mode.Sent;
}
}
}
Figure 14.16. Two scenarios for the composition with the protocol features.
0
1
ReqSetup(0, 2)
6
7
ReqWork(1, 2)
5
3
ReqWork(2, 2)
2
ResSetup(0, 2, Status("Completed"))
ResWork(1, 2, Status("Completed"))
8
ReqWork(2, 2)
10
Cancel(1)
ResWork(1, 2, Status("Completed"))
9
ResWork(2, 2, Status("Completed"))
ResWork(1, 2, Status("Cancelled"))
ResWork(1, 2, Status("Completed"))
4
ResWork(2, 2, Status("Completed"))
ResWork(2, 2, Status("Completed"))
ResWork(1, 2, Status("Completed"))
ResWork(1, 2, Status("Cancelled"))
ResWork(1, 2, Status("Completed"))
Figure 14.17. Full exploration of the sample protocol model including the scenarios in Figure 14.16.
Client Server
ReqSetup(0,2)
ResSetup(0,2,Status("Completed"))
ReqWork(1,2)
ReqWork(2,2)
Cancel(1)
ResWork(2,2,Status("Completed"))
ResWork(1,2,Status("Completed"))
Figure 14.18. A valid trace of actions in Figure 14.17.
240
Advanced Topics 241
14.3 Properties of model program composition
Recall from Section 7.3 that, under composition, model programs synchronize steps
for shared actions and interleave actions not found in their common action vocabulary.
We now describe in greater detail how actions are combined, taking into
account both action symbols and arguments, including the placeholder (underscore).
Recall that it is the actions (the terms) that are considered when combining
actions, not the action methods (the C# code).
Pages:
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319