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. For example, in states where phase == Phase.Send, both ClientSend and
ServerSend are enabled, so either partner could send the first message.
Unlike the implmentation, here the client’s send method has no command argument,
and the server has no receive buffer. In the runs we wish to model, these
items always have the same value (the T command), so they add no information to
the state. They are only used for synchronization. In the model, synchronization is
achieved by the phase variable.
Like the implementation, here the server’s send method has an argument, a
number that represents the temperature acquired by the server. In the model, the
server’s send method simply assigns this number to the client’s receive buffer. This
models the effect of transmission across the network.
In the model, the receive buffer is a number (a C# double), not a string as it
is in the implementation. To model the situation where this buffer is empty in the
implementation, we set it to a special numeric constant double.MaxValue that we
name EmptyBuffer.
We limit the receive buffer to just two temperature values, the constants we call
Temp2 and Temp3. We achieve this by limiting the temperatures that can be assigned
to the receive buffer by the ServerSend method. We limit that method’s datum