MODULE main
 VAR
   semaphore : boolean;
   proc1     : process user(semaphore);
   proc2     : process user(semaphore);
 ASSIGN
   init(semaphore) := FALSE;
 SPEC AG ! (proc1.state = critical & proc2.state = critical)
 SPEC AG (proc1.state = entering -> AF proc1.state = critical)
MODULE user(semaphore)
 VAR
   state : {idle, entering, critical, exiting};
 ASSIGN
   init(state) := idle;
   next(state) :=
    case
     state = idle : {idle, entering}; 
     state = entering & !semaphore : critical;
     state = critical : {critical, exiting};
     state = exiting : idle;
     TRUE    : state ;
     esac;
    next(semaphore) :=
  case
    state = entering : TRUE;
    state = exiting  : FALSE;
       TRUE             : semaphore;
     esac;
 FAIRNESS
   running