HOLD_PREVIOUS

TYPE

state: ENUM {idle , entering , critical , exiting};

VAR

semaphore: boolean INITVAL false;


MODULE USER(){

VAR

user_state: state INITVAL idle;

	TRANS NON_DETERMINISTIC_IDLE_OR_ENTERING:
		enable: user_state = idle;
	        assign: user_state' := {idle,entering};	--relation: ((user_state' = idle) \/ (user_state' = entering));

	TRANS ENTERING_AND_SEMAPHOR_IS_FALSE:
		enable: ((user_state = entering) /\ (semaphore = false));
		assign: user_state' := critical;
			semaphore' := true;

	TRANS ENTERING_BUT_SEMAPHOR_IS_TRUE:
		enable: ((user_state = entering) /\ (semaphore = true));
		assign: user_state' := entering;

	TRANS NON_DETERMINISTIC_CRITICAL_OR_EXITING:
		enable: user_state = critical;
		assign: user_state' := {critical,exiting};

	TRANS RETURN_TO_IDLE_AND_FREE_SEMAPHORE:
		enable: user_state = exiting;
		assign: user_state' := idle;
			semaphore' := false;
}

MODULE SYSTEM(){

	(USER() ||| USER())
}