2. The Socket type provides all of the values needed by both sockets,
although each socket uses only some of them. Both variables are initialized to None
to indicate no sockets have been allocated, and are intended to reach Closed at the
end of every run.
The Phase type enumerates the values of the control state variable phase. They
represent the alternation of send and receive actions. The initialization ensures that
a send action comes first. The phase variable is updated by the send and receive
Systems with Finite Models 81
actions of both partners. This would not be possible in the implementation, where
the client and server execute separate programs with no shared data.
The sequences of actions that are possible are determined by the enabling conditions,
boolean methods that test the values of the control state variables. Some
enabling conditions test the states of both partners, which would not be possible in
the implementation. For example, ClientConnectEnable and ServerAcceptEnable
ensure that ClientConnect follows ServerListen and precedes ServerAccept. They
prevent the sequences that would cause the client implementation to crash (if it
connects before the server listens) or cause the server implementation to block (if it
accepts before the client connects).
In most states more than one action is enabled, so many different runs are
possible.
Pages:
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128