Disseminating a token in Alloy

Question

I'm following an example in Daniel Jackson's excellent book (Software Abstractions), specifically the example in which he has a token-ring setup in order to elect a leader.

I'm attempting to extend this example (Ring election) to ensure that the token, instead of being limited to one, is being passed around to all members within the provided time (and each member only being elected once, not multiple times). However (mostly due to my inexperience in Alloy), I'm having issues figuring out the best way. Initially I'd thought that I could play with some of the operators (changing -'s to +'s), but I don't seem to be quite hitting the nail on the head.

Below is the code from the example. I've marked up a few areas with questions...any and all help is appreciated. I'm using Alloy 4.2.

module chapter6/ringElection1 --- the version up to the top of page 181

open util/ordering[Time] as TO
open util/ordering[Process] as PO

sig Time {}

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

// ensure processes are in a ring
fact ring {
    all p: Process | Process in p.^succ
    }

pred init [t: Time] {
    all p: Process | p.toSend.t = p
    }

//QUESTION: I'd thought that within this predicate and the following fact, that I could 
//  change the logic from only having one election at a time to all being elected eventually.  
//  However, I can't seem to get the logic down for this portion.  
pred step [t, t': Time, p: Process] {
    let from = p.toSend, to = p.succ.toSend |
        some id: from.t {
            from.t' = from.t - id
            to.t' = to.t + (id - p.succ.prevs)
        }
    }

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

fact traces {
    init [first]
    all t: Time-last |
        let t' = t.next |
            all p: Process |
                step [t, t', p] or step [t, t', succ.p] or skip [t, t', p]
    }

pred skip [t, t': Time, p: Process] {
    p.toSend.t = p.toSend.t'
    }

pred show { some elected }
run show for 3 Process, 4 Time
// This generates an instance similar to Fig 6.4

//QUESTION: here I'm attempting to assert that ALL Processes have an election, 
//  however the 'all' keyword has been deprecated.  Is there an appropriate command in 
//  Alloy 4.2 to take the place of this?
assert OnlyOneElected { all elected.Time }
check OnlyOneElected for 10 Process, 20 Time

Answer 1

1. This network protocol is exactly about how to elect a single process to be the leader, so I don't really understand the meaning of your idea of having "all processes elected eventually".
2. instead of all elected.Time, you can equivalently write elected.Time = Process (since the type of elected is Process -> Time). This just says that elected.Time (all processes elected at any time step) is exactly the set of all processes, which, obviously, doesn't mean that "only one process is elected", as suggested by the name of your assertion.