alloy - 在 Alloy 中分发代币

Question

我正在关注 Daniel Jackson 的优秀著作 (Software Abstractions)) 中的一个示例，特别是他设置 token 环以选举领导者的示例。

我正在尝试扩展此示例( Ring election )以确保 token (而不是仅限于一个)在提供的时间内传递给所有成员(并且每个成员只被选举一次，而不是多次) .但是(主要是由于我对合金缺乏经验)，我在找出最佳方法时遇到了问题。最初我认为我可以与一些运算符一起玩(将 - 更改为 + )，但我似乎并没有完全击中头部。

下面是示例中的代码。我已经用问题标记了一些区域......感谢任何和所有帮助。我正在使用合金 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

这个网络协议(protocol)正是关于如何选举单个进程作为领导者，所以我不太明白你“最终选举所有进程”的想法的含义。

而不是 all elected.Time , 你可以等价写成 elected.Time = Process (因为 elected 的类型是 Process -> Time )。这只是说elected.Time (在任何时间步骤选出的所有进程)正是所有进程的集合，显然，这并不意味着“只选出一个进程”，正如您的断言名称所暗示的那样。