modeling - 如何在 TLA+ Toolbox 中建模 Paxos？

Question

我尝试在 TLA+ Toolbox（工具箱）中建模 Paxos（ Paxos 示例）。我应该在模型中输入什么数字才能使其工作？或者还有其他方法可以在这个工具箱中确认这个算法吗？

基于此代码：

CONSTANT Value,     \* The set of choosable values.
     Acceptor,  \* A set of processes that will choose a value.
     Quorum     \* The set of "quorums", where a quorum" is a 
                \*   "large enough" set of acceptors

我尝试这样的数字：

接受者 <- [11,12,13,14,15];

法定人数 <- [11,12,13,14,15,16,17,18,19];

值 <- [0,1]；

但我收到 ArrayIndexOutOfBoundsException 错误。

Answer 1

您的模型存在一些问题：

1. 要指定一个集合，您应该使用花括号，因此 Acceptor <- {11,12,13,14,15}。

2. Quorum 应该是一组接受者，例如 Quorum <- {{11,12,13},{12,13,14}}。