Module System

local shared : int where shared = 6
local x : int where x = 0
local y : int where y = 0
local z : bool where z = true


Module A :
local can_change_shared : bool where can_change_shared = true
export ENTER_CRITIC1_EXIT_CRITIC2,EXIT_CRITIC1_ENTER_CRITIC2

Transition EXIT_CRITIC1_ENTER_CRITIC2 NoFairness:
enable !can_change_shared
assign can_change_shared := true

Transition ENTER_CRITIC1_EXIT_CRITIC2 NoFairness:
enable can_change_shared
assign shared := shared+1,can_change_shared := false

Transition NON_CRITIC1 NoFairness:
enable z
assign x := 10
EndModule


Module B :
local can_change_shared : bool where can_change_shared = false
export ENTER_CRITIC1_EXIT_CRITIC2,EXIT_CRITIC1_ENTER_CRITIC2

Transition EXIT_CRITIC1_ENTER_CRITIC2 NoFairness:
enable can_change_shared
assign shared := shared-1,can_change_shared := false

Transition ENTER_CRITIC1_EXIT_CRITIC2 NoFairness:
enable !can_change_shared
assign can_change_shared := true

Transition NON_CRITIC2 NoFairness:
enable z
assign y := 11
EndModule


Module SYSTEM :

include A : ( A )
 || B : ( B )
EndModule