/* ========================================================================
   The subject of this model is a connection service providing domain
   interoperation.
      This module differs from the main version by having a target-only
   category of addresses.
      This module also differs from the main version by using a stepwise
   version of reachedBy, just for variety.  As a result, it depends on the
   ordering module from the Alloy library.
======================================================================== */

module alloy/fme/TOinterop
open alloy/ordering[Step] as ord

/* ========================================================================
   SECTION 1.  AGENTS
======================================================================== */

abstract sig Agent { attachments: set Domain }
-- An agent is any active entity that participates directly in network
-- connections.  It can be hardware or software.  Its attachments are the
-- domains to which it is attached, and which it can call upon to make
-- connections.

sig Server extends Agent { }
-- A server is an agent that is service-controlled.

sig Client extends Agent { knownAt: Address -> Domain }
-- A client is an agent that is user-controlled.
-- Note that clients and servers participate symmetrically in 
-- network connections; we use "client" rather than "user" simply because we
-- need the latter word for another purpose.  
-- A client is "known at" certain published addresses in certain domains.  
-- Other clients will use these addresses to request connections to it.  

fact { knownAt: Client lone -> (Address -> Domain) }
-- An address in a domain cannot be advertised as reaching more than one
-- client.

/* ========================================================================
   SECTION 2.  ADMINISTRATIVE DOMAINS
======================================================================== */

sig Address { }

sig Domain {
   space: set Address,
   targetOnly: set space,
   map: space -> Agent 
}
-- The address "space" of a domain contains all the addresses that can be 
-- used in the domain's protocol.
-- The "map" of a domain maps its addresses to agents.

fact { all d: Domain, g: Agent |
   g in Address.(d.map) => d in g.attachments }
-- If a domain maps an address to an agent, that agent is attached to the
-- domain.

/* ========================================================================
   SECTION 3.  HOPS
======================================================================== */

sig Hop { 
   domain: Domain, 
   initiator, acceptor: Agent, 
   source, target: Address } {
   domain in initiator.attachments && domain in acceptor.attachments
-- The protocol of a domain creates connections called hops between agents 
-- attached to it.
-- Note that a hop can have the same initiator and acceptor, if the 
-- domain's routing happens to work that way.

   (source + target) in domain.space
-- The source and target addresses of the hop must be in the hop domain's
-- address space.

   acceptor in target.(domain.map)
-- A hop is routed to an agent that its target address maps to.  This is
-- the "routing algorithm" for a domain with no subscription features.  It
-- will need to be changed for domains with subscription features.

   source !in domain.targetOnly
-- This is the meaning of a target-only address.
}

/* ========================================================================
   SECTION 4.  LINKS
======================================================================== */

abstract sig End {}
one sig Init, Accept extends End {}

sig Link { 
   agent: Server, 
   oneHop, anotherHop: Hop,
   oneEnd, anotherEnd: End } {
   oneHop != anotherHop
   oneEnd in Init => agent = oneHop.initiator
   oneEnd in Accept => agent = oneHop.acceptor
   anotherEnd in Init => agent = anotherHop.initiator
   anotherEnd in Accept => agent = anotherHop.acceptor
}
-- A link connects two distinct hops of an agent, within the agent.  We
-- consider only links made by servers.
-- Note that it is necessary to distinguish which end of a hop is being
-- linked because of the possibility that both ends of a hop are the same
-- agent.

fact { all g: Server, h: Hop | lone l: Link | 
   (h = l.oneHop && Init = l.oneEnd) ||
   (h = l.anotherHop && Init = l.anotherEnd)
}
fact { all g: Server, h: Hop | lone l: Link | 
   (h = l.oneHop && Accept = l.oneEnd) ||
   (h = l.anotherHop && Accept = l.anotherEnd)
}
-- In a server, an end of a hop can participate in at most one link.

/* ========================================================================
   SECTION 5.  FEATURES
======================================================================== */

abstract sig Feature { domain: Domain, servers: set Server }
-- Each feature belongs to a domain.
-- Each feature has at least one server.

fact { servers: Feature one -> some Server }
-- Every server is a server of exactly one feature.  This means that the
-- purpose of routing a particular hop to a particular server is clear.
-- This simplifies the model, and it is straightforward to change to a more
-- efficient implementation in which a server can have multiple purposes..

/* ========================================================================
   SECTION 6.  FUNCTIONS OF INTEROPERATION FEATURES
======================================================================== */

sig InteropFeature extends Feature {
   toDomain: Domain,
   exported, imported, remote, local: set Address,
   interTrans: exported some -> some imported } {
   domain != toDomain
   exported in domain.space   && remote in exported 
   imported in toDomain.space && local  in imported 
   remote.interTrans = local
}
-- Interoperation means reaching a distinct domain.
-- Note from the multiplicity markings that exported and imported are the
-- true domain and range of interTrans, which translates addresses in the
-- feature's domain to the corresponding addresses in its toDomain.
-- remote contains the addresses of the feature's domain that trigger
-- the feature, and local is the image of remote in the toDomain.

fact { all f: InteropFeature, g: Agent, h1: Hop |
   g in f.servers && h1.acceptor = g && 
   h1.domain = f.domain && h1.target in f.remote
   =>
   (some l: Link, h2: Hop |
      l.agent = g && l.oneHop = h1 && l.anotherHop = h2 &&
      h2.domain = f.toDomain && h2.initiator = g &&
      h2.target in (h1.target).(f.interTrans) &&
      (h1.source in f.exported => h2.source in (h1.source).(f.interTrans))
   )
}
-- If an interoperation server receives a hop targeted to an address it is
-- triggered by and in the server's domain, then the server makes a 
-- continuing link and hop into the reached domain.

fact { all f: InteropFeature, g: Agent, h: Hop |
   g in f.servers && h.acceptor = g && 
   ( !(h.domain = f.domain) || !(h.target in f.remote) )
   =>
   no l: Link | l.agent = g && h in l.(oneHop + anotherHop)
}
-- If an interoperation server receives a hop not describable as above,
-- then the server cannot link the hop to anything.
-- A hop can have an "unused" target address, because no constraint
-- prevents its domain from routing it to an interoperation server.  This
-- rule ensures that when this happens, the server will behave properly.

fact { all f: InteropFeature, g: Agent, l: Link |
   g in f.servers && g = l.agent =>
      l.oneEnd = Accept || l.anotherEnd = Accept }
-- An interoperation server only creates links where one of the linked hops
-- was received by the server.

/* ========================================================================
   SECTION 7.  USE OF INTEROPERATION FEATURES
======================================================================== */

pred Foreign (a: Address, d: Domain) {
   some f: InteropFeature | d = f.domain && a in f.remote }
-- A foreign address in a domain is defined as one that triggers some
-- interoperation feature in that domain.

pred Native (a: Address, d: Domain ) {
   some g: Client | g in a.(d.map) }
-- A native address in a domain is defined as one that maps to a client.
-- This definition is provided for completeness only.

fact { all a: Address, d: Domain | let s = a.(d.map) |
   Foreign(a,d) => 
      some s && 
      (all g: Agent | g in s =>
         (some f: InteropFeature | 
            d = f.domain && a in f.remote && g in f.servers) )
}
-- If an address is foreign in a domain, it maps to something in that
-- domain, and everything it maps to is a server of an interoperation 
-- feature triggered by it.
--    This is written to allow more than one interoperation feature 
-- triggered by the same address.  Excluding this case, if necessary, must
-- be done explicitly.

/* ========================================================================
   SECTION 8.  CONNECTIONS
======================================================================== */

sig Step { }

one sig Connections {
atomConnected, connected: Hop -> Hop,
reachedBy: Client -> Address -> Domain,
reachedByStep: Client -> Address -> Domain -> Step } {
atomConnected = { h1, h2: Hop |
   some l: Link | l.(oneHop + anotherHop) = h1 + h2 }
connected = *atomConnected
reachedBy = reachedByStep.ord/last()
all g: Client, a: Address, d: Domain |
   (a->d) in g.(reachedByStep.ord/first()) iff g in a.(d.map)
all g: Client, a: Address, d: Domain, s: Step - ord/first() |
   (a->d) in g.(reachedByStep.s) iff
   (
      (a->d) in g.(reachedByStep.ord/prev(s))
   ||
      some f: InteropFeature | f.domain = d && a in f.remote &&
      some ( (a.(f.interTrans)->f.toDomain) & g.(reachedByStep.ord/prev(s)) )
   )
}
-- This declares a unique object containing only derived fields.  
-- (g->a->d) is in reachedBy if and only if the client g can be reached
-- from address a in domain d, either directly or through interoperation.
-- The stepwise definition of reachedBy ensures that its value is a least
-- fixed point.

/* ========================================================================
   SECTION 9.  CONSTRAINTS NECESSARY FOR REACHABILITY AND RETURNABILITY
======================================================================== */

fact Constraint1 { all a: Address, d: Domain | 
   some ( a.(d.map) & Client ) => one a.(d.map) }
-- If an address maps to a client in a domain, then it does not map to
-- anything else.  This means that a client attached to a domain can be
-- addressed unambiguously in that domain.

fact Constraint2 {
   all f: InteropFeature, a: Address | lone a.(f.interTrans) }
-- Interoperation address translation is a partial function.

fact Constraint3 { all a: Address, d: Domain | 
   lone f: InteropFeature | f.domain = d && a in f.remote }
-- In each domain, each address triggers at most one interoperation 
-- feature.

/* ========================================================================
   SECTION 10.  CONSTRAINT NECESSARY FOR REACHABILITY ALONE
======================================================================== */
 
fact Constraint4 { 
   all c: Connections, g: Client | g.knownAt in g.(c.reachedBy) }
-- If a client is known at an address in a domain, it is reached by that
-- address in that domain.

/* ========================================================================
   SECTION 11.  CONSTRAINTS NECESSARY FOR RETURNABILITY ALONE
======================================================================== */

fact Constraint5 { all h: Hop |
   h.initiator in Client => h.source in ((h.domain).map).(h.initiator) }
-- If a hop is initiated by a client, its source must be an address of the
-- client in the domain.

fact Constraint6 { all f: InteropFeature | f.domain.space in f.exported }
-- Every interoperation feature's exported set must include the address
-- space of its domain.  This prevents the loss of source information.

pred PartnerTo (f1, f2: InteropFeature) {
   f1.domain = f2.toDomain && f1.toDomain = f2.domain &&
   let newlocal = (f1.remote - f1.domain.targetOnly).(f1.interTrans) |
   (f1.imported - newlocal) in f2.remote
}

fact Constraint7 { 
   all f1: InteropFeature | some f2: InteropFeature | PartnerTo(f1,f2) }
-- Each interoperation feature has a partner that serves as its "return 
-- feature".

fact Constraint8 { all f1, f2: InteropFeature | PartnerTo(f1,f2) =>
   all a: f1.domain.space |
   a in f1.domain.targetOnly || (a.(f1.interTrans)).(f2.interTrans) = a
}
-- The address translation of interoperation is invertible.