proc S0 = send.S0' proc S0' = 's0.(rack0.S1 + rack1.S0' + t.S0') proc S1 = send.S1' proc S1' = 's1.(rack1.S0 + rack0.S1' + t.S1') proc R0 = r0.'receive.'sack0.R1 + r1.'sack1.R0 + t.'sack1.R0 proc R1 = r1.'receive.'sack1.R0 + r0.'sack0.R1 + t.'sack0.R1 proc C1 = s0.'r0.C1 + s1.'r1.C1 + sack0.'rack0.C1 + sack1.'rack1.C1 proc C2 = s0.('r0.C2 + C2) + s1.('r1.C2 + C2) + sack0.('rack0.C2 + C2) + sack1.('rack1.C2 + C2) set Internals = { r0,r1,s0,s1,rack0,rack1,sack0,sack1 } proc SYS1 = (R0 | C1 | S0) \ Internals proc SYS2 = (R0 | C2 | S0) \ Internals