MODULE main
VAR
  right 		: boolean;
  left  		: boolean;
  alwaysTrue 	: boolean;
  alwaysFalse	: boolean;
  
ASSIGN
  init(alwaysTrue)  := TRUE;
  init(alwaysFalse) := FALSE;	
  init(right) := TRUE;
  next(right) := case  
					right = FALSE                 : {TRUE, FALSE};
					right = TRUE   & !left 	  	  : TRUE;
					right = TRUE   & left         : FALSE;
				esac;
				
  init(left)  := TRUE;
  next(left)  := case  
					left  = FALSE  & !right       : FALSE;
					left  = FALSE  & right 	  	  : TRUE;
					left  = TRUE           		  : FALSE;
				esac;

CTLSPEC 
		EF(right) -> EG(left)
		--EF(right) -> EG(left)
		--alwaysFalse  -> EG(left)		
		--EG(right -> EG(left))
		--AG(right -> left)
		--AX(right -> left)