/* ========================================================================
A MODEL OF THE FULL 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
   Simplifications:
   (1) In this model, the node itself, its IP address, and its hashed 
identifier are all conflated.
   (2) The successor list of a node has size 2.  As far as I can tell, this
brevity does not eliminate any interesting behaviors.
   (3) Fingers are not included in this model, as they have no effect on
ring structure.
======================================================================== */

sig Node {
   succ: Node lone -> Time,
   succ2: Node lone -> Time,
   prdc: Node lone -> Time,
   bestSucc: Node lone -> Time }
{  
-- This defines bestSucc.
   all t: Time |
      (Member[succ.t,t] && Member[succ2.t,t] => bestSucc.t = succ.t)
   && (Member[succ.t,t] && NonMember[succ2.t,t] => bestSucc.t = succ.t)
   && (NonMember[succ.t,t] && Member[succ2.t,t] => bestSucc.t = succ2.t)
   && (NonMember[succ.t,t] && NonMember[succ2.t,t] => no bestSucc.t)

-- 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 && no n.succ2.t  }

pred Between [n1, n2, n3: Node] {
   lt[n1,n3] =>   ( lt[n1,n2] && lt[n2,n3] )
             else ( lt[n1,n2] || lt[n2,n3] )  }
                                       -- for all x and y,   Between{x,y,x]
                                             -- for all x, ! Between{x,x,x]
                                       -- for all x and y, ! Between{x,x,y]
                                       -- for all x and y, ! Between{y,x,x]

/* ========================================================================
POSSIBLE INVARIANT PROPERTIES
======================================================================== */

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

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

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

pred OrderedAppendages [t: Time] {
   let members = { n: Node | Member[n,t] } |
   let cycleMembers = { n: members | n in n.(^(bestSucc.t)) } |
   let appendSucc = bestSucc.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 OrderedMerges [t: Time] {
   let cycleMembers = { n: Node | n in n.(^(bestSucc.t)) } |
      all disj n1, n2, n3: Node |
         (  n3 in n1.bestSucc.t
         && n3 in n2.bestSucc.t
         && n1 in cycleMembers 
         && n2 !in cycleMembers
         && n3 in cycleMembers 
         ) => Between[n1,n2,n3]
}

pred DistinctSuccessors [t: Time] {
   all n: Node | Member[n,t] => n.succ2.t != n.succ.t && n.succ2.t != n }

pred OrderedSuccessors [t: Time] {
   all n: Node | 
      Member[n,t] && some n.succ2.t => Between[n,n.succ.t,n.succ2.t] 
}

pred ValidSuccessorList [t: Time] { 
   let members = { n: Node | Member[n,t] } |
   all n, m: members | 
      let antes = (succ.t).n |
         Between[n.succ.t,m,n.succ2.t]
                                  -- n's successors skip over a live node m
         => m !in antes.succ2.t
                          -- m is not in successor list of any n antecedent
}  

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

pred Valid [t: Time] { 
      OneOrderedCycle[t]                         -- from PODC Full, revised
   && ConnectedAppendages[t]                     -- from PODC Full, revised
   && AntecedentPredecessors[t]                                      -- new
   && OrderedAppendages[t]                                -- from PODC Full
   && OrderedMerges[t]                                    -- from PODC Full
   && DistinctSuccessors[t]                                          -- new
   && OrderedSuccessors[t]                                           -- new
   && ValidSuccessorList[t]                      -- from PODC Full, revised
   && ReachableSuccessor2[t]                                         -- new
}

-- These are the only properties needed for an undisturbed network to
-- become ideal through stabilization and reconciliation.
pred CoreValid [t: Time] { 
      OneOrderedCycle[t]                         -- from PODC Full, revised
   && ConnectedAppendages[t]                     -- from PODC Full, revised
}

pred SomeBestSuccessor [t: Time] { 
   all n: Node | Member[n,t] => some n.bestSucc.t  }

assert ValidImpliesSomeBestSuccessor {
   all t: Time | Valid[t] => SomeBestSuccessor[t] }
check ValidImpliesSomeBestSuccessor for 5 but 0 Event, 1 Time
check ValidImpliesSomeBestSuccessor for 7 but 0 Event, 1 Time

/* ========================================================================
IDEAL PROPERTIES
======================================================================== */

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 | some n.succ.t } |
   all n1, n2: members | n2 in n1.(^(succ.t))
}

pred Reconciled [t: Time] { let members = { n: Node | Member[n,t] } |
   all n: members | 
         Member[n.succ.t,t] 
      && Member[n.succ2.t,t]
      && n.succ2.t = (n.succ.t).succ.t
}

pred Succ2Correctness [t: Time] { let members = { n: Node | Member[n,t] } |
   all n: members |
      (Member[n.succ2.t,t] && n.succ2.t != n.bestSucc.t)
   => n.succ2.t = (n.bestSucc.t).bestSucc.t
}

pred Ideal [t: Time] {  
      Valid[t] 
   && Stable[t]                                  -- from PODC Full, revised
   && Reconciled[t]                              -- from PODC Full, revised
}

assert IdealImpliesAllCycle { all t: Time | Ideal[t] => AllCycle[t] }
check IdealImpliesAllCycle for 5 but 0 Event, 1 Time
check IdealImpliesAllCycle for 7 but 0 Event, 1 Time

assert IdealImpliesSucc2Correct { all t: Time | 
   Ideal[t] => Succ2Correctness[t] }
check IdealImpliesSucc2Correct for 5 but 0 Event, 1 Time
check IdealImpliesSucc2Correct for 7 but 0 Event, 1 Time

/* ========================================================================
SPECIFICATION OF EVENTS
   Simplifications:
   (1) The event specifications assume that an event occurs only when the
structure is valid.
   (2) The Join specification assumes that a node cannot join if a current
member has a pointer to it, because that pointer will be left over from a
previous phase of membership, and may be invalid.
   (3) The specification assumes that an operation is an atomic event, even
if it retrieves information from other nodes (Are you alive?  What is your
successor?), because this seems clearly serializable.  The only non-atomic
operations are those that change the states of multiple nodes.
   (4) The Fail specification will not allow a node to fail if it would
leave another node with no live node in its successor list.  This is a
deterministic version of the probabilistic assertion supported by the
length of real successor lists.
   Bug fixes:
   (1) The Join specification checks that the successor adopted by the
joining node is live.  Otherwise the structure can become disconnected
immediately.
   (2) The Stabilize specification checks that the successor adopted by the
stabilizing node is live.  Otherwise the cycle can be lost easily.
   (3) The Update specification requires removal of a succ2 when it is
promoted to succ.  This preserves the property of distinct successors.
   (4) The Reconcile specification does not allow a node to have itself as
succ2.  This is necessary to avoid losing the cycle.
======================================================================== */

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 }
sig Fail extends RingEvent { } { no cause }
sig Flush extends RingEvent { } { no cause }
sig Update extends RingEvent { } { no cause }
sig Reconcile extends RingEvent { } { no cause }

fact NonMemberCanJoin {
   all j: Join, n: j.node, t: j.pre | {
      NonMember[n,t]
      n !in Node.succ.t
      n !in Node.succ2.t
      n !in Node.prdc.t
      (some m: Node |    Member[m,t]
                      && Between[m,n,m.succ.t]
                      && Member[m.succ.t,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]
      Member[n.succ.t,t]
      (  (  some newSucc
         && Between[n,newSucc,n.succ.t]
         && Member[newSucc,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 |
      (   Member[n,t]
      && (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)
}

fact MemberCanFail {
   all f: Fail, n: f.node, t: f.pre | {
      Member[n,t]
      (all m: Node | m.succ.t = n => Member[m.succ2.t,t])
      (all m: Node | m.succ2.t = n => Member[m.succ.t,t])
      NonMember[n,f.post] 
      no cause:>f
}  }

fact FlushMayChangePredecessor {
   all f: Flush, n: f.node, t: f.pre | {
      (Member[n,t] && NonMember[n.prdc.t,t])
         =>   no n.prdc.(f.post) 
         else n.prdc.(f.post) = n.prdc.t
      no cause:>f
}  }

fact UpdateMayChangeSuccessor {
   all u: Update, n: u.node, t: u.pre |
      let oldSucc = n.succ.t |  
      let oldSucc2 = n.succ2.t | {
         (Member[n,t] && NonMember[oldSucc,t] && some oldSucc2)
         =>   (  n.succ.(u.post) = oldSucc2
              && no n.succ2.(u.post)
              )
         else (n.succ.(u.post) = oldSucc && n.succ2.(u.post) = oldSucc2)
                               --  at least one of the two must be a member
      no cause:>u
}  }

fact ReconcileMayChangeSuccessor2 {
   all r: Reconcile, n: r.node, t: r.pre |
      let oldSucc2 = n.succ2.t      | 
      let newSucc2 = (n.succ.t).succ.t | {      -- not necessarily a member
         (  Member[n,t] 
         && Member[n.succ.t,t]
         && newSucc2 != oldSucc2                   -- this must be a change
         && newSucc2 != n.succ.t             -- successors must be distinct
         && newSucc2 != n 
         )  =>   n.succ2.(r.post) = newSucc2
            else n.succ2.(r.post) = oldSucc2
         no cause:>r
}  }

/* ========================================================================
FRAME CONDITIONS
======================================================================== */

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

fact Successor2FieldFrameCondition {
   all e: Event, n: Node | n.succ2.(e.pre) != n.succ2.(e.post)
   => (  (e in Fail && e.node = n)
      || (e in Reconcile && e.node = n)
      )
}

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

/* ========================================================================
CHANGE PREDICATES
======================================================================== */

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

pred StabilizationShouldChangePredecessor [n, nSucc: Node, t: Time] {
   (  (  StabilizationWillChangeSuccessor[n,nSucc,t]
      || (nSucc = n.succ.t && Member[n,t] && Member[nSucc,t])
      )
   && (  no nSucc.prdc.t 
      || (some nSucc.prdc.t && Between[nSucc.prdc.t,n,nSucc])
      )
   )
}

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

pred ReconciliationWillChangeSuccessor [n, nSucc: Node, t: Time] {
      Member[n,t] && NonMember[n.succ.t,t] 
   && some n.succ2.t && nSucc = n.succ2.t }

pred ReconciliationWillChangeSuccessor2 [n, nSucc2: Node, t: Time] {
   let oldSucc2 = n.succ2.t |
   let newSucc2 = (n.succ.t).succ.t | 
         Member[n,t] 
      && Member[n.succ.t,t]
      && newSucc2 != oldSucc2
      && newSucc2 != n.succ.t
      && newSucc2 != n 
      && nSucc2 = newSucc2
}

/* ========================================================================
SAFETY VERIFICATION OF INITIALIZATION AND SINGLE OPERATIONS
   The scopes here preclude any operations but single ones.
   This verification cannot be completed; see the paper for details.
======================================================================== */

assert InitialIsValid { 
   let members = { n: Node | Member[n,trace/first] } |
   (  one members 
   && members.succ.trace/first = members
   && no members.prdc.trace/first 
   && no members.succ2.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 1 but 1 Event, 2 Time
check JoinPreservesValidity for 2 but 1 Event, 2 Time
check JoinPreservesValidity for 3 but 1 Event, 2 Time
check JoinPreservesValidity for 4 but 1 Event, 2 Time
check JoinPreservesValidity for 5 but 1 Event, 2 Time
check JoinPreservesValidity for 6 but 1 Event, 2 Time
check JoinPreservesValidity for 7 but 1 Event, 2 Time

assert StabilizationPreservesValidity {
   (some Stabilize && Valid[trace/first])
   => (Valid[trace/first.next] && Valid[trace/last]) }
check StabilizationPreservesValidity for 1 but 2 Event, 3 Time
check StabilizationPreservesValidity for 2 but 2 Event, 3 Time
check StabilizationPreservesValidity for 3 but 2 Event, 3 Time
check StabilizationPreservesValidity for 4 but 2 Event, 3 Time
check StabilizationPreservesValidity for 5 but 2 Event, 3 Time
check StabilizationPreservesValidity for 6 but 2 Event, 3 Time
check StabilizationPreservesValidity for 7 but 2 Event, 3 Time

assert FailPreservesValidity {
   some Fail && Valid[trace/first] => Valid[trace/last] }
check FailPreservesValidity for 1 but 1 Event, 2 Time
check FailPreservesValidity for 2 but 1 Event, 2 Time
check FailPreservesValidity for 3 but 1 Event, 2 Time
check FailPreservesValidity for 4 but 1 Event, 2 Time
check FailPreservesValidity for 5 but 1 Event, 2 Time
check FailPreservesValidity for 6 but 1 Event, 2 Time
check FailPreservesValidity for 7 but 1 Event, 2 Time

assert FlushPreservesValidity {
   some Flush && Valid[trace/first] => Valid[trace/last] }
check FlushPreservesValidity for 1 but 1 Event, 2 Time
check FlushPreservesValidity for 2 but 1 Event, 2 Time
check FlushPreservesValidity for 3 but 1 Event, 2 Time
check FlushPreservesValidity for 4 but 1 Event, 2 Time
check FlushPreservesValidity for 5 but 1 Event, 2 Time
check FlushPreservesValidity for 6 but 1 Event, 2 Time
check FlushPreservesValidity for 7 but 1 Event, 2 Time

assert UpdatePreservesValidity { 
   some Update && Valid[trace/first] => Valid[trace/last]  }
check UpdatePreservesValidity for 1 but 1 Event, 2 Time
check UpdatePreservesValidity for 2 but 1 Event, 2 Time
check UpdatePreservesValidity for 3 but 1 Event, 2 Time
check UpdatePreservesValidity for 4 but 1 Event, 2 Time
check UpdatePreservesValidity for 5 but 1 Event, 2 Time
check UpdatePreservesValidity for 6 but 1 Event, 2 Time
check UpdatePreservesValidity for 7 but 1 Event, 2 Time

assert ReconcilePreservesValidity { 
   some Reconcile && Valid[trace/first] => Valid[trace/last]  }
check ReconcilePreservesValidity for 1 but 1 Event, 2 Time
check ReconcilePreservesValidity for 2 but 1 Event, 2 Time
check ReconcilePreservesValidity for 3 but 1 Event, 2 Time
check ReconcilePreservesValidity for 4 but 1 Event, 2 Time
check ReconcilePreservesValidity for 5 but 1 Event, 2 Time
check ReconcilePreservesValidity for 6 but 1 Event, 2 Time
check ReconcilePreservesValidity for 7 but 1 Event, 2 Time

/* ========================================================================
LIVENESS VERIFICATION
======================================================================== */

assert NontrivialValidRingIsImprovable {
   let members = { n: Node | Member[n,trace/first] } |
      (  CoreValid[trace/first] 
      && ! Ideal[trace/first]
      && # members > 2
      ) 
   =>
   (  (some n1, n2: Node | 
         StabilizationWillChangeSuccessor[n1,n2,trace/first])
   || (some n1, n2: Node | 
         StabilizationShouldChangePredecessor[n1,n2,trace/first])
   || (some n: Node | ReconciliationWillFlushPredecessor[n,trace/first])
   || (some n1, n2: Node | 
         ReconciliationWillChangeSuccessor[n1,n2,trace/first])
   || (some n1, n2: Node | 
         ReconciliationWillChangeSuccessor2[n1,n2,trace/first])
   )
}
check NontrivialValidRingIsImprovable for 5 but 0 Event, 1 Time 
check NontrivialValidRingIsImprovable for 7 but 0 Event, 1 Time 

pred TrivialValidRingIsImprovable [t: Time] {
   let members = { n: Node | Member[n,t] } |
         CoreValid[t] 
      && ! Ideal[t]
      && # members <= 2
      && (  (some n1, n2: Node | 
               StabilizationWillChangeSuccessor[n1,n2,t])
         || (some n1, n2: Node | 
               StabilizationShouldChangePredecessor[n1,n2,t])
         || (some n: Node | ReconciliationWillFlushPredecessor[n,t])
         || (some n1, n2: Node | 
               ReconciliationWillChangeSuccessor[n1,n2,t])
         || (some n1, n2: Node | 
               ReconciliationWillChangeSuccessor2[n1,n2,t])
         )
}
run TrivialValidRingIsImprovable for 1 but 0 Event, 1 Time 
run TrivialValidRingIsImprovable for 2 but 0 Event, 1 Time 

pred TrivialValidRingIsNotImprovable [t: Time] {
   let members = { n: Node | Member[n,t] } |
         CoreValid[t] 
      && ! Ideal[t]
      && # members <= 2
      && (  (no n1, n2: Node | 
               StabilizationWillChangeSuccessor[n1,n2,t])
         && (no n1, n2: Node | 
               StabilizationShouldChangePredecessor[n1,n2,t])
         && (no n: Node | ReconciliationWillFlushPredecessor[n,t])
         && (no n1, n2: Node | 
               ReconciliationWillChangeSuccessor[n1,n2,t])
         && (no n1, n2: Node | 
               ReconciliationWillChangeSuccessor2[n1,n2,t])
         )
}
run TrivialValidRingIsNotImprovable for 1 but 0 Event, 1 Time 
run TrivialValidRingIsNotImprovable for 2 but 0 Event, 1 Time 

assert IdealRingCannotImprove {
   Ideal[trace/first]
   =>
   (  (no n1, n2: Node | 
         StabilizationWillChangeSuccessor[n1,n2,trace/first])
   && (no n1, n2: Node | 
         StabilizationShouldChangePredecessor[n1,n2,trace/first])
   && (no n: Node | ReconciliationWillFlushPredecessor[n,trace/first])
   && (no n1, n2: Node | 
         ReconciliationWillChangeSuccessor[n1,n2,trace/first])
   && (no n1, n2: Node | 
         ReconciliationWillChangeSuccessor2[n1,n2,trace/first])
   )
}
check IdealRingCannotImprove for 5 but 0 Event, 1 Time 
check IdealRingCannotImprove for 7 but 0 Event, 1 Time 

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

assert SSChangeWorksSequentially {
   all n, nSucc: Node |
   (  Valid[trace/first]
   && StabilizationWillChangeSuccessor[n,nSucc,trace/first]
   && (some s: Stabilize | s.node = n)
   )
   => n.succ.trace/last = nSucc
}
check SSChangeWorksSequentially for 5 but 1 Event, 2 Time 

assert SPChangeWorksSequentially {
   all n, nSucc: Node |
   (  Valid[trace/first]
   && StabilizationShouldChangePredecessor[n,nSucc,trace/first]
   && (some s: Stabilize | s.node = n)
   )
   => nSucc.prdc.trace/last = n
}
check SPChangeWorksSequentially for 5 but 2 Event, 3 Time 

assert RPChangeWorksSequentially {
   all n: Node |
   (  Valid[trace/first]
   && ReconciliationWillFlushPredecessor[n,trace/first]
   && (some f: Flush | f.node = n)
   )
   => no n.prdc.trace/last
}
check RPChangeWorksSequentially for 5 but 1 Event, 2 Time 

assert RSChangeWorksSequentially {
   all n, nSucc: Node |
   (  Valid[trace/first]
   && ReconciliationWillChangeSuccessor[n,nSucc,trace/first]
   && (some u: Update | u.node = n)
   )
   => n.succ.trace/last = nSucc
}
check RSChangeWorksSequentially for 5 but 1 Event, 2 Time 

assert RS2ChangeWorksSequentially {
   all n, nSucc2: Node |
   (  Valid[trace/first]
   && ReconciliationWillChangeSuccessor2[n,nSucc2,trace/first]
   && (some r: Reconcile | r.node = n)
   )
   => n.succ2.trace/last = nSucc2
}
check RS2ChangeWorksSequentially for 5 but 1 Event, 2 Time 
======================================================================== */

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

pred NotOneOrderedCycle [t: Time] { 
      ! OneOrderedCycle[t]    
   && ConnectedAppendages[t]
   && AntecedentPredecessors[t] 
   && OrderedAppendages[t]     
   && OrderedMerges[t]        
   && DistinctSuccessors[t]  
   && OrderedSuccessors[t]  
   && ValidSuccessorList[t]
   && ReachableSuccessor2[t]
}
run NotOneOrderedCycle for 2 but 0 Event, 1 Time

pred DisconnectedAppendage [t: Time] { 
      OneOrderedCycle[t]    
   && ! ConnectedAppendages[t]
   && AntecedentPredecessors[t] 
   && OrderedAppendages[t]     
   && OrderedMerges[t]        
   && DistinctSuccessors[t]  
   && OrderedSuccessors[t]  
   && ValidSuccessorList[t]
   && ReachableSuccessor2[t]
}
run DisconnectedAppendage for 3 but 0 Event, 1 Time

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

pred DisorderedAppendage [t: Time] { 
      OneOrderedCycle[t]    
   && ConnectedAppendages[t]
   && AntecedentPredecessors[t] 
   && ! OrderedAppendages[t]     
   && OrderedMerges[t]        
   && DistinctSuccessors[t]  
   && OrderedSuccessors[t]  
   && ValidSuccessorList[t]
   && ReachableSuccessor2[t]
}
run DisorderedAppendage for 3 but 0 Event, 1 Time

pred DisorderedMerge [t: Time] { 
      OneOrderedCycle[t]    
   && ConnectedAppendages[t]
   && AntecedentPredecessors[t] 
   && OrderedAppendages[t]     
   && ! OrderedMerges[t]        
   && DistinctSuccessors[t]  
   && OrderedSuccessors[t]  
   && ValidSuccessorList[t]
   && ReachableSuccessor2[t]
}
run DisorderedMerge for 3 but 0 Event, 1 Time

pred RedundantSuccessors [t: Time] { 
      OneOrderedCycle[t]    
   && ConnectedAppendages[t]
   && AntecedentPredecessors[t] 
   && OrderedAppendages[t]     
   && OrderedMerges[t]        
   && ! DistinctSuccessors[t]  
   && OrderedSuccessors[t]  
   && ValidSuccessorList[t]
   && ReachableSuccessor2[t]
}
run RedundantSuccessors for 2 but 0 Event, 1 Time

pred DisorderedSuccessors [t: Time] { 
      OneOrderedCycle[t]    
   && ConnectedAppendages[t]
   && AntecedentPredecessors[t] 
   && OrderedAppendages[t]     
   && OrderedMerges[t]        
   && DistinctSuccessors[t]  
   && ! OrderedSuccessors[t]  
   && ValidSuccessorList[t]
   && ReachableSuccessor2[t]
}
run DisorderedSuccessors for 2 but 0 Event, 1 Time

pred InvalidSuccessors [t: Time] { 
      OneOrderedCycle[t]    
   && ConnectedAppendages[t]
   && AntecedentPredecessors[t] 
   && OrderedAppendages[t]     
   && OrderedMerges[t]        
   && DistinctSuccessors[t]  
   && OrderedSuccessors[t]  
   && ! ValidSuccessorList[t]
   && ReachableSuccessor2[t]
}
run InvalidSuccessors for 4 but 0 Event, 1 Time

pred ExternalSuccessor [t: Time] { 
      OneOrderedCycle[t]    
   && ConnectedAppendages[t]
   && AntecedentPredecessors[t] 
   && OrderedAppendages[t]     
   && OrderedMerges[t]        
   && DistinctSuccessors[t]  
   && OrderedSuccessors[t]  
   && ValidSuccessorList[t]
   && ! ReachableSuccessor2[t]
}
run ExternalSuccessor 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 UnStable [t: Time] {  
   Valid[t] && ! Stable[t] && Reconciled[t]  }
run UnStable for 3 but 0 Event, 1 Time

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

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

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

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

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