如何在TLA+工具箱中建模Paxos？
如何在TLA+工具箱中建模Paxos？
提问于 2016-05-01 14:51:21
我尝试在Paxos示例工具箱( TLA+ Toolbox，工具箱)中建模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错误。
回答 1
Stack Overflow用户
回答已采纳
发布于 2016-08-22 15:54:08
您的模型有几个问题：
- 对于指定集合，您应该使用大括号，因此受主<- {11,12,13,14,15}。
- 法定人数应是一组承兑者，例如法定人数<- {11，12，13}，{12，13，14}。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/36967985
复制相关文章
相似问题
腾讯云开发者
