MODULE main
VAR
     request: boolean;
     stateA: {ready, busy};
ASSIGN
     init(stateA) := ready;
     next(stateA) := case
			stateA=ready & request: busy;
			1: {ready, busy};
		esac;

FAIRNESS (stateA=busy);
FAIRNESS (stateA=ready);

SPEC AF stateA=busy

SPEC EF stateA=busy

SPEC AG(request -> AF (stateA = busy))
  
LTLSPEC G(request -> F (stateA=busy))