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.