/* ========================================================================
A MODEL OF THE PURE-JOIN CHORD ROUTING PROTOCOL IN ALLOY
   Pamela Zave, 14 September 2009
      Copyright AT&T Labs, Inc., 2009.
======================================================================== */

open util/ordering[Time] as trace
open util/ordering[Node] as cycle

/* ========================================================================
TEMPORAL STRUCTURE
   Note that if time has a scope of x, there will be exactly x times, not
x or fewer.  However, there need not be x-1 real events, because Null
events will take up the slack.
======================================================================== */

sig Time { }

abstract sig Event {
   pre:  Time,
   post: Time,
   cause: lone (Event - Null)
}

sig Null extends Event { } { no cause }

fact TemporalStructure {
   all t: Time - trace/last | one e: Event | e.pre = t 
   all t: trace/last | no  e: Event | e.pre = t 
   all e: Event | e.post = (e.pre).next  
}

fact CauseHasSingleEffect { cause in Event lone -> Event }

fact CausePrecedesEffect { 
   all e1, e2: Event | e1 = e2.cause => lt[e1.pre,e2.pre]  }

/* ========================================================================
STRUCTURE OF A RING NETWORK
======================================================================== */

sig Node {
   succ: Node lone -> Time,
   prdc: Node lone -> Time  }
-- A node is unambiguously a member or not.
{  all t: Time | Member[this,t] || NonMember[this,t]  }

pred Member [n: Node, t: Time] {  some n.succ.t  }
pred NonMember [n: Node, t: Time] {
   no n.succ.t && no n.prdc.t  }

pred Between [n1, n2, n3: Node] {
   lt[n1,n3] =>   ( lt[n1,n2] && lt[n2,n3] )
             else ( lt[n1,n2] || lt[n2,n3] )  }

pred OneOrderedCycle [t: Time] {
   let cycleMembers = { n: Node | n in n.(^(succ.t)) } |
      some cycleMembers                               -- at least one cycle
   && (all disj n1, n2: cycleMembers | n1 in n2.(^(succ.t)) )    -- not two
   && (all disj n1, n2, n3: cycleMembers |             -- cycle is globally
         n2 = n1.succ.t => ! Between[n1,n3,n2]         -- ordered
      )
}

pred ConnectedAppendages [t: Time] {
   let members = { n: Node | Member[n,t] } |
   let cycleMembers = { n: Node | n in n.(^(succ.t)) } |
      all na: members - cycleMembers |                          -- na is in
         some nc: cycleMembers | nc in na.(^(succ.t))       -- an appendage
                                                       -- yet reaches cycle
}

pred AntecedentPredecessors [t: Time]  {
   let members = { n: Node | some n.succ.t } |
      all n: members | let antes = (succ.t).n | n.prdc.t in antes
}

pred OrderedAppendages [t: Time] {
   let members = { n: Node | Member[n,t] } |
   let cycleMembers = { n: members | n in n.(^(succ.t)) } |
   let appendSucc = succ.t - (cycleMembers -> Node) |
      all n: cycleMembers |
         all disj a1, a2, a3: (members - cycleMembers) + n |
            (  n in a1.(^appendSucc)
            && a2 = a1.appendSucc
            && (a1 in a3.(^appendSucc) || a3 in a2.(^appendSucc) )
            )  => ! Between[a1,a3,a2]
}

pred Valid [t: Time] { 
      OneOrderedCycle[t]
   && ConnectedAppendages[t] 
   && AntecedentPredecessors[t]
   && OrderedAppendages[t]
}

pred Stable [t: Time] { let members = { n: Node | Member[n,t] } |
   all n1, n2: members | n2 = n1.succ.t <=> n1 = n2.prdc.t
}

pred AllCycle [t: Time] { let members = { n: Node | Member[n,t] } |
   all n1, n2: members | n2 in n1.(^(succ.t))
}

pred Ideal [t: Time] { Valid[t] && Stable[t] }

assert IdealImpliesAllCycle {
   all t: Time | Ideal[t] => AllCycle[t] }
/*
check IdealImpliesAllCycle for 4 but 0 Event, 1 Time -- 601+  150 ms
check IdealImpliesAllCycle for 7 but 0 Event, 1 Time -- 782+79442 ms
*/

/* ========================================================================
SPECIFICATION OF EVENTS
   The specification assumes that events occur only when the ring is valid.
======================================================================== */

abstract sig RingEvent extends Event { node: Node }
sig Join extends RingEvent { } { no cause }
sig Stabilize extends RingEvent { } { no cause }
sig Notify extends RingEvent { newPrdc: Node } { some cause }

fact NonmemberCanJoin { 
   all j: Join, n: j.node, t: j.pre | 
         NonMember[n,t]
      && (some m: Node | Member[m,t] && Between[m,n,m.succ.t] &&
                         n.succ.(j.post) = m.succ.t 
         )
      && no n.prdc.(j.post)
      && no cause:>j
}

fact StabilizeMayChangeSuccessor {
   all s: Stabilize, n: s.node, t: s.pre |
   let newSucc = (n.succ.t).prdc.t       |
         Member[n,t]
      && (  (  some newSucc
            && Between[n,newSucc,n.succ.t]
            )
            -- accept new successor or not
            => n.succ.(s.post) = newSucc else n.succ.(s.post) = n.succ.t
         )
      && (some f: Notify |   f.cause = s
                          && f.node = n.succ.(s.post)
                          && f.newPrdc = n
         )
}

fact NotifyMayChangePredecessor {
   all f: Notify, n: f.node, p: f.newPrdc, t: f.pre |
      (no n.prdc.t || Between[n.prdc.t,p,n])
-- accept new predecessor
      =>   (n.prdc.(f.post) = p && no cause:>f)
-- else do nothing
      else (n.prdc.(f.post) = n.prdc.t && no cause:>f)
}

/* ========================================================================
FRAME CONDITIONS AND CHANGE PREDICATES
======================================================================== */

fact SuccessorFieldFrameCondition {
   all e: Event, n: Node | n.succ.(e.pre) != n.succ.(e.post)
   => (  (e in Stabilize && e.node = n)
      || (e in Join && e.node = n)
      )
}

fact PredecessorFieldFrameCondition {
   all e: Event, n: Node | n.prdc.(e.pre) != n.prdc.(e.post)
   => (e in Notify && e.node = n)
}

pred StabilizationWillChangeSuccessor [n, newSucc: Node, t: Time] {
   newSucc = (n.succ.t).prdc.t &&
   some newSucc && Between[n,newSucc,n.succ.t]                       
}

pred StabilizationShouldChangePredecessor [n1, n2: Node, t: Time] {
   let queried = n1.succ.t |
   let newSucc = (n1.succ.t).prdc.t |
      n2 = (  some newSucc && Between[n1,newSucc,n1.succ.t] 
           => newSucc else queried
           )
   && (no n2.prdc.t || Between[n2.prdc.t,n1,n2]) 
}

/* ========================================================================
VALIDATION OF RING STRUCTURE

pred NoCycle [t: Time] { 
   let cycleMembers = { n: Node | n in n.(^(succ.t)) } |
      no cycleMembers 
   && ConnectedAppendages[t] 
   && AntecedentPredecessors[t]
   && OrderedAppendages[t]
}
run NoCycle for 1 but 0 Event, 1 Time

pred MultipleCycles [t: Time] { 
   let cycleMembers = { n: Node | n in n.(^(succ.t)) } |
      ! (all disj n1, n2: cycleMembers | n1 in n2.(^(succ.t)) )
   && ConnectedAppendages[t] 
   && AntecedentPredecessors[t]
   && OrderedAppendages[t]
}
run MultipleCycles for 2 but 0 Event, 1 Time

pred DisorderedCycle [t: Time] { 
   let cycleMembers = { n: Node | n in n.(^(succ.t)) } |
      ! (all disj n1, n2, n3: cycleMembers |   
           n2 = n1.succ.t => ! Between[n1,n3,n2] )
   && ConnectedAppendages[t] 
   && AntecedentPredecessors[t]
   && OrderedAppendages[t]
}
run DisorderedCycle for 3 but 0 Event, 1 Time

pred DisconnectedAppendages [t: Time] { 
      OneOrderedCycle[t]
   && ! ConnectedAppendages[t] 
   && AntecedentPredecessors[t]
   && OrderedAppendages[t]
}
run DisconnectedAppendages for 3 but 0 Event, 1 Time

pred NonAntecedentPredecessor [t: Time] { 
      OneOrderedCycle[t]
   && ConnectedAppendages[t] 
   && ! AntecedentPredecessors[t]
   && OrderedAppendages[t]
}
run NonAntecedentPredecessor for 2 but 0 Event, 1 Time

pred DisorderedAppendages [t: Time] { 
      OneOrderedCycle[t]
   && ConnectedAppendages[t] 
   && AntecedentPredecessors[t]
   && ! OrderedAppendages[t]
}
run DisorderedAppendages for 3 but 0 Event, 1 Time

pred ValidRingWithOneMember [t: Time] {
   let members = { n: Node | Member[n,t] } |
      # members = 1 && Valid[t] && ! Ideal[t] }
run ValidRingWithOneMember for 1 but 0 Event, 1 Time

pred ValidRingWithTwoMembers [t: Time] {
   let members = { n: Node | Member[n,t] } |
      # members = 2 && Valid[t] && ! Ideal[t] }
run ValidRingWithTwoMembers for 2 but 0 Event, 1 Time

pred ValidRingWithThreeMembers [t: Time] {
   let members = { n: Node | Member[n,t] } |
      # members = 3 && Valid[t] && ! Ideal[t] }
run ValidRingWithThreeMembers for 3 but 0 Event, 1 Time

pred ValidRingWithFourMembers [t: Time] {
   let members = { n: Node | Member[n,t] } |
      # members = 4 && Valid[t] && ! Ideal[t] }
run ValidRingWithFourMembers for 4 but 0 Event, 1 Time

pred ValidRingWithFiveMembers [t: Time] {
   let members = { n: Node | Member[n,t] } |
      # members = 5 && Valid[t] && ! Ideal[t] }
run ValidRingWithFiveMembers for 5 but 0 Event, 1 Time

pred ValidRingWithSixMembers [t: Time] {
   let members = { n: Node | Member[n,t] } |
      # members = 6 && Valid[t] && ! Ideal[t] }
run ValidRingWithSixMembers for 6 but 0 Event, 1 Time

pred ValidRingWithSevenMembers [t: Time] {
   let members = { n: Node | Member[n,t] } |
      # members = 7 && Valid[t] && ! Ideal[t] }
run ValidRingWithSevenMembers for 7 but 0 Event, 1 Time

pred UnStable [t: Time] {  
      Valid[t] 
   && ! Stable[t] 
}
run UnStable for 1 but 0 Event, 1 Time

pred IdealRingWithOneMember [t: Time] {
   let members = { n: Node | some n.succ.t } | Ideal[t] && # members = 1 }
run IdealRingWithOneMember for 1 but 0 Event, 1 Time

pred IdealRingWithTwoMembers [t: Time] {
   let members = { n: Node | some n.succ.t } | Ideal[t] && # members = 2 }
run IdealRingWithTwoMembers for 2 but 0 Event, 1 Time

pred IdealRingWithThreeMembers [t: Time] {
   let members = { n: Node | some n.succ.t } | Ideal[t] && # members = 3 }
run IdealRingWithThreeMembers for 3 but 0 Event, 1 Time

pred IdealRingWithSevenMembers [t: Time] {
   let members = { n: Node | some n.succ.t } | Ideal[t] && # members = 7 }
run IdealRingWithSevenMembers for 7 but 0 Event, 1 Time
======================================================================== */

/* ========================================================================
VALIDATION OF CHANGE PREDICATES

assert SuccessorChangeWorksSequentially {
   all n, newSucc: Node |
   (  Valid[trace/first]
   && StabilizationWillChangeSuccessor[n,newSucc,trace/first]
   && (some s: Stabilize | s.node = n)
   )
   => n.succ.trace/last = newSucc   
}
check SuccessorChangeWorksSequentially for 4 but 2 Event, 3 Time-- 229+ 79
check SuccessorChangeWorksSequentially for 7 but 2 Event, 3 Time--1113+567

assert PredecessorChangeWorksSequentially {
   all n, nSucc: Node |
   (  Valid[trace/first]
   && StabilizationShouldChangePredecessor[n,nSucc,trace/first]
   && (some s: Stabilize | s.node = n)
   )
   => nSucc.prdc.trace/last = n
}
check PredecessorChangeWorksSequentially for 4 but 2 Event, 3 Time
--  232+ 145 ms
check PredecessorChangeWorksSequentially for 7 but 2 Event, 3 Time
-- 1240+1706 ms
======================================================================== */

/* ========================================================================
SAFETY AND LIVENESS VERIFICATION OF SINGLE OPERATIONS
   A successor or precedessor change is an improvement by definition.
   The scopes here preclude any operations but single ones. 

assert InitialIsValid {
   let members = { n: Node | Member[n,trace/first] } |
   (  one members
   && members.succ.trace/first = members
   && no members.prdc.trace/first
   ) => Valid[trace/first]
}
check InitialIsValid for 1 but 0 Event, 1 Time--

assert JoinPreservesValidity { 
   some Join && Valid[trace/first] => Valid[trace/last] }
check JoinPreservesValidity for 4 but 1 Event, 2 Time-- 193+    284 ms
check JoinPreservesValidity for 7 but 1 Event, 2 Time--1036+1108733 ms

assert StabilizationPreservesValidity { 
   (some Stabilize && Valid[trace/first])
   => (Valid[trace/first.next] && Valid[trace/last]) }
check StabilizationPreservesValidity for 4 but 2 Event, 3 Time
--  349+   2684 ms
check StabilizationPreservesValidity for 7 but 2 Event, 3 Time
-- 1798+5478466 ms

assert ValidRingIsImprovable {
   (Valid[trace/first] && ! Ideal[trace/first]) =>
   (  (some n, newSucc: Node | 
         StabilizationWillChangeSuccessor[n,newSucc,trace/first])
   || (some n, nSucc: Node | 
         StabilizationShouldChangePredecessor[n,nSucc,trace/first] )
   )
}
check ValidRingIsImprovable for 4 but 0 Event, 1 Time--157+  114 ms
check ValidRingIsImprovable for 7 but 0 Event, 1 Time--826+65291 ms

assert IdealRingCannotChange { 
      Ideal[trace/first]
   => (  (no n, newSucc: Node | 
            StabilizationWillChangeSuccessor[n,newSucc,trace/first] )
      && (no n, nSucc: Node |
            StabilizationShouldChangePredecessor[n,nSucc,trace/first] )
      )
}
check IdealRingCannotChange for 4 but 0 Event, 1 Time-- 92+    65 ms
check IdealRingCannotChange for 7 but 0 Event, 1 Time--485+101994 ms
======================================================================== */

/* ========================================================================
VERIFICATION OF CONCURRENT OPERATIONS

pred NestedStabilizations [disj s1, s2: Stabilize, f1, f2: Notify]
{  Valid[trace/first]
   && lt[s1.pre,s2.pre]
   && s1 in f1.(^cause) && s2 in f2.(^cause) 
   && lt[f2.pre,f1.pre]
}
run NestedStabilizations for 3 but 4 Event, 5 Time

assert NestedStabilizationsPreserveValidity {
   all s1, s2: Stabilize, f1, f2: Notify |
      NestedStabilizations[s1,s2,f1,f2] => 
      (  Valid[trace/first.next]
      && Valid[(trace/first.next).next]
      && Valid[((trace/first.next).next).next]
      && Valid[trace/last]
      )
}
check NestedStabilizationsPreserveValidity for 5 but 4 Event, 5 Time
-- 1705+228914 ms

pred OverlappingStabilizations [disj s1, s2: Stabilize, f1, f2: Notify]
{  Valid[trace/first]
   && lt[s1.pre,s2.pre]
   && s1 in f1.(^cause) && s2 in f2.(^cause) 
   && lt[s2.pre,f1.pre]
   && lt[f1.pre,f2.pre]
}
run OverlappingStabilizations for 3 but 4 Event, 5 Time

assert OverlappingStabilizationsPreserveValidity {
   all s1, s2: Stabilize, f1, f2: Notify |
      OverlappingStabilizations[s1,s2,f1,f2] => 
      (  Valid[trace/first.next]
      && Valid[(trace/first.next).next]
      && Valid[((trace/first.next).next).next]
      && Valid[trace/last]
      )
}
check OverlappingStabilizationsPreserveValidity for 5 but 4 Event, 5 Time
-- 1542+173469 ms

pred ConcurrentJoinAndStabilize [s: Stabilize, j: Join, f: Notify]
{  Valid[trace/first]
   && lt[s.pre,j.pre]
   && lt[j.pre,f.pre]
   && s in f.(^cause)
}
run ConcurrentJoinAndStabilize for 3 but 3 Event, 4 Time

assert ConcurrentJoinAndStabilizePreserveValidity {
   all s: Stabilize, j: Join, f: Notify |
      ConcurrentJoinAndStabilize[s,j,f] => 
      (  Valid[trace/first.next]
      && Valid[(trace/first.next).next]
      && Valid[trace/last]
      )
}
check ConcurrentJoinAndStabilizePreserveValidity for 5 but 4 Event, 5 Time
-- 1440+298294 ms

-- There are six cases to verify: 
--    { nested, overlapping, concjoin } x { succ, pred }

-- NESTED CASES -----------------------------------------------------------
-- Note that in any nested stabilization s1.node cannot equal s2.node, 
-- because then the same node would be initiating a stabilization without
-- finishing its last one.

assert SuccessorChangeWorksNested1 {
   all s1, s2: Stabilize, f1, f2: Notify, w: Node |
      (  NestedStabilizations[s1,s2,f1,f2]
      && StabilizationWillChangeSuccessor[s1.node,w,trace/first]
      && s1.node != s2.node
      ) => (s1.node).succ.trace/last = w    
}
check SuccessorChangeWorksNested1 for 5 but 4 Event, 5 Time--1007+416 ms

assert SuccessorChangeWorksNested2 {
   all s1, s2: Stabilize, f1, f2: Notify, w: Node |
      (  NestedStabilizations[s1,s2,f1,f2]
      && StabilizationWillChangeSuccessor[s2.node,w,trace/first]
      && s1.node != s2.node
      ) => (s2.node).succ.trace/last = w    
}
check SuccessorChangeWorksNested2 for 5 but 4 Event, 5 Time--1032+336 ms

assert PredecessorChangeWorksNested1 {
   all s1, s2: Stabilize, f1, f2: Notify, w: Node |
      (  NestedStabilizations[s1,s2,f1,f2]
      && StabilizationShouldChangePredecessor[s1.node,w,trace/first]
      && s1.node != s2.node
      ) => (  w.prdc.trace/last = s1.node
           || Between[s1.node,w.prdc.trace/last,w]
           )
}
check PredecessorChangeWorksNested1 for 5 but 4 Event, 5 Time--1256+374 ms
-- This shows that the resulting predecessor is either expected or better
-- than expected.

assert PredecessorChangeWorksNested2 {
   all s1, s2: Stabilize, f1, f2: Notify, w: Node |
      (  NestedStabilizations[s1,s2,f1,f2]
      && StabilizationShouldChangePredecessor[s2.node,w,trace/first]
      && s1.node != s2.node
      ) => (  w.prdc.trace/last = s2.node
           || Between[s2.node,w.prdc.trace/last,w]
           )
}
check PredecessorChangeWorksNested2 for 5 but 4 Event, 5 Time--1051+1818 ms
-- This shows that the resulting predecessor is either expected or better
-- than expected.

-- Overall, in the nested case, successor changes are independent.  
-- Predecessor changes are independent unless both stabilizing nodes end up
-- with the same successor, in which case its predecessor will end up as
-- the best of the stabilizing nodes.  In effect, the operations are
-- serializable with the better-predecessor operation coming second.

-- OVERLAPPING CASES ------------------------------------------------------
-- Note that in any overlapping stabilization s1.node cannot equal s2.node,
-- because then the same node would be initiating a stabilization without
-- finishing its last one.

-- Note that nested and overlapping stabilizations are the same with
-- respect to successor changes.

assert PredecessorChangeWorksOverlapping1 {
   all s1, s2: Stabilize, f1, f2: Notify, w: Node |
      (  OverlappingStabilizations[s1,s2,f1,f2]
      && StabilizationShouldChangePredecessor[s1.node,w,trace/first]
      && s1.node != s2.node
      ) => (  w.prdc.trace/last = s1.node
           || Between[s1.node,w.prdc.trace/last,w]
           )
}
check PredecessorChangeWorksOverlapping1 for 5 but 4 Event, 5 Time
-- 1082+1103 ms

assert PredecessorChangeWorksOverlapping2 {
   all s1, s2: Stabilize, f1, f2: Notify, w: Node |
      (  OverlappingStabilizations[s1,s2,f1,f2]
      && StabilizationShouldChangePredecessor[s2.node,w,trace/first]
      && s1.node != s2.node
      ) => (  w.prdc.trace/last = s2.node
           || Between[s2.node,w.prdc.trace/last,w]
           )
}
check PredecessorChangeWorksOverlapping2 for 5 but 4 Event, 5 Time
-- 1048+1069 ms

-- CONCURRENT JOIN CASES --------------------------------------------------

assert SuccChangeWorksInConcurrentJoinAndStabilize {
   all s: Stabilize, j: Join, f: Notify, w: Node |
      (  ConcurrentJoinAndStabilize[s,j,f] 
      && StabilizationWillChangeSuccessor[s.node,w,trace/first]
      ) => (s.node).succ.trace/last = w    
}
check SuccChangeWorksInConcurrentJoinAndStabilize for 5 but 3 Event, 4 Time
-- 694+362 ms

assert PrdcChangeWorksInConcurrentJoinAndStabilize {
   all s: Stabilize, j: Join, f: Notify, w: Node |
      (  ConcurrentJoinAndStabilize[s,j,f] 
      && StabilizationShouldChangePredecessor[s.node,w,trace/first]
      ) => w.prdc.trace/last = s.node
}
check PrdcChangeWorksInConcurrentJoinAndStabilize for 5 but 3 Event, 4 Time
-- 693+814 ms
======================================================================== */

/* ========================================================================
   Node, Time, Event
======================================================================== */