module S1
q : [0..3] init 0;
[a1] (q=0) -> (q’=1);
[a2] (q=1) -> (q’=2);
[a2] (q=2) -> true;
[a1] (q=2) -> (q’=3);
[a2] (q=3) -> (q’=0);
endmodule
module S2
r : [0..2] init 0;
[a1] (r=0) -> (r’=1);
[a3] (r=1) -> true;
[a3] (r=1) -> (r’=2);
[a3] (r=2) -> (r’=0);
endmodule