/* * An incomplete model of leader election in a ring. * Follow the instructions in the Dynamic Modeling lecture to complete. */ 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.(t.prev)) } } fact traces { init [to/first] all t: Time - to/last | let t' = t.next | 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