7 with the scenario in Figure
14.10. Labels on transitions are abbreviated by action symbols.
State variables
The model program uses an enumeration CMD of commands. Each element x of CMD is
used to relate an x request with an x response. The state variable cmd maps message
IDs to commands.
Actions
Each action has a separate update rule. When the client issues a request with
command X and message ID m, the update rule records that using the cmd variable.
The request is enabled only if the request is not pending already. When the server
responds with a message ID m, then the command in that response must be cmd[m].
Notice that both the credits and the status fields are ignored in this model program.
Exploration
The model program is rather straigthforward in this case. It is still useful to visualize
a scenario of this model program.We use the FSM in Figure 14.13. The composition
of this FSM with the commands model program is shown in Figure 14.14.
14.2.5 Setup feature
The fourth and final feature of the protocol that we model here is the initial setup
phase of the protocol. Before the protocol is initialized, the client must issue a setup
request to the server and the server has to respond that the setup is completed. Once
the protocol has been initialized the Setup command can no longer be issued. We
can model this feature as an FSM shown in Figure 14.
Pages:
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314