semaphore.smv

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)

SPEC EF !(proc1.state = critical & proc2.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;

JUSTICE
	state = critical
--  running