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
parameter to the two values, by using the Domain attribute:
public static void ServerSend([Domain("Temperatures")] double datum)
{
.
Pages:
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129