A Cancel request is a ???meta??? request
in the sense that it triggers no response of its own, it has no separate ID besides k,
232 Compositional Modeling
and it is not considered as part of the credits feature; that is, a Cancel request cannot
be used by the client to get more credits. The model program of the cancellation
feature is shown in Figure 14.7.
State variables
The cancellation model program has one state variable mode whose value is a map of
pending request IDs that records for each entry whether it has been sent or cancelled
by the client. Initially no request has been either sent or cancelled, so the value of
mode is the empty map.
Actions
The action vocabulary of the cancellation model program contains all of the action
symbols listed above. The credits field is ignored in all actions.
The update rule of a Setup or a Work request updates the mode of that request ID
to indicate that the request has been sent to the server. The enabling condition is that
a request with the same ID is not pending.
A Cancel request is enabled for all requests. This is needed to avoid race conditions
between the client and the server. A Cancel request must have no effect on the
behavior of the server unless the request being cancelled has actually been sent to
the server and is not yet cancelled or completed.
The update rule of a response action removes the pending request.
Pages:
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310