我的老师让我们在 Promela 中编写 Dijkstra 的令牌终止算法。这是算法：
“每个节点都维护一个计数器 c。发送消息将 c 加一；收到消息将 c 减一。因此，所有计数器的总和等于网络中未决消息的数量。当节点 0 启动检测探测时，它向节点 N-1 发送一个值为 0 的令牌。每个节点 i 保留令牌直到它变为被动；然后它将令牌转发给节点 i-1，将令牌值增加 c。每个节点和令牌都有一个颜色（最初全白）。当节点收到消息时，节点变为黑色。当节点转发令牌时，节点变为白色。如果黑色机器转发令牌，则令牌变为黑色；否则令牌保持其颜色. 当节点 0 再次收到令牌时，可以结束，如果节点 0 是被动白色，则令牌是白色的，令牌值与 c 之和为 0。否则，节点 0 可能会启动新的探测。”
我有点明白这个想法，但我很难真正理解发生了什么。如果有人可以帮助准确地解释算法正在逐步执行的操作，那就太好了。此外，虽然我不希望任何人为我编写代码，但有关如何开始的任何提示都会有所帮助。