uni/fmi/fmi23block4/ex1.smv

MODULE main
VAR
  semaphore : boolean;
  proc1 : process user(semaphore);
  proc2 : process user(semaphore);
ASSIGN
  init(semaphore) := FALSE;

-- safety property: for all executions, both states cannot be critical at the same time
SPEC AG !(proc1.state = critical & proc2.state = critical)
-- liveness property: for all executions, if proc2 enters, it must eventually become critical
LTLSPEC G (proc2.state = entering -> F 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;			
FAIRNESS
  running