Module System

type T#SYSTEM#state = {ready,busy}


Module v#SYSTEM#state :
external out state : T#SYSTEM#state 
external out request : bool 
local __init : bool where __init = true


Transition T_state_0 NoFairness:
enable __init
modrel (state'=ready)/\!__init'

Transition T_state_1 NoFairness:
enable !__init/\(state=ready/\request)
modrel state'=busy

Transition T_state_2 NoFairness:
enable !__init/\!(state=ready/\request)
modrel state'=ready\/state'=busy
EndModule


Module SYSTEM :
local request : bool 
local state : T#SYSTEM#state 

include v#SYSTEM#state : ( v#SYSTEM#state where out state = state,request = request)
EndModule