Module System

type T#user#state = {idle,entering,critical,exiting}


Module v#SYSTEM#semaphore :
external out semaphore : bool 
local __init : bool where __init = true


Transition T_semaphore_0 NoFairness:
enable __init
modrel (semaphore'=0)/\!__init'

Transition T_semaphore_1 NoFairness:
enable !__init
modrel semaphore'=false\/semaphore'=true
EndModule


Module v#user#state :
external out state : T#user#state 
external out semaphore : bool 
local __init : bool where __init = true
export T_state_0_T_semaphore_0,T_state_0_T_semaphore_1,T_state_0_T_semaphore_2,T_state_0_T_semaphore_3,T_state_1_T_semaphore_0,T_state_1_T_semaphore_1,T_state_1_T_semaphore_2,T_state_1_T_semaphore_3,T_state_2_T_semaphore_0,T_state_2_T_semaphore_1,T_state_2_T_semaphore_2,T_state_2_T_semaphore_3,T_state_3_T_semaphore_0,T_state_3_T_semaphore_1,T_state_3_T_semaphore_2,T_state_3_T_semaphore_3,T_state_4_T_semaphore_0,T_state_4_T_semaphore_1,T_state_4_T_semaphore_2,T_state_4_T_semaphore_3,T_state_5_T_semaphore_0,T_state_5_T_semaphore_1,T_state_5_T_semaphore_2,T_state_5_T_semaphore_3

Transition T_state_5_T_semaphore_3 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\!(state=critical)/\!(state=exiting)
modrel state'=state

Transition T_state_5_T_semaphore_2 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\!(state=critical)/\!(state=exiting)
modrel state'=state

Transition T_state_5_T_semaphore_1 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\!(state=critical)/\!(state=exiting)
modrel state'=state

Transition T_state_5_T_semaphore_0 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\!(state=critical)/\!(state=exiting)
modrel state'=state

Transition T_state_4_T_semaphore_3 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\!(state=critical)/\(state=exiting)
modrel state'=idle

Transition T_state_4_T_semaphore_2 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\!(state=critical)/\(state=exiting)
modrel state'=idle

Transition T_state_4_T_semaphore_1 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\!(state=critical)/\(state=exiting)
modrel state'=idle

Transition T_state_4_T_semaphore_0 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\!(state=critical)/\(state=exiting)
modrel state'=idle

Transition T_state_3_T_semaphore_3 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\(state=critical)
modrel state'=critical\/state'=exiting

Transition T_state_3_T_semaphore_2 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\(state=critical)
modrel state'=critical\/state'=exiting

Transition T_state_3_T_semaphore_1 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\(state=critical)
modrel state'=critical\/state'=exiting

Transition T_state_3_T_semaphore_0 NoFairness:
enable !__init/\!(state=idle)/\!(state=entering/\!semaphore)/\(state=critical)
modrel state'=critical\/state'=exiting

Transition T_state_2_T_semaphore_3 NoFairness:
enable !__init/\!(state=idle)/\(state=entering/\!semaphore)
modrel state'=critical

Transition T_state_2_T_semaphore_2 NoFairness:
enable !__init/\!(state=idle)/\(state=entering/\!semaphore)
modrel state'=critical

Transition T_state_2_T_semaphore_1 NoFairness:
enable !__init/\!(state=idle)/\(state=entering/\!semaphore)
modrel state'=critical

Transition T_state_2_T_semaphore_0 NoFairness:
enable !__init/\!(state=idle)/\(state=entering/\!semaphore)
modrel state'=critical

Transition T_state_1_T_semaphore_3 NoFairness:
enable !__init/\(state=idle)
modrel state'=idle\/state'=entering

Transition T_state_1_T_semaphore_2 NoFairness:
enable !__init/\(state=idle)
modrel state'=idle\/state'=entering

Transition T_state_1_T_semaphore_1 NoFairness:
enable !__init/\(state=idle)
modrel state'=idle\/state'=entering

Transition T_state_1_T_semaphore_0 NoFairness:
enable !__init/\(state=idle)
modrel state'=idle\/state'=entering

Transition T_state_0_T_semaphore_3 NoFairness:
enable __init
modrel (state'=idle)/\!__init'

Transition T_state_0_T_semaphore_2 NoFairness:
enable __init
modrel (state'=idle)/\!__init'

Transition T_state_0_T_semaphore_1 NoFairness:
enable __init
modrel (state'=idle)/\!__init'

Transition T_state_0_T_semaphore_0 NoFairness:
enable __init
modrel (state'=idle)/\!__init'
EndModule


Module v#user#semaphore :
external out semaphore : bool 
external out state : T#user#state 
local __init : bool where __init = true
export T_state_0_T_semaphore_0,T_state_0_T_semaphore_1,T_state_0_T_semaphore_2,T_state_0_T_semaphore_3,T_state_1_T_semaphore_0,T_state_1_T_semaphore_1,T_state_1_T_semaphore_2,T_state_1_T_semaphore_3,T_state_2_T_semaphore_0,T_state_2_T_semaphore_1,T_state_2_T_semaphore_2,T_state_2_T_semaphore_3,T_state_3_T_semaphore_0,T_state_3_T_semaphore_1,T_state_3_T_semaphore_2,T_state_3_T_semaphore_3,T_state_4_T_semaphore_0,T_state_4_T_semaphore_1,T_state_4_T_semaphore_2,T_state_4_T_semaphore_3,T_state_5_T_semaphore_0,T_state_5_T_semaphore_1,T_state_5_T_semaphore_2,T_state_5_T_semaphore_3

Transition T_state_5_T_semaphore_3 NoFairness:
enable !__init/\!(state=entering)/\!(state=exiting)
modrel semaphore'=semaphore

Transition T_state_5_T_semaphore_2 NoFairness:
enable !__init/\!(state=entering)/\(state=exiting)
modrel semaphore'=0

Transition T_state_5_T_semaphore_1 NoFairness:
enable !__init/\(state=entering)
modrel semaphore'=1

Transition T_state_5_T_semaphore_0 NoFairness:
enable __init
modrel (semaphore'=false\/semaphore'=true)/\!__init'

Transition T_state_4_T_semaphore_3 NoFairness:
enable !__init/\!(state=entering)/\!(state=exiting)
modrel semaphore'=semaphore

Transition T_state_4_T_semaphore_2 NoFairness:
enable !__init/\!(state=entering)/\(state=exiting)
modrel semaphore'=0

Transition T_state_4_T_semaphore_1 NoFairness:
enable !__init/\(state=entering)
modrel semaphore'=1

Transition T_state_4_T_semaphore_0 NoFairness:
enable __init
modrel (semaphore'=false\/semaphore'=true)/\!__init'

Transition T_state_3_T_semaphore_3 NoFairness:
enable !__init/\!(state=entering)/\!(state=exiting)
modrel semaphore'=semaphore

Transition T_state_3_T_semaphore_2 NoFairness:
enable !__init/\!(state=entering)/\(state=exiting)
modrel semaphore'=0

Transition T_state_3_T_semaphore_1 NoFairness:
enable !__init/\(state=entering)
modrel semaphore'=1

Transition T_state_3_T_semaphore_0 NoFairness:
enable __init
modrel (semaphore'=false\/semaphore'=true)/\!__init'

Transition T_state_2_T_semaphore_3 NoFairness:
enable !__init/\!(state=entering)/\!(state=exiting)
modrel semaphore'=semaphore

Transition T_state_2_T_semaphore_2 NoFairness:
enable !__init/\!(state=entering)/\(state=exiting)
modrel semaphore'=0

Transition T_state_2_T_semaphore_1 NoFairness:
enable !__init/\(state=entering)
modrel semaphore'=1

Transition T_state_2_T_semaphore_0 NoFairness:
enable __init
modrel (semaphore'=false\/semaphore'=true)/\!__init'

Transition T_state_1_T_semaphore_3 NoFairness:
enable !__init/\!(state=entering)/\!(state=exiting)
modrel semaphore'=semaphore

Transition T_state_1_T_semaphore_2 NoFairness:
enable !__init/\!(state=entering)/\(state=exiting)
modrel semaphore'=0

Transition T_state_1_T_semaphore_1 NoFairness:
enable !__init/\(state=entering)
modrel semaphore'=1

Transition T_state_1_T_semaphore_0 NoFairness:
enable __init
modrel (semaphore'=false\/semaphore'=true)/\!__init'

Transition T_state_0_T_semaphore_3 NoFairness:
enable !__init/\!(state=entering)/\!(state=exiting)
modrel semaphore'=semaphore

Transition T_state_0_T_semaphore_2 NoFairness:
enable !__init/\!(state=entering)/\(state=exiting)
modrel semaphore'=0

Transition T_state_0_T_semaphore_1 NoFairness:
enable !__init/\(state=entering)
modrel semaphore'=1

Transition T_state_0_T_semaphore_0 NoFairness:
enable __init
modrel (semaphore'=false\/semaphore'=true)/\!__init'
EndModule


Module user :
external out semaphore : bool 
local state : T#user#state 

include v#user#state : ( v#user#state where out state = state,semaphore = semaphore)
 || v#user#semaphore : ( v#user#semaphore where out semaphore = semaphore,state = state)
EndModule


Module user :
external out semaphore : bool 
local state : T#user#state 

include v#user#state : ( v#user#state where out state = state,semaphore = semaphore)
 || v#user#semaphore : ( v#user#semaphore where out semaphore = semaphore,state = state)
EndModule


Module SYSTEM :
local semaphore : bool 

include v#SYSTEM#semaphore : ( v#SYSTEM#semaphore where out semaphore = semaphore)
 || user : ( user where out semaphore = semaphore)
 || user : ( user where out semaphore = semaphore)
EndModule