[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] TLC report an unexpected runtime error
While I was check a Raft TLA+ spec using TLC, it report an unexpected runtime error that:
```txt
Error: 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
: Attempted to apply tuple
<<>>
to integer 1 which is out of domain.
Error: The behavior up to this point is:
...
```
the TLA+ code trigger this error was at line `364 /\ log[i][index].term = m.mentries[1].term` which I think it should not happend since line `362 /\ \/ m.mentries = << >>` has a check that ensure `m.mentries` is no empty:
```txt
360 /\ LET index == m.mprevLogIndex + 1
361 IN \/ \* already done with request
362 /\ \/ m.mentries = << >>
363 \/ /\ Len(log[i]) >= index
364 /\ log[i][index].term = m.mentries[1].term
365 \* This could make our commitIndex decrease (for
366 \* example if we process an old, duplicated request),
367 \* but that doesn't really affect anything.
```
So how could this happend?
The whold TLA+ spec and config can be found here: https://github.com/kikimo/tla-checks/tree/master/cli_raft
and the whole errror report:
```txt
TLC2 Version 2.16 of 31 December 2020 (rev: cdddf55)
Running breadth-first search Model-Checking with fp 66 and seed -5673513601640176068 with 32 workers on 128 cores with 58254MB heap and 64MB offheap memory (L
inux 5.4.151-1.el7.elrepo.x86_64 amd64, Oracle Corporation 1.8.0_271 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /data/src/raft/raft.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/TLC.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module raft
Starting... (2022-12-01 18:43:21)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2022-12-01 18:43:21.
Progress(13) at 2022-12-01 18:43:25: 2,114,544 states generated (2,114,544 s/min), 401,778 distinct states found (401,778 ds/min), 298,959 states left on queu
e.
Progress(15) at 2022-12-01 18:44:25: 88,608,361 states generated (86,493,817 s/min), 13,078,913 distinct states found (12,677,135 ds/min), 9,635,911 states le
ft on queue.
Progress(16) at 2022-12-01 18:45:25: 198,657,892 states generated (110,049,531 s/min), 27,818,804 distinct states found (14,739,891 ds/min), 20,237,432 states
left on queue.
Progress(16) at 2022-12-01 18:46:25: 320,820,421 states generated (122,162,529 s/min), 43,590,049 distinct states found (15,771,245 ds/min), 31,857,906 states
left on queue.
Progress(16) at 2022-12-01 18:47:25: 448,026,717 states generated (127,206,296 s/min), 58,642,657 distinct states found (15,052,608 ds/min), 42,239,156 states
left on queue.
Progress(17) at 2022-12-01 18:48:25: 581,330,557 states generated (133,303,840 s/min), 74,084,138 distinct states found (15,441,481 ds/min), 52,513,520 states
left on queue.
Progress(17) at 2022-12-01 18:49:25: 716,841,744 states generated (135,511,187 s/min), 92,510,693 distinct states found (18,426,555 ds/min), 66,588,941 states
left on queue.
Progress(17) at 2022-12-01 18:50:25: 855,693,652 states generated (138,851,908 s/min), 109,405,350 distinct states found (16,894,657 ds/min), 79,003,367 state
s left on queue.
Progress(17) at 2022-12-01 18:51:25: 993,618,083 states generated (137,924,431 s/min), 126,848,578 distinct states found (17,443,228 ds/min), 92,071,593 state
s left on queue.
Progress(17) at 2022-12-01 18:52:25: 1,136,521,786 states generated (142,903,703 s/min), 143,198,622 distinct states found (16,350,044 ds/min), 103,932,798 st
ates left on queue.
Progress(17) at 2022-12-01 18:53:25: 1,289,912,910 states generated (153,391,124 s/min), 160,656,788 distinct states found (17,458,166 ds/min), 116,088,463 st
ates left on queue.
Progress(17) at 2022-12-01 18:54:25: 1,448,748,507 states generated (158,835,597 s/min), 178,651,662 distinct states found (17,994,874 ds/min), 128,607,956 st
ates left on queue.
Progress(17) at 2022-12-01 18:55:25: 1,611,996,346 states generated (163,247,839 s/min), 196,511,563 distinct states found (17,859,901 ds/min), 140,833,141 st
ates left on queue.
Error: 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
: Attempted to apply tuple
<<>>
to integer 1 which is out of domain.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ elections = {}
/\ messages = << >>
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Follower @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1)
/\ votesResponded = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> << >> @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> Nil @@ s2 :> Nil @@ s3 :> Nil)
State 2: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = {}
/\ messages = << >>
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Follower @@ s2 :> Candidate @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 1 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> << >> @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> Nil @@ s2 :> Nil @@ s3 :> Nil)
State 3: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = {}
/\ messages = << >>
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Follower @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 1 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> << >> @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> Nil @@ s2 :> Nil @@ s3 :> Nil)
State 4: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = {}
/\ messages = << >>
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Candidate @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> << >> @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> Nil @@ s2 :> Nil @@ s3 :> Nil)
State 5: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = {}
/\ messages = ( [ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s1 ] :>
1 )
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Candidate @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> << >> @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> Nil @@ s2 :> Nil @@ s3 :> Nil)
State 6: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = {}
/\ messages = ( [ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s1 ] :>
1 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s2 ] :>
1 )
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Candidate @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> << >> @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> Nil @@ s2 :> Nil @@ s3 :> Nil)
State 7: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = {}
/\ messages = ( [ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s1,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
1 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s1 ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s2 ] :>
1 )
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Candidate @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> << >> @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> s1 @@ s2 :> Nil @@ s3 :> Nil)
State 8: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = {}
/\ messages = ( [ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s1,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s1 ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s2 ] :>
1 )
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Candidate @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {s1} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {s1} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> (s1 :> <<>>) @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> s1 @@ s2 :> Nil @@ s3 :> Nil)
State 9: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = {}
/\ messages = ( [ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s1,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s2,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
1 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s1 ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s2 ] :>
0 )
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Candidate @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {s1} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {s1} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> (s1 :> <<>>) @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> s1 @@ s2 :> s1 @@ s3 :> Nil)
State 10: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = {}
/\ messages = ( [ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s1,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s2,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s1 ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s2 ] :>
0 )
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Candidate @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> (s1 :> <<>> @@ s2 :> <<>>) @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> s1 @@ s2 :> s1 @@ s3 :> Nil)
State 11: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = { [ eterm |-> 2,
eleader |-> s1,
elog |-> <<>>,
evotes |-> {s1, s2},
evoterLog |-> (s1 :> <<>> @@ s2 :> <<>>) ] }
/\ messages = ( [ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s1,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s2,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s1 ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s2 ] :>
0 )
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Leader @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> (s1 :> <<>> @@ s2 :> <<>>) @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> s1 @@ s2 :> s1 @@ s3 :> Nil)
State 12: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = { [ eterm |-> 2,
eleader |-> s1,
elog |-> <<>>,
evotes |-> {s1, s2},
evoterLog |-> (s1 :> <<>> @@ s2 :> <<>>) ] }
/\ messages = ( [ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s1,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s2,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s1 ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s2 ] :>
0 @@
[ mtype |-> AppendEntriesRequest,
mterm |-> 2,
msource |-> s1,
mdest |-> s2,
mprevLogIndex |-> 0,
mprevLogTerm |-> 0,
mentries |-> <<>>,
mlog |-> <<>>,
mcommitIndex |-> 0 ] :>
1 )
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Leader @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> (s1 :> <<>> @@ s2 :> <<>>) @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> s1 @@ s2 :> s1 @@ s3 :> Nil)
State 13: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = { [ eterm |-> 2,
eleader |-> s1,
elog |-> <<>>,
evotes |-> {s1, s2},
evoterLog |-> (s1 :> <<>> @@ s2 :> <<>>) ] }
/\ messages = ( [ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s1,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s2,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s1 ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s2 ] :>
0 @@
[ mtype |-> AppendEntriesRequest,
mterm |-> 2,
msource |-> s1,
mdest |-> s2,
mprevLogIndex |-> 0,
mprevLogTerm |-> 0,
mentries |-> <<>>,
mlog |-> <<>>,
mcommitIndex |-> 0 ] :>
1 )
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<[term |-> 2, value |-> v3]>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Leader @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> (s1 :> <<>> @@ s2 :> <<>>) @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> s1 @@ s2 :> s1 @@ s3 :> Nil)
State 14: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = { [ eterm |-> 2,
eleader |-> s1,
elog |-> <<>>,
evotes |-> {s1, s2},
evoterLog |-> (s1 :> <<>> @@ s2 :> <<>>) ] }
/\ messages = ( [ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s1,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s2,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s1 ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s2 ] :>
0 @@
[ mtype |-> AppendEntriesRequest,
mterm |-> 2,
msource |-> s1,
mdest |-> s2,
mprevLogIndex |-> 0,
mprevLogTerm |-> 0,
mentries |-> <<>>,
mlog |-> <<>>,
mcommitIndex |-> 0 ] :>
1 @@
[ mtype |-> AppendEntriesRequest,
mterm |-> 2,
msource |-> s1,
mdest |-> s2,
mprevLogIndex |-> 0,
mprevLogTerm |-> 0,
mentries |-> <<[term |-> 2, value |-> v3]>>,
mlog |-> <<[term |-> 2, value |-> v3]>>,
mcommitIndex |-> 0 ] :>
1 )
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = (s1 :> <<[term |-> 2, value |-> v3]>> @@ s2 :> <<>> @@ s3 :> <<>>)
/\ state = (s1 :> Leader @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>, <<[term |-> 2, value |-> v3]>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> (s1 :> <<>> @@ s2 :> <<>>) @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> s1 @@ s2 :> s1 @@ s3 :> Nil)
State 15: <Next line 458, col 9 to line 469, col 58 of module raft>
/\ elections = { [ eterm |-> 2,
eleader |-> s1,
elog |-> <<>>,
evotes |-> {s1, s2},
evoterLog |-> (s1 :> <<>> @@ s2 :> <<>>) ] }
/\ messages = ( [ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s1,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteResponse,
mterm |-> 2,
msource |-> s2,
mdest |-> s1,
mlog |-> <<>>,
mvoteGranted |-> TRUE ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s1 ] :>
0 @@
[ mtype |-> RequestVoteRequest,
mterm |-> 2,
mlastLogTerm |-> 0,
mlastLogIndex |-> 0,
msource |-> s1,
mdest |-> s2 ] :>
0 @@
[ mtype |-> AppendEntriesRequest,
mterm |-> 2,
msource |-> s1,
mdest |-> s2,
mprevLogIndex |-> 0,
mprevLogTerm |-> 0,
mentries |-> <<>>,
mlog |-> <<>>,
mcommitIndex |-> 0 ] :>
1 @@
[ mtype |-> AppendEntriesRequest,
mterm |-> 2,
msource |-> s1,
mdest |-> s2,
mprevLogIndex |-> 0,
mprevLogTerm |-> 0,
mentries |-> <<[term |-> 2, value |-> v3]>>,
mlog |-> <<[term |-> 2, value |-> v3]>>,
mcommitIndex |-> 0 ] :>
1 )
/\ matchIndex = ( s1 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s2 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) @@
s3 :> (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0) )
/\ log = ( s1 :> <<[term |-> 2, value |-> v3]>> @@
s2 :> <<[term |-> 2, value |-> v3]>> @@
s3 :> <<>> )
/\ state = (s1 :> Leader @@ s2 :> Follower @@ s3 :> Follower)
/\ allLogs = {<<>>, <<[term |-> 2, value |-> v3]>>}
/\ commitIndex = (s1 :> 0 @@ s2 :> 0 @@ s3 :> 0)
/\ currentTerm = (s1 :> 2 @@ s2 :> 2 @@ s3 :> 1)
/\ votesResponded = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ nextIndex = ( s1 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s2 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) @@
s3 :> (s1 :> 1 @@ s2 :> 1 @@ s3 :> 1) )
/\ votesGranted = (s1 :> {s1, s2} @@ s2 :> {} @@ s3 :> {})
/\ voterLog = (s1 :> (s1 :> <<>> @@ s2 :> <<>>) @@ s2 :> << >> @@ s3 :> << >>)
/\ votedFor = (s1 :> s1 @@ s2 :> s1 @@ s3 :> Nil)
Error: The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 458, column 9 to line 469, column 58 in raft
1. Line 458, column 12 to line 467, column 55 in raft
2. Line 465, column 15 to line 465, column 51 in raft
3. Line 465, column 42 to line 465, column 51 in raft
4. Line 426, column 5 to line 440, column 52 in raft
5. Line 430, column 8 to line 440, column 52 in raft
6. Line 436, column 11 to line 437, column 48 in raft
7. Line 436, column 14 to line 436, column 43 in raft
8. Line 437, column 14 to line 437, column 48 in raft
9. Line 333, column 5 to line 393, column 49 in raft
10. Line 337, column 8 to line 393, column 49 in raft
11. Line 337, column 11 to line 337, column 35 in raft
12. Line 338, column 11 to line 392, column 73 in raft
13. Line 357, column 14 to line 392, column 73 in raft
14. Line 357, column 17 to line 357, column 40 in raft
15. Line 358, column 17 to line 358, column 35 in raft
16. Line 359, column 17 to line 359, column 21 in raft
17. Line 333, column 18 to line 336, column 68 in raft
18. Line 333, column 21 to line 333, column 39 in raft
19. Line 360, column 17 to line 392, column 73 in raft
20. Line 361, column 20 to line 392, column 73 in raft
21. Line 362, column 24 to line 378, column 59 in raft
22. Line 362, column 27 to line 364, column 71 in raft
23. Line 363, column 30 to line 364, column 71 in raft
24. Line 363, column 33 to line 363, column 52 in raft
25. Line 364, column 33 to line 364, column 71 in raft
26. Line 364, column 54 to line 364, column 71 in raft
27. Line 364, column 54 to line 364, column 66 in raft
1736283024 states generated, 208856733 distinct states found, 148457799 states left on queue.
Finished in 12min 46s at (2022-12-01 18:56:07)
```
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/473c9b3f-5966-4903-9d58-e5bab1784eb2n%40googlegroups.com.