/*
 * An incomplete model of leader election in a ring.
 * Follow the instructions in the Dynamic Modeling lecture to complete.
 */
module examples/tutorial/ringElection

open util/ordering[Time] as to
open util/ordering[Process] as po

sig Time {}
sig Process {
  succ: Process,
  toSend: Process -> Time,
  elected: set Time
}

fact defineElected {
  no elected.(to/first())
  all t: Time - to/first() |
    elected.t = {p:Process | p in (p.toSend.t - p.toSend.(to/prev(t)))}
}

fact traces {
  init(to/first())
  all t: Time - to/last() | let t' = to/next(t) |
    all p: Process |
      step(t, t', p) || step(t, t', succ.p) || skip(t, t', p)
}

pred init(t: Time) {
  // every process has exactly itself to send
}

pred skip(t, t': Time, p: Process) {
  // a no-op: process p send no ids during that time step
}

pred step(t, t': Time, p: Process) {
  // process p sends one id to successor
  // successor keeps it or drops it
}

assert atMostOneElected {
  // no more than one process is deemed elected
  // no process is deemed elected more than once
}
check atMostOneElected for 3 Process, 7 Time

assert atLeastOneElected {
  // at least one process is elected on each trace
}
check atLeastOneElected for 3 Process, 7 Time

pred looplessPath() {
  no disj t, t': Time | toSend.t = toSend.t'
}
// run looplessPath for 3 Process, ? Time