byte Slot[6]; byte next=0; init { d_step { Slot[0] =1; Slot[1] =0; Slot[2] =0; Slot[3] =0; Slot[4] =0; Slot[5] =0; } atomic { run P_0(); run P_1(); run P_2(); run P_3(); run P_4(); run P_5(); } } proctype P_0() { byte my_place=0; byte cs=0, wait=0; NCS: cs = 0; if :: d_step {my_place = next;next = next+1;} goto p1; fi; p1: wait = 1; if :: d_step {my_place==6-1;next = next-6;} goto p2; :: d_step {my_place!=6-1;my_place = my_place%6;} goto p2; fi; p2: wait = 1; if :: Slot[my_place]==1; goto p3; fi; p3: wait = 1; if :: Slot[(my_place+6-1)%6] = 0; goto CS; fi; CS: wait = 0; cs = 1; if :: Slot[(my_place+1)%6] = 1; goto NCS; fi; } proctype P_1() { byte my_place=0; NCS: if :: d_step {my_place = next;next = next+1;} goto p1; fi; p1: if :: d_step {my_place==6-1;next = next-6;} goto p2; :: d_step {my_place!=6-1;my_place = my_place%6;} goto p2; fi; p2: if :: Slot[my_place]==1; goto p3; fi; p3: if :: Slot[(my_place+6-1)%6] = 0; goto CS; fi; CS: if :: Slot[(my_place+1)%6] = 1; goto NCS; fi; } proctype P_2() { byte my_place=0; NCS: if :: d_step {my_place = next;next = next+1;} goto p1; fi; p1: if :: d_step {my_place==6-1;next = next-6;} goto p2; :: d_step {my_place!=6-1;my_place = my_place%6;} goto p2; fi; p2: if :: Slot[my_place]==1; goto p3; fi; p3: if :: Slot[(my_place+6-1)%6] = 0; goto CS; fi; CS: if :: Slot[(my_place+1)%6] = 1; goto NCS; fi; } proctype P_3() { byte my_place=0; NCS: if :: d_step {my_place = next;next = next+1;} goto p1; fi; p1: if :: d_step {my_place==6-1;next = next-6;} goto p2; :: d_step {my_place!=6-1;my_place = my_place%6;} goto p2; fi; p2: if :: Slot[my_place]==1; goto p3; fi; p3: if :: Slot[(my_place+6-1)%6] = 0; goto CS; fi; CS: if :: Slot[(my_place+1)%6] = 1; goto NCS; fi; } proctype P_4() { byte my_place=0; NCS: if :: d_step {my_place = next;next = next+1;} goto p1; fi; p1: if :: d_step {my_place==6-1;next = next-6;} goto p2; :: d_step {my_place!=6-1;my_place = my_place%6;} goto p2; fi; p2: if :: Slot[my_place]==1; goto p3; fi; p3: if :: Slot[(my_place+6-1)%6] = 0; goto CS; fi; CS: if :: Slot[(my_place+1)%6] = 1; goto NCS; fi; } proctype P_5() { byte my_place=0; NCS: if :: d_step {my_place = next;next = next+1;} goto p1; fi; p1: if :: d_step {my_place==6-1;next = next-6;} goto p2; :: d_step {my_place!=6-1;my_place = my_place%6;} goto p2; fi; p2: if :: Slot[my_place]==1; goto p3; fi; p3: if :: Slot[(my_place+6-1)%6] = 0; goto CS; fi; CS: if :: Slot[(my_place+1)%6] = 1; goto NCS; fi; }