mdp

label “sc1”= (q=9);
label “sc2”= (r=9);

global turn:[1..2] init 1;

module P1
want1: bool init false;
q:[2..11] init 2;
[] (q=2) -> (q’=3);
[] (q=3) -> (want1’= true) & (q’=4);
[] (q=4) & !(want2) -> (q’=9);
[] (q=4) & want2 -> (q’=5);
[] (q=5) & (turn=1) -> (q’=4);
[] (q=5) & (turn=2) -> (q’=6);
[] (q=6) -> (want1’=false) & (q’=7);
[] (q=7) & (turn=2) -> (q’=7);
[] (q=7) & (turn =1) -> (q’=8);
[] (q=8) -> (want1’=true) & (q’=4);
[] (q=9) -> (q’=10);
[] (q=10) -> (turn’=2) & (q’=11);
[] (q=11) -> (want1’=false) & (q’=2);
endmodule

module P2
want2: bool init false;
r:[2..11] init 2;
[] (r=2) -> (r’=3);
[] (r=3) -> (want2’= true) & (r’=4);
[] (r=4) & !(want1) -> (r’=9);
[] (r=4) & want1 -> (r’=5);
[] (r=5) & (turn=2) -> (r’=4);
[] (r=5) & (turn=1) -> (r’=6);
[] (r=6) -> (want2’=false) & (r’=7);
[] (r=7) & (turn=1) -> (r’=7);
[] (r=7) & (turn =2) -> (r’=8);
[] (r=8) -> (want2’=true) & (r’=4);
[] (r=9) -> (r’=10);
[] (r=10) -> (turn’=1) & (r’=11);
[] (r=11) -> (want2’=false) & (r’=2);
endmodule