| Variable | Enabling Range | State Transformation | Remarks |
|---|---|---|---|
| C1WaitsForServer(C1WaitsForServer) | in {0,...,2} | not modified | Action occurs at full range of values! |
| C1WaitsForUser(C1WaitsForUser) | in {0,...,2} | not modified | Action occurs at full range of values! |
| C2WaitsForServer(C2WaitsForServer) | = 0 | not modified | |
| C2WaitsForUser(C2WaitsForUser) | = 1 | v'=v-1 | |
| C2Thinking(C2Thinking) | = 0 | v'=v+1 |