在Alloy中传播令牌-Java 学习之路

我是一本优秀的书（Software Abstractions)，特别是他为了选举领导者而设置了令牌环的例子 .

我正在尝试扩展此示例（Ring election）以确保令牌（而不是限制为1）在所提供的时间内传递给所有成员（并且每个成员仅被选举一次，而不是多次） . 然而（主要是由于我在Alloy方面的经验不足），我认为我可以和一些操作员一起玩（改变 - 但是我似乎并没有完全击中头部 .

以下是示例中的代码 . 我已经在几个方面标记了问题......任何和所有帮助都表示赞赏 . 我正在使用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

1 回答

1
- 这个网络协议正是关于如何选择一个进程成为领导者，所以我真的不明白你的想法的含义"all processes elected eventually" .
- 而不是 all elected.Time ，您可以等效地写 elected.Time = Process （因为 elected 的类型是 Process -> Time ） . 这只是说 elected.Time （在任何时间步骤选出的所有进程）都是所有进程的集合，显然，这并不意味着"only one process is elected"，正如你的断言名称所暗示的那样 .
回复于 2024-04-29T01:36:27+08:00

在Alloy中传播令牌

1 回答

相关问题