如何解决如何在 Raft 的 TLA+ 上运行 TLC 检查器?
我想运行 Raft's TLA+ implementation,所以我构建了一个新模块,并设置如下:
然而,TLC 产生了很多状态,而且似乎永远不会停止。
我突然想到,根据 Lamport's Lecture 09,我可能应该限制 messages
的长度和其他一些变量。
Len(messages) =< 10
但是,它现在抛出以下错误
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: tlc2.tool.EvalException:
The argument of Len should be a sequence,but instead it is:
( [ mtype |-> RequestVoteRequest,mterm |-> 2,mlastLogTerm |-> 0,mlastLogIndex |-> 0,msource |-> r2,mdest |-> r1 ] :>
1 )
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. /\ Len(messages) =< 10
1. Len(messages) =< 10
2. Len(messages)
我对此感到困惑。我的问题是如何在 Raft 的 TLA 规范上正确运行 TLC?
--- 更新 --- 我在 Issue 1
中找到了一个配置CONSTANTS Server = {r1,r2,r3}
Value = {v1,v2}
Follower = Follower
Candidate = Candidate
leader = leader
Nil = Nil
RequestVoteRequest = RequestVoteRequest
RequestVoteResponse = RequestVoteResponse
AppendEntriesRequest = AppendEntriesRequest
AppendEntriesResponse = AppendEntriesResponse
TLC_MAX_TERM = 3
TLC_MAX_ENTRY = 1
TLC_MAX_MESSAGE = 1
\* PNat = {1,2,3,4,5}
\* Nat = {0,1,5}
\*SYMMETRY Perms
SPECIFICATION Spec
\*CONSTRAINT TermConstraint
\*CONSTRAINT LogConstraint
\*CONSTRAINT MessageConstraint
\*INVARIANT AtMostOneleaderPerTerm
\*INVARIANT TermAndindexDeterminesLogPrefix
\*INVARIANT StateMachinesafety
\*INVARIANT NewleaderHasCompleteLog
\*INVARIANT CommitInorder
\*INVARIANT MessageTypeInv
\*INVARIANT TypeInv
但是,我不知道如何使用它,因为我没有TermConstraint
之类的定义。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。