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

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

datatype bundle = b1 | b2
datatype service = s1 | s2 | s3 | s4
datatype application_context = b1ac1 | b1ac2 | b2ac1 | b2ac2

get_app_ctxs(b1) = {b1ac1, b1ac2}
get_app_ctxs(b2) = {b2ac1, b2ac2}

get_services(b1ac1) = {s1, s4}
get_services(b1ac2) = {s2}
get_services(b2ac1) = {s3}
get_services(b2ac2) = {}

-- Bundles
-- The events in this model should be just sufficient to model the interaction between bundles and Spring DM.

channel b_started, b_stopping: bundle

Bundles = let
              Bundle(i) = b_started.i -> b_stopping.i -> Bundle(i) -- recycle bundle to avoid artificial deadlock
          within
              ||| i:bundle @ Bundle(i)

-- Service registry.

channel sr_publish, sr_lookup, sr_retract: service

ServiceRegistration(s) = sr_publish.s -> PublishedServiceRegistration(s)
PublishedServiceRegistration(s) = sr_lookup.s -> PublishedServiceRegistration(s) [] sr_retract.s -> ServiceRegistration(s)

ServiceRegistry = ||| s : service @ ServiceRegistration(s)

-- Application contexts.

channel ac_start, ac_stop, ac_refresh, ac_close, ac_fail, ac_timeout: application_context

-- Recycle application contexts to avoid artifical deadlock, but only within a single bundle start/stop cycle
StopAppCtx(a) = ac_stop.a -> AppCtx(a)

AppCtx(a) = let
                InitAppCtx = ac_refresh.a -> ServiceLookup(a, service) [] ac_fail.a -> StopAppCtx(a)
            within
                ac_start.a -> InitAppCtx

ServiceLookup(a, {}) = ServicePublish(a, {}, {})
ServiceLookup(a, remaining) = let
                                  Timeout = ac_timeout.a -> StopAppCtx(a)
                                  Lookup = (|~| s:remaining @ sr_lookup.s -> ServiceLookup(a, diff(remaining, {s}))) [> Timeout
                              within
                                  ServicePublish(a, inter(remaining, get_services(a)), {}) |~| Lookup

ServicePublish(a, {}, published) = RunningAppCtx(a, published)
ServicePublish(a, remaining, published) = let
                                              PublishMore(s) = ServicePublish(a, diff(remaining, {s}), union(published, {s}))
                                              Publish = |~| s:remaining @ sr_publish.s -> PublishMore(s)
                                          within
                                              RunningAppCtx(a, published) |~| Publish

RunningAppCtx(a, published) = ac_stop.a -> ac_close.a -> ServiceTerm(a, published)

ServiceTerm(a, {}) = AppCtx(a)
ServiceTerm(a, published) = [] s:published @ sr_retract.s -> ServiceTerm(a, diff(published, {s}))

AppCtxs = ||| a:application_context @ AppCtx(a)

-- Multiplex bundle stopped and starting events to application context start and stop events, respectively.

Multiplex(i) = let
                   ac = get_app_ctxs(i)
                   StartAppCtxs({}) = Multiplex(i)
                   StartAppCtxs(acs) = [] a:acs @ ac_start.a -> StartAppCtxs(diff(acs, {a}))
				   StopAppCtxs({}) = Multiplex(i)
                   StopAppCtxs(acs) = [] a:acs @ ac_stop.a -> StopAppCtxs(diff(acs, {a}))
               within
                   b_started.i -> StartAppCtxs(ac) [] b_stopping.i -> StopAppCtxs(ac)

Multiplexer = ||| i:bundle @ Multiplex(i)

-- A system comprising bundles, multiplexer, application contexts, and the service registry.

MultiplexedBundles = Bundles [|{|b_started, b_stopping|}|] Multiplexer
EmbeddedAppCtxs = AppCtxs [|{|sr_publish, sr_lookup, sr_retract|}|] ServiceRegistry

System = MultiplexedBundles [|{|ac_start, ac_stop|}|] EmbeddedAppCtxs

assert System :[ deadlock free [F] ]