MODULE main 
VAR
   req1:boolean;
   req2:boolean;
   ack1:boolean;
   ack2:boolean;
ASSIGN
   ack1:= req1;
   ack2:= req2& !req1;
SPEC
  AG( !(ack1 & ack2)) 
SPEC
  AG(req1|req2 -> ack1|ack2)
SPEC
  AG(ack1 ->req1)
SPEC
  AG(ack2 ->req2)
SPEC
  AG(req2 -> !req1)