4. Another scenario,CreditsScenario2, for the Credits model program. Message IDs are 0
and 1. Requests ask for two credits. Responses grant up to two credits.
0 1
ReqSetup(0, 2)
3 5
ReqSetup(1, 2)
2 4 ReqSetup(1, 2)
6
8
7
ResSetup(0, 1)
ResSetup(0, 2)
ResSetup(1, 1)
ResSetup(1, 2)
ResSetup(1, 0)
ResSetup(1, 2)
ResSetup(1, 1)
Figure 14.5. Composition of the scenario in Figure 14.4 with the amended credits model program.
Let us consider another scenario that allows two message IDs to be used and
assumes that the client always requests two credits, whereas the server grants at
most two credits (see Figure 14.4). The full exploration of the composition of this
scenario with the amended credits model program is shown in Figure 14.5.
14.2.2 Message parameters
It is useful to identify those parameter domains of actions that have finite domains
that can be derived from the model program state. These domains can be used
to make the model program explorable. Recall that for a model program to be
explorable, all action parameters must have finite domains. Looking at the credits
model program for example, we can see that all responses from the server must
have message identifiers present in the requests map. Also, all granted credits from
the server must be between zero and the maximum credit requested by the client.
We add these derived parameter domains as another feature model program to SP
(see Figure 14.
Pages:
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308