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