MODULE main

VAR
  run   : 1..2;
  semaphore : boolean;
  proc1_state :{idle, entering, critical, exiting};
  proc2_state :{idle, entering, critical, exiting};

ASSIGN
  init(run):={1,2};
  next(run):={1,2};

  init(proc1_state) := idle;
  next(proc1_state) :=
    case
      run = 1 & proc1_state = idle                  : {idle, entering};
      run = 1 & proc1_state = entering & !semaphore : critical;
      run = 1 & proc1_state = critical              : {critical, exiting};
      run = 1 & proc1_state = exiting               : idle;
      TRUE                                          : proc1_state;
    esac;

  init(proc2_state) := idle;
  next(proc2_state) :=
    case
      run = 2 & proc2_state = idle                  : {idle, entering};
      run = 2 & proc2_state = entering & !semaphore : critical;
      run = 2 & proc2_state = critical              : {critical, exiting};
      run = 2 & proc2_state = exiting               : idle;
      TRUE                                          : proc2_state;
    esac;

  init(semaphore) := FALSE;
  next(semaphore) :=
    case
      run = 1 & proc1_state = entering : TRUE;
      run = 1 & proc1_state = entering : FALSE;
      run = 2 & proc2_state = entering : TRUE;
      run = 2 & proc2_state = entering : FALSE;
      TRUE                             : semaphore;
    esac;

SPEC AG (! (proc1_state = critical & proc2_state = critical))
SPEC AG (AF (run=1))
SPEC AG (proc1_state = entering -> AF (proc1_state = critical))