1

我的老师让我们在 Promela 中编写 Dijkstra 的令牌终止算法。这是算法:

“每个节点都维护一个计数器 c。发送消息将 c 加一;收到消息将 c 减一。因此,所有计数器的总和等于网络中未决消息的数量。当节点 0 启动检测探测时,它向节点 N-1 发送一个值为 0 的令牌。每个节点 i 保留令牌直到它变为被动;然后它将令牌转发给节点 i-1,将令牌值增加 c。每个节点和令牌都有一个颜色(最初全白)。当节点收到消息时,节点变为黑色。当节点转发令牌时,节点变为白色。如果黑色机器转发令牌,则令牌变为黑色;否则令牌保持其颜色. 当节点 0 再次收到令牌时,可以结束,如果节点 0 是被动白色,则令牌是白色的,令牌值与 c 之和为 0。否则,节点 0 可能会启动新的探测。”

我有点明白这个想法,但我很难真正理解发生了什么。如果有人可以帮助准确地解释算法正在逐步执行的操作,那就太好了。此外,虽然我不希望任何人为我编写代码,但有关如何开始的任何提示都会有所帮助。

4

0 回答 0