Блог

Я хочу запустить реализацию TLA Raft, поэтому я создаю новый модуль и настраиваю его следующим образом:

Однако TLC генерирует множество состояний, и кажется, что это никогда не прекратится.

И мне пришло в голову, что, возможно, мне следует ограничить длину messages и некоторые другие переменные, согласно лекции 09 Лэмпорта.

Поэтому я добавляю следующий код в «Ограничение состояния».

 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)
 

И я в замешательстве по этому поводу. Мой вопрос в том, как я могу правильно запустить TLC в спецификации TLA Raft?

— ОБНОВЛЕНИЕ — Я нахожу конфигурацию в выпуске 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 и так далее.