mtype = {b0,b1,k}; bool proc0InCrit = false; bool proc1InCrit = false; init { chan mem0 = [0] of {mtype,bit}; chan mem1 = [0] of {mtype,bit}; run Memory(mem0, mem1, false, false, 0); run Process0(mem0); run Process1(mem1); } proctype Memory(chan mem0, mem1; bit b0v, b1v, kv) { do :: mem0?b0,b0v; :: mem0?k,kv; :: mem1?b1,b1v; :: mem1?k,kv; :: mem0!b1,b1v; :: mem0!k,kv; :: mem1!b0,b0v; :: mem1!k,kv; od; } proctype Process0(chan mem) { BEGIN: mem!b0,true; mem!k,1; do :: mem?b1,false; break; :: mem?b1,true; :: mem?k,0; break; :: mem?k,1; od; proc0InCrit = true; proc0InCrit = false; mem!b0,false; goto BEGIN; } proctype Process1(chan mem) { BEGIN: mem!b1,true; mem!k,0; do :: mem?b0,false; break; :: mem?b0,true; :: mem?k,0; :: mem?k,1; break; od; proc1InCrit = true; proc1InCrit = false; mem!b1,false; goto BEGIN; }