-- CSP model of the SpringSource Application Platform phase manager
-- This is currently work in progress, so don't trust it!

-- Limited sets of bundles, services, and application contexts for model-checking purposes.

--channel a, b, c, d, e, f, g, h, i, j, k, l

--T = ( b -> e -> g -> i -> STOP) [|{| i |}|] ( c -> f -> h -> i -> STOP)
--U = a -> e -> j -> STOP
--V = ( d -> f -> k -> l -> STOP ) [|{| l |}|] ( j -> l -> STOP )

--Sys = ( T [|{| e |}|] U ) [|{| f, j |}|] V

-- Deployer

datatype Bundle = b1 | b2

channel s, a, b : Bundle
channel started, deployed

Deploy = ( [|{ started }|] i : Bundle @ ( s.i -> started -> STOP ) ) [|{ started }|]
         (started -> ( [|{ deployed }|] i : Bundle @ ( a.i -> b.i -> deployed -> STOP ) ))

B(i) = s.i -> b.i -> STOP
AC(i) = s.i -> a.i -> STOP

DeployerSys = ( Deploy [|{| s, b |}|] (||| i : Bundle @ B(i)) ) [|{| s, a |}|] (||| i : Bundle @ AC(i))