MODULE main
 VAR
   semaphore : boolean;
   proc1     : process user(semaphore);
   proc2     : process user(semaphore);
 ASSIGN
   init(semaphore) := FALSE;
 LTLSPEC G ! (proc1.state = critical & proc2.state = critical)
 LTLSPEC G (proc1.state = entering -> F 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