global turn : [1 .. 2];
module P1
D1 : bool init false;
p : [0..3] init 0;
[] (p=0) -> true;
[] (p=0) -> (p’=1) & (D1’=true);
[] (p=1) -> (p’=2) & (turn’=2);
[] (p=2) & ((turn=1) | (D2=false)) -> (p’=3);
[] (p=2) & ((turn=2) & (D2=true)) -> (p’=2);
[] (p=3) -> (p’=0) & (D1’=false);
endmodule

module P2
D2 : bool init false;
q : [0..3] init 0;
[] (q=0) -> true;
[] (q=0) -> (q’=1) & (D2’=true);
[] (q=1) -> (q’=2) & (turn’=1);
[] (q=2) & ((turn=2) | (D1=false)) -> (q’=3);
[] (q=2) & ((turn=1) & (D1=true)) -> (q’=2);
[] (q=3) -> (q’=0) & (D2’=false);
endmodule