mdp
label “a” = (q=2 | q=5);
label “b” = (q=3 | q=4 | q=5);
module General
q : [0..5];
[] (q=0) -> (q’=1);
[] (q=0) -> (q’=2);
[] (q=0) -> (q’=4);
[] (q=1) -> (q’=3);
[] (q=3) -> (q’=3);
[] (q=3) -> (q’=1);
[] (q=2) -> (q’=5);
[] (q=4) -> (q’=0);
[] (q=4) -> (q’=4);
[] (q=4) -> (q’=5);
[] (q=5) -> (q’=4);
[] (q=5) -> (q’=5);
endmodule