9"))
32
ClientReceive_Start() ClientReceive_Finish(double("99.9"))
ClientReceive_Finish(double("99.9"))
ServerClose() ClientSocket()
Figure 7.1. Client/server: true FSM.
and Listen, and the client executes Socket. There are several runs where the client
Socket action is interleaved between different server actions. We know that all of
these runs have to be equivalent because the client and server do not even begin to
interact until the client??™s Connect action. Before that, the order of the interleaving
of client and server actions cannot make any difference. Indeed, all of these runs
reach the same state. There are several other runs where the server executes Close
before the client connects. Nothing interesting can happen after that, so these runs
end in dead states. In the usual case where we want to see what happens after the
client and server connect, we could replace all of the runs in Figure 7.2 by a single
run without losing any useful information.
Systems with Finite Models 117
0
2
ServerSocket()
1
ClientSocket()
3
9
ServerClose()
4
ClientSocket()
5
ServerBind() ServerSocket()
ServerClose()
7
ServerBind()
ServerClose() 8
ServerListen()
ServerClose()
10
ClientConnect()
ServerClose()
ClientSocket()
6
ServerListen()
ServerClose() ClientSocket()
Figure 7.2. Client/server: the first few transitions of all runs.
This example shows that we often know a priori ??“ before any exploration or
testing ??“ that we do not want to consider certain runs.
Pages:
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177