A response
action has a status field as the third argument. The value of the status field indicates
whether the requested operation was cancelled or completed by the server. If the
status of a response is Cancelled, it must be the case that cancellation of the
corresponding request was sent by the client. Notice that the client may try to cancel
a request but the cancellation arrives too late to the server who has already completed
the request. Therefore, the status of a response to a request that has been cancelled
by the client may be either Cancelled or Completed.
Exploration
Let us look at a particular scenario of the cancellation model program. First note
that the model program behaves uniformly for all message IDs and there are no
interactions or dependencies between actions with distinct message IDs. It is therefore
enough to fix a single message ID, say 2. A convenient way to do so is to use
the FSM scenario shown in Figure 14.8. Notice that the scenario disables all the
work actions by including them in the vocabulary of the FSM. The composition
of the scenario in Figure 14.8 with the cancellation model program is shown in
Figure 14.9.
For visual inspection and validation it is important to choose a small set of
parameters. For example, if we add another message ID 3 into the scenario in
Figure 14.8, that is, we consider the FSM in Figure 14.
Pages:
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311