传播令牌在合金

Question

我按照丹尼尔·杰克逊的优秀图书（Software Abstractions)，具体的例子，他有一个令牌环的设置，以选出一个领导者的例子。

我试图扩展此示例（Ring election）以确保令牌（而不是限于一个）在所提供的时间内传递给所有成员（并且每个成员只选择一次，而不是多次）。但是（主要是由于我在合金方面没有经验），我在找出最佳方法时遇到了问题。最初我以为我可以和一些运营商一起玩（改变为+的），但我似乎并不完全击中头部的指甲

下面是该示例的代码。我已经标记了几个有问题的地方...任何和所有的帮助表示赞赏。我正在使用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. 这种网络协议究竟是如何选出一个过程中成为领导者，所以我真的不明白你有“的所有进程最终当选”的思想意义。
2. 而不是all elected.Time，您可以等效地编写elected.Time = Process（因为elected的类型为Process -> Time）。这只是说，elected.Time（所有在任何时间步骤选出的进程）都是所有进程的集合，显然，这并不意味着“只有一个进程被选中”，正如断言的名称所表明的那样。