mtype = { MESSAGE }; chan request[2] = [1] of { mtype }; chan answer [2] = [1] of { mtype }; bool inC[2] = false; bool wait[2] = false; proctype client(byte id) { do :: true -> request[id-1] ! MESSAGE; wait[id-1] = true; answer[id-1] ? MESSAGE; wait[id-1] = false; inC[id-1] = true; C: skip; inC[id-1] = false; request[id-1] ! MESSAGE od; } proctype server() { unsigned given : 2 = 0; unsigned waiting : 2 = 0; unsigned sender : 2; do :: true -> if :: request[0] ? MESSAGE -> sender = 1 :: request[1] ? MESSAGE -> sender = 2 fi; if :: sender == given -> if :: waiting == 0 -> given = 0 :: else -> given = waiting; waiting = 0; answer[given-1] ! MESSAGE fi; :: given == 0 -> given = sender; answer[given-1] ! MESSAGE :: else waiting = sender fi; od; } init { run client(1); run client(2); run server(); }