Module System

type state = {idle,entering,critical,exiting}
local semaphore : bool where semaphore = false


Module USER :
local user_state : state where user_state = idle


Transition NON_DETERMINISTIC_IDLE_OR_ENTERING NoFairness:
enable user_state=idle
modrel (user_state' = idle \/ user_state' = entering)

Transition ENTERING_AND_SEMAPHOR_IS_FALSE NoFairness:
enable ((user_state=entering)/\(semaphore=false))
assign user_state := critical,semaphore := true

Transition ENTERING_BUT_SEMAPHOR_IS_TRUE NoFairness:
enable ((user_state=entering)/\(semaphore=true))
assign user_state := entering

Transition NON_DETERMINISTIC_CRITICAL_OR_EXITING NoFairness:
enable user_state=critical
modrel (user_state' = critical \/ user_state' = exiting)

Transition RETURN_TO_IDLE_AND_FREE_SEMAPHORE NoFairness:
enable user_state=exiting
assign user_state := idle,semaphore := false
EndModule


Module SYSTEM :

include USER : ( USER )
 || USER : ( USER )
EndModule