This scenario is also a dependent feature of the sample protocol model because it
references the state of the cancellation model program.
Full exploration of the sample protocol model with all the features composed
with the scenarios in Figure 14.16 is shown in Figure 14.17. Notice how the features
interact by synchronizing on actions whose symbols are shared. The allowed action
traces of the composed model program belong to the intersection of the traces of the
individual model programs.
A valid trace of actions is illustrated in Figure 14.18. In this trace all requests
were completed, even though request 1 was cancelled by the client. The status field
in the response actions comes from the cancellation model program, whereas the
allowed message IDs come from the credits model program. The fact that setup
has to precede work is due to the setup model program. In state 2 the window
of the credits model program is the set {3, 4, 5, 6} and all the map-valued state
variables are empty maps. If we would remove the restriction that the server always
grants the maximum number of credits, we would obtain a state transition graph
that represents all the valid server behaviors for the given client behaviors. The
state graph would have 24 states and 62 transitions. The final state of every valid
trace would have a credits window equal to one of the sets {3}, {3, 4}, {3, 4, 5},
or {3, 4, 5, 6}, depending on the actual number credits granted by the server in the
responses.
Pages:
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317