MODULE main
VAR
   state:{q0, q1, q2, q3, q4};
   input: {R1,D1,R2,D2};
   out: {G1,G2};
ASSIGN
   init(state):=q0;
   next(state):=
      case
        (state=q0) &(input= R1): q1;
        (state=q1) &(out= G1): q2;
        (state=q2) &(input= D1): q0;
        (state=q0) &(input= R2): q3;
        (state=q3) &(out= G2): q4;
        (state=q4) &(input= D2): q0;
        1: state;
      esac;
SPEC
AG EF (state=q0) 
SPEC
AG EF (state=q4)
SPEC
AG AF (state=q4)
SPEC
(state=q1)->AX(state=q2)