The number of credits granted by the
server determines how the pool grows or shrinks as time progresses. There is quite
226 Compositional Modeling
a lot of implementation freedom in the way that the server can grant credits and in
the way that the client can ask for new credits or use the available message IDs.
This is an example of a sliding window protocol. Here the pool of identifiers is
the ???window??? whose contents change or ???slide??? as time progresses. However, the
pool is not necessarily a consecutive interval of numbers because the client does not
have to pick the numbers from the pool in any particular order.
This feature is defined uniformly for all of the commands that are communicated
between the server and the client, except for Cancel.
State variables
The model program of the credits feature is shownin Figure 14.1. The model program
has three state variables: window is the set of all message IDs that the client may use
to send new requests to the server, requests is a map containing all the outstanding
credit requests with message IDs as keys, and maxId is the largest ID that has been
granted by the server. In the initial state of the model program the only possible
message ID is 0, the maximum ID is also 0, and there are no pending requests.
Actions
The action vocabulary of the credits model program consists of the action symbols
ReqSetup, ReqWork, ResSetup, and ResWork.
Pages:
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302