HOLD_PREVIOUS

TYPE
   T#user#state: ENUM {idle,entering,critical,exiting};

MODULE SYSTEM()
{
VAR
   semaphore: BOOLEAN;

   ((
       v#SYSTEM#semaphore(semaphore)
    ||| user(semaphore)  )
    ||| user(semaphore)  )

}

MODULE user(semaphore: BOOLEAN)
{
VAR
   state: T#user#state;

   (
       v#user#state(state, semaphore)
    || v#user#semaphore(semaphore, state)  )

}

MODULE v#SYSTEM#semaphore(semaphore: BOOLEAN)
{
VAR
   __init: BOOLEAN INITVAL TRUE;

TRANS T_semaphore_0:
    enable:   __init;
    relation: (semaphore'=0) /\ !__init';

TRANS T_semaphore_1:
    enable:   !__init;
    relation: semaphore'=FALSE \/ semaphore'=TRUE;

}

MODULE v#user#state(state: T#user#state, semaphore: BOOLEAN)
{
VAR
   __init: BOOLEAN INITVAL TRUE;

TRANS T_state_0:
    enable:   __init;
    relation: (state'=idle) /\ !__init';

TRANS T_state_1:
    enable:   !__init /\ (state=idle);
    relation: state'=idle \/ state'=entering;

TRANS T_state_2:
    enable:   !__init /\ !(state=idle) /\ (state=entering /\ !semaphore);
    relation: state'=critical;

TRANS T_state_3:
    enable:   !__init /\ !(state=idle) /\ !(state=entering /\ !semaphore) /\ (state=critical);
    relation: state'=critical \/ state'=exiting;

TRANS T_state_4:
    enable:   !__init /\ !(state=idle) /\ !(state=entering /\ !semaphore) /\ !(state=critical) /\ (state=exiting);
    relation: state'=idle;

TRANS T_state_5:
    enable:   !__init /\ !(state=idle) /\ !(state=entering /\ !semaphore) /\ !(state=critical) /\ !(state=exiting);
    relation: state'=state;

}

MODULE v#user#semaphore(semaphore: BOOLEAN, state: T#user#state)
{
VAR
   __init: BOOLEAN INITVAL TRUE;

TRANS T_semaphore_0:
    enable:   __init;
    relation: (semaphore'=FALSE \/ semaphore'=TRUE) /\ !__init';

TRANS T_semaphore_1:
    enable:   !__init /\ (state=entering);
    relation: semaphore'=1;

TRANS T_semaphore_2:
    enable:   !__init /\ !(state=entering) /\ (state=exiting);
    relation: semaphore'=0;

TRANS T_semaphore_3:
    enable:   !__init /\ !(state=entering) /\ !(state=exiting);
    relation: semaphore'=semaphore;

}