4

Daniel Jackson の優れた本 ( Software Abstractions)の例、具体的にはリーダーを選出するために彼がトークンリングをセットアップしている例に従っています。

この例 (リング選挙) を拡張して、トークンが 1 つに限定されるのではなく、指定された時間内にすべてのメンバーに渡されるようにしようとしています (各メンバーは複数回ではなく 1 回だけ選出されます)。ただし (主に合金の経験が浅いため)、最善の方法を見つけるのに問題があります。最初は、いくつかの演算子 (- を + に変更) をいじれると思っていましたが、うまくいきませんでした。

以下は、例のコードです。私は質問でいくつかの領域をマークアップしました...すべての助けに感謝します。アロイ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
4

1 に答える 1

1
  1. このネットワーク プロトコルは、1 つのプロセスをリーダーとして選出する方法に関するものなので、「すべてのプロセスが最終的に選出される」というあなたの考えの意味がよくわかりません。
  2. の代わりにall elected.Time、同等に書くことができますelected.Time = Process(の型がelectedisであるためProcess -> Time)。これは、elected.Time(任意の時間ステップで選出されたすべてのプロセス) がまさにすべてのプロセスのセットであることを示しています。これは明らかに、アサーションの名前が示唆するように、「1 つのプロセスのみが選出される」という意味ではありません。
于 2012-11-29T17:23:43.917 に答える