傳播令牌在合金

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（所有在任何時間步驟選出的進程）都是所有進程的集合，顯然，這並不意味着「只有一個進程被選中」，正如斷言的名稱所表明的那樣。