/* ========================================================================
   This module contains the requirements for interoperation, and the checks
   that they are satisfied.
      The important signatures are Agent, Address, Domain, Hop, Link,
   Feature.
======================================================================== */

module alloy/fme/interopRequ
open alloy/fme/interop

-- This module can be used with any version of the interop module.
-- Keeping these files in /Users/pamela/alloy requires setting path to
-- ".:/Users/pamela"

/* ========================================================================
   SECTION 12.  SANITY CHECKS
      Section 12 consists of assertions about the environment.  Their 
   purpose is simply to ensure the validity of the modeling.
======================================================================== */

assert ConnectedIsEquivalence { all c: Connections |
   (all h: Hop | h in h.(c.connected) ) &&
   (all h1,h2: Hop | h1 in h2.(c.connected) => h2 in h1.(c.connected)) &&
   (all h1,h2,h3: Hop | 
      h2 in h1.(c.connected) && h3 in h2.(c.connected) =>
      h3 in h1.(c.connected) )
}
-- check ConnectedIsEquivalence for 4
--    but 3 Domain,6 Feature,10 Agent,6 Address,4 Hop,3 Link
-- checked with no optional constraints

/* ========================================================================
   SECTION 13.  LIMITATIONS TO THE SCOPE OF THE STUDY, THEIR CONSEQUENCES
======================================================================== */

fact { Feature = InteropFeature }
-- All features are interoperation features.

assert UnidirectionalChains { all l: Link |
      (l.agent = l.oneHop.acceptor && l.agent = l.anotherHop.initiator) ||
      (l.agent = l.oneHop.initiator && l.agent = l.anotherHop.acceptor) 
}
-- check UnidirectionalChains for 4
--    but 3 Domain,6 Feature,10 Agent,6 Address,4 Hop,3 Link
-- checked with no optional constraints

/* ========================================================================
   SECTION 14.  THE REACHABILITY REQUIREMENT
   Checks are done with, at most, constraints for reachability.
======================================================================== */

assert Reachability { 
   all c: Connections, g1, g2: Client, h: Hop, a: Address, d: Domain |
      g1 = h.initiator && d = h.domain && a = h.target &&
      (a->d) in g2.knownAt
   => (some h2: Hop | g2 = h2.acceptor && (h->h2) in c.connected)
}
-- If a client is requesting a connection to an address in a domain
-- known as a way of reaching another client, then the first client is
-- connected to the second client through that request.

-- check Reachability for 3
--    but 3 Domain,4 Feature,7 Agent,5 Address,3 Hop,2 Link
-- checked

-- check Reachability for 3
--    but 2 Domain,2 Feature,4 Agent,4 Address,4 Hop,3 Link

/* ========================================================================
   SECTION 15.  THE RETURNABILITY REQUIREMENT
   Checks are done with, at most, constraints for returnability.
======================================================================== */

assert Returnability {
   all c: Connections, g1, g2: Client, h1, h2, h3: Hop |
      h1.initiator = g1 && h2.acceptor = g2 && (h1->h2) in c.connected &&
      h3.initiator = g2 && h3.domain = h2.domain && h3.target = h2.source 
   => (some h4: Hop | h4.acceptor = g1 && (h3->h4) in c.connected)       
}
-- If one client is connected to another client, and if the second client
-- is requesting a return connection using the domain and source address
-- it has received, then the second client is also connected to the first
-- client through the return request.

assert ReachReturnability {
   all c: Connections, g1, g2: Client, h1, h2: Hop | 
      h1.initiator = g1 && h2.acceptor = g2 && (h1->h2) in c.connected
   => (h2.source->h2.domain) in g1.(c.reachedBy)
}
-- This is a lemma that can be used, in conjunction with reachability minus
-- Constraint 4, to imply returnability.

-- check ReachReturnability for 3
--    but 3 Domain,4 Feature,7 Agent,5 Address,3 Hop,2 Link
-- checked

/* ========================================================================
   SECTION 16.  THE NONUNIQUENESS REQUIREMENT
   Should be instantiated with all optional constraints in force.
======================================================================== */

pred NonUniqueness (g1, g2: Client, d1, d2: Domain, a: Address) {
   (a->d1) in g1.knownAt && (a->d2) in g2.knownAt }

/* ========================================================================
   SECTION 17.  INSTANCES
======================================================================== */

pred ThreeInteroperationIsReturnedPlus (
   disj h1, h2, h3, h4, h5, h6: Hop, disj g1, g2, g3: Client) {
   some c: Connections, a1, a2, a3: Address | {
   (h1->h2) in c.atomConnected
   (h2->h3) in c.atomConnected
   (h4->h5) in c.atomConnected
   (h5->h6) in c.atomConnected
   h1.domain = h6.domain && h2.domain = h5.domain && h3.domain = h4.domain
   h1.domain != h2.domain && h2.domain != h3.domain && h1.domain!=h3.domain
   h4.target = h3.source
   (h1.initiator + h6.acceptor) = g1
   (h4.initiator + h3.acceptor) = g2
   h1.source = a1 && h1.target = a2
   h2.source = a2 && h2.target = a3
   h3.source = a3 && h3.target = a1
   (h1.domain).space = (h2.domain).space
   (h2.domain).space = (h3.domain).space
   (h3.domain).space = (h1.domain).space
   g1 in a1.((h1.domain).map)
   g2 in a1.((h3.domain).map)
   g3 in a1.((h2.domain).map)
} }
run ThreeInteroperationIsReturnedPlus for 3
   but 3 Domain,4 Feature,7 Agent,3 Address,6 Hop,4 Link
-- instantiated with all optional constraints
-- an instance is Figure 4 in the paper

/*
pred VPN (
   disj h1, h2, h3, h4: Hop, disj g1, g2: Client, 
   disj a1, a2, a3, a4: Address, c: Connections, f: InteropFeature) {
{  (h1->h2) in c.atomConnected
   (h2->h3) in c.atomConnected
   h1.domain = h3.domain && h1.domain != h2.domain
   (h1.initiator + h4.acceptor) = g1
   (h3.acceptor + h4.initiator) = g2
   a1 = h1.source && a1 = h2.source && a1 = h3.source && a1 = h4.target
   a2 = h1.target && a3 = h2.target && a3 = h3.target && a3 = h4.source
   f.domain = h1.domain && f.toDomain = h2.domain
   a2.(f.interTrans) = a3.(f.interTrans)
   a1.(f.interTrans) = a4.(f.interTrans)
   (a2 + a4)   in h1.domain.targetOnly
   (a2 + a4)   in f.remote
   (a1 + a3) ! in h1.domain.targetOnly
   no h2.domain.targetOnly
} }
run VPN for 2
   but 2 Domain,2 Feature,4 Agent,4 Address,4 Hop,2 Link,3 Step
*/
-- instantiated with TOinterop.als, all optional constraints
-- does not compile with interop.als
-- an instance is Figure 5 in the paper