MODULE main
 VAR
   semaphore : boolean;
   proc1     : process user(semaphore);
   proc2     : process user(semaphore);
 ASSIGN
   init(semaphore) := FALSE;
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
       state = exiting
       TRUE
     esac;
   next(semaphore) :=
     case
       state = entering : TRUE;
       state = exiting  : FALSE;
       TRUE             : semaphore;
     esac;
 FAIRNESS
  running