1

我想运行Raft 的 TLA+ 实现，所以我构建了一个新模块，并设置如下：

在此处输入图像描述

但是，TLC 会产生很多状态，而且似乎永远不会停止。

在此处输入图像描述

根据Lamport 的 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 Spec 上正确运行 TLC？

---更新--- 我在问题 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,2,3,4,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。

4

0 回答 0