2 node raft spec #2
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Violation of java -XX:+UseParallelGC -DTLA-Library=.. -Dtlc2.output.MP.warning2error=true -Dtlc2.tool.impl.Tool.cdot=true -Dtlc2.value.Values.width=999999 -DOFFtlc2.tool.queue.IStateQueue=StateDeque -cp /Users/markus/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.5.2906/tools/tla2tools.jar -DTLA-Library= -Dtlc2.TLC.ide=vscode tlc2.TLC MCextendedraft.tla -tool -modelcheck -config MCextendedraft.cfg
TLC2 Version 2.18 of Day Month 20?? (rev: 7279336)
Running breadth-first search Model-Checking with fp 2 and seed -2619444902489916522 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 15931] (Mac OS X 13.6.7 aarch64, Homebrew 11.0.23 x86_64, MSBDiskFPSet, DiskStateQueue).
Starting SANY...
Parsing file /Users/markus/src/TLA/_specs/MSFT/extended-raft-paper/tla/MCextendedraft.tla
Parsing file /Users/markus/src/TLA/_specs/MSFT/extended-raft-paper/tla/extendedraft.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-2491281636660094416/TLC.tla (jar:file:/Users/markus/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.5.2906/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-2491281636660094416/Functions.tla (jar:file:/Users/markus/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.5.2906/tools/CommunityModules-deps.jar!/Functions.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-2491281636660094416/Bags.tla (jar:file:/Users/markus/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.5.2906/tools/tla2tools.jar!/tla2sany/StandardModules/Bags.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-2491281636660094416/Naturals.tla (jar:file:/Users/markus/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.5.2906/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-2491281636660094416/FiniteSets.tla (jar:file:/Users/markus/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.5.2906/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-2491281636660094416/Sequences.tla (jar:file:/Users/markus/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.5.2906/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-2491281636660094416/SequencesExt.tla (jar:file:/Users/markus/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.5.2906/tools/CommunityModules-deps.jar!/SequencesExt.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-2491281636660094416/FiniteSetsExt.tla (jar:file:/Users/markus/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.5.2906/tools/CommunityModules-deps.jar!/FiniteSetsExt.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-2491281636660094416/Folds.tla (jar:file:/Users/markus/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.5.2906/tools/CommunityModules-deps.jar!/Folds.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 Bags
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module SequencesExt
Semantic processing of module extendedraft
Semantic processing of module MCextendedraft
SANY finished.
Starting... (2024-05-31 15:15:22)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-05-31 15:15:22.
Progress(15) at 2024-05-31 15:15:25: 70,331 states generated (70,331 s/min), 21,204 distinct states found (21,204 ds/min), 12,900 states left on queue.
Progress(18) at 2024-05-31 15:16:25: 2,137,487 states generated (2,067,156 s/min), 785,320 distinct states found (764,116 ds/min), 550,760 states left on queue.
Progress(19) at 2024-05-31 15:17:25: 4,223,915 states generated (2,086,428 s/min), 1,540,369 distinct states found (755,049 ds/min), 1,081,472 states left on queue.
Progress(19) at 2024-05-31 15:18:25: 6,300,831 states generated (2,076,916 s/min), 2,268,312 distinct states found (727,943 ds/min), 1,597,884 states left on queue.
Progress(19) at 2024-05-31 15:19:25: 8,337,909 states generated (2,037,078 s/min), 2,954,585 distinct states found (686,273 ds/min), 2,066,538 states left on queue.
Progress(19) at 2024-05-31 15:20:25: 10,446,443 states generated (2,108,534 s/min), 3,692,223 distinct states found (737,638 ds/min), 2,587,398 states left on queue.
Progress(19) at 2024-05-31 15:21:25: 12,519,331 states generated (2,072,888 s/min), 4,400,938 distinct states found (708,715 ds/min), 3,075,555 states left on queue.
Progress(20) at 2024-05-31 15:22:25: 14,575,935 states generated (2,056,604 s/min), 5,135,681 distinct states found (734,743 ds/min), 3,598,817 states left on queue.
Checkpointing of run states/24-05-31-15-15-22.102
Checkpointing completed at (2024-05-31 18:21:36)
Progress(20) at 2024-05-31 18:21:36: 16,635,546 states generated (2,059,611 s/min), 5,841,440 distinct states found (705,759 ds/min), 4,103,470 states left on queue.
Checkpointing of run states/24-05-31-15-15-22.102
Checkpointing completed at (2024-06-01 01:33:44)
Progress(20) at 2024-06-01 01:33:44: 18,655,890 states generated (2,020,344 s/min), 6,512,660 distinct states found (671,220 ds/min), 4,573,133 states left on queue.
Checkpointing of run states/24-05-31-15-15-22.102
Checkpointing completed at (2024-06-01 12:57:08)
Progress(20) at 2024-06-01 12:57:08: 20,645,438 states generated (1,989,548 s/min), 7,187,916 distinct states found (675,256 ds/min), 5,048,552 states left on queue.
Checkpointing of run states/24-05-31-15-15-22.102
Checkpointing completed at (2024-06-01 16:07:34)
Progress(20) at 2024-06-01 16:07:34: 22,729,385 states generated (2,083,947 s/min), 7,848,809 distinct states found (660,893 ds/min), 5,502,441 states left on queue.
Progress(20) at 2024-06-01 16:28:14: 24,682,852 states generated (1,953,467 s/min), 8,474,971 distinct states found (626,162 ds/min), 5,925,951 states left on queue.
Progress(20) at 2024-06-01 16:29:14: 26,707,758 states generated (2,024,906 s/min), 9,127,652 distinct states found (652,681 ds/min), 6,366,539 states left on queue.
Progress(20) at 2024-06-01 16:30:14: 28,685,766 states generated (1,978,008 s/min), 9,791,491 distinct states found (663,839 ds/min), 6,820,071 states left on queue.
Invariant QuorumLogInv is violated.
The behavior up to this point is:
1: <Initial predicate>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<0, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 0, hadNumClientRequests |-> 0, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 2}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<1, 1, 1>>
/\ votedFor = <<Nil, Nil, Nil>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {}
/\ state = <<Follower, Follower, Follower>>
/\ voterLog = <<<<>>, <<>>, <<>>>>
/\ messages = <<>>
/\ log = <<<<>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{}, {}, {}>>
2: <MCTimeout(1) line 103, col 5 to line 105, col 68 of module MCextendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<0, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 0, hadNumClientRequests |-> 0, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 2}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 1>>
/\ votedFor = <<Nil, Nil, Nil>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {}
/\ state = <<Candidate, Follower, Follower>>
/\ voterLog = <<<<>>, <<>>, <<>>>>
/\ messages = <<>>
/\ log = <<<<>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{}, {}, {}>>
3: <MCRequestVote(1,1) line 95, col 5 to line 96, col 28 of module MCextendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<0, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 0, hadNumClientRequests |-> 0, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 2}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 1>>
/\ votedFor = <<Nil, Nil, Nil>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {}
/\ state = <<Candidate, Follower, Follower>>
/\ voterLog = <<<<>>, <<>>, <<>>>>
/\ messages = ([mtype |-> RequestVoteRequest, mterm |-> 2, mlastLogTerm |-> 0, mlastLogIndex |-> 0, msource |-> 1, mdest |-> 1] :> 1)
/\ log = <<<<>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{}, {}, {}>>
4: <NextRequestVoteRequest line 644, col 27 to line 644, col 95 of module extendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<0, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 0, hadNumClientRequests |-> 0, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 2}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 1>>
/\ votedFor = <<1, Nil, Nil>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {}
/\ state = <<Candidate, Follower, Follower>>
/\ voterLog = <<<<>>, <<>>, <<>>>>
/\ messages = ([mtype |-> RequestVoteResponse, mterm |-> 2, msource |-> 1, mdest |-> 1, mlog |-> <<>>, mvoteGranted |-> TRUE] :> 1)
/\ log = <<<<>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{}, {}, {}>>
5: <NextRequestVoteResponse line 645, col 28 to line 645, col 97 of module extendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<0, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 0, hadNumClientRequests |-> 0, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 2}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 1>>
/\ votedFor = <<1, Nil, Nil>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {}
/\ state = <<Candidate, Follower, Follower>>
/\ voterLog = <<<<<<>>>>, <<>>, <<>>>>
/\ messages = <<>>
/\ log = <<<<>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1}, {}, {}>>
6: <MCRequestWitnessVote(1) line 99, col 5 to line 100, col 28 of module MCextendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<0, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 0, hadNumClientRequests |-> 0, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 2}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 1>>
/\ votedFor = <<1, Nil, Nil>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {}
/\ state = <<Candidate, Follower, Follower>>
/\ voterLog = <<<<<<>>>>, <<>>, <<>>>>
/\ messages = ([mtype |-> RequestWitnessVoteRequest, mterm |-> 2, mlastLogTerm |-> 0, msource |-> 1, mdest |-> 3, mlastLogSubterm |-> 0, mvotesGranted |-> {1}] :> 1)
/\ log = <<<<>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1}, {}, {}>>
7: <NextRequestWitnessVoteRequest line 646, col 34 to line 646, col 109 of module extendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<0, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 0, hadNumClientRequests |-> 0, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 2}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, Nil>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {}
/\ state = <<Candidate, Follower, Follower>>
/\ voterLog = <<<<<<>>>>, <<>>, <<>>>>
/\ messages = ([mtype |-> RequestWitnessVoteRequest, mterm |-> 2, mlastLogTerm |-> 0, msource |-> 1, mdest |-> 3, mlastLogSubterm |-> 0, mvotesGranted |-> {1}] :> 1)
/\ log = <<<<>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1}, {}, {}>>
8: <NextRequestWitnessVoteRequest line 646, col 34 to line 646, col 109 of module extendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<0, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 0, hadNumClientRequests |-> 0, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 2}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {}
/\ state = <<Candidate, Follower, Follower>>
/\ voterLog = <<<<<<>>>>, <<>>, <<>>>>
/\ messages = ([mtype |-> RequestVoteResponse, mterm |-> 2, msource |-> 3, mdest |-> 1, mlog |-> <<>>, mvoteGranted |-> TRUE] :> 1)
/\ log = <<<<>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1}, {}, {}>>
9: <NextRequestVoteResponse line 645, col 28 to line 645, col 97 of module extendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<0, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 0, hadNumClientRequests |-> 0, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 2}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {}
/\ state = <<Candidate, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = <<>>
/\ log = <<<<>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
10: <MCBecomeLeader(1) line 83, col 5 to line 84, col 61 of module MCextendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<0, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 1, hadNumClientRequests |-> 0, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 2}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {[eterm |-> 2, eleader |-> 1, elog |-> <<>>, evotes |-> {1, 3}, evoterLog |-> (1 :> <<>> @@ 3 :> <<>>)]}
/\ state = <<Leader, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = <<>>
/\ log = <<<<>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
11: <MCAdjustReplicationSet(1,{1, 3}) line 69, col 5 to line 71, col 82 of module MCextendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<1, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 1], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 1, hadNumClientRequests |-> 0, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 3}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {[eterm |-> 2, eleader |-> 1, elog |-> <<>>, evotes |-> {1, 3}, evoterLog |-> (1 :> <<>> @@ 3 :> <<>>)]}
/\ state = <<Leader, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = <<>>
/\ log = <<<<>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
12: <MCClientRequest(1,v1) line 78, col 5 to line 80, col 68 of module MCextendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<1, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 1], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 1, hadNumClientRequests |-> 1, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 3}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {[eterm |-> 2, eleader |-> 1, elog |-> <<>>, evotes |-> {1, 3}, evoterLog |-> (1 :> <<>> @@ 3 :> <<>>)]}
/\ state = <<Leader, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = <<>>
/\ log = <<<<[term |-> 2, subterm |-> 1, value |-> v1]>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
13: <MCAppendEntriesToWitness(1) line 91, col 5 to line 92, col 28 of module MCextendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<1, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 1], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 1, hadNumClientRequests |-> 1, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 3}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {<<2, 1>>}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {[eterm |-> 2, eleader |-> 1, elog |-> <<>>, evotes |-> {1, 3}, evoterLog |-> (1 :> <<>> @@ 3 :> <<>>)]}
/\ state = <<Leader, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = ([mtype |-> AppendEntriesToWitnessRequest, mterm |-> 2, msource |-> 1, mdest |-> 3, mentries |-> <<[term |-> 2, subterm |-> 1, value |-> v1]>>, mlog |-> <<[term |-> 2, subterm |-> 1, value |-> v1]>>, mlogTerm |-> 2, mlogSubterm |-> 1, mreplicationSet |-> {1, 3}, mindex |-> 1] :> 1)
/\ log = <<<<[term |-> 2, subterm |-> 1, value |-> v1]>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
14: <MCClientRequest(1,v1) line 78, col 5 to line 80, col 68 of module MCextendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<1, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 1], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 1, hadNumClientRequests |-> 2, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 3}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {<<2, 1>>}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {[eterm |-> 2, eleader |-> 1, elog |-> <<>>, evotes |-> {1, 3}, evoterLog |-> (1 :> <<>> @@ 3 :> <<>>)]}
/\ state = <<Leader, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = ([mtype |-> AppendEntriesToWitnessRequest, mterm |-> 2, msource |-> 1, mdest |-> 3, mentries |-> <<[term |-> 2, subterm |-> 1, value |-> v1]>>, mlog |-> <<[term |-> 2, subterm |-> 1, value |-> v1]>>, mlogTerm |-> 2, mlogSubterm |-> 1, mreplicationSet |-> {1, 3}, mindex |-> 1] :> 1)
/\ log = <<<<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
15: <MCAppendEntriesToWitness(1) line 91, col 5 to line 92, col 28 of module MCextendedraft>
/\ witnessLastLogTerm = 0
/\ currentSubterm = <<1, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 1], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 1, hadNumClientRequests |-> 2, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 2}
/\ replicationSet = <<{1, 3}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 0
/\ witnessAcks = {<<2, 1>>, <<2, 2>>}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {[eterm |-> 2, eleader |-> 1, elog |-> <<>>, evotes |-> {1, 3}, evoterLog |-> (1 :> <<>> @@ 3 :> <<>>)]}
/\ state = <<Leader, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = ([mtype |-> AppendEntriesToWitnessRequest, mterm |-> 2, msource |-> 1, mdest |-> 3, mentries |-> <<[term |-> 2, subterm |-> 1, value |-> v1]>>, mlog |-> <<[term |-> 2, subterm |-> 1, value |-> v1]>>, mlogTerm |-> 2, mlogSubterm |-> 1, mreplicationSet |-> {1, 3}, mindex |-> 1] :> 1 @@ [mtype |-> AppendEntriesToWitnessRequest, mterm |-> 2, msource |-> 1, mdest |-> 3, mentries |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlog |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlogTerm |-> 2, mlogSubterm |-> 1, mreplicationSet |-> {1, 3}, mindex |-> 2] :> 1)
/\ log = <<<<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, <<>>, <<>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
16: <NextAppendEntriesToWitnessRequest line 649, col 38 to line 649, col 117 of module extendedraft>
/\ witnessLastLogTerm = 2
/\ currentSubterm = <<1, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 1], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 1, hadNumClientRequests |-> 2, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 3}
/\ replicationSet = <<{1, 3}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 1>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 1
/\ witnessAcks = {<<2, 1>>, <<2, 2>>}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {[eterm |-> 2, eleader |-> 1, elog |-> <<>>, evotes |-> {1, 3}, evoterLog |-> (1 :> <<>> @@ 3 :> <<>>)]}
/\ state = <<Leader, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = ([mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> 3, mdest |-> 1, msuccess |-> TRUE, mmatchIndex |-> 1] :> 1 @@ [mtype |-> AppendEntriesToWitnessRequest, mterm |-> 2, msource |-> 1, mdest |-> 3, mentries |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlog |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlogTerm |-> 2, mlogSubterm |-> 1, mreplicationSet |-> {1, 3}, mindex |-> 2] :> 1)
/\ log = <<<<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, <<>>, <<[term |-> 2, subterm |-> 1, value |-> v1]>>>>
/\ witnessSubterm = <<0, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
17: <NextAppendEntriesResponse line 648, col 30 to line 648, col 101 of module extendedraft>
/\ witnessLastLogTerm = 2
/\ currentSubterm = <<1, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 1], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 1, hadNumClientRequests |-> 2, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 3}
/\ replicationSet = <<{1, 3}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 2>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 1>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 1
/\ witnessAcks = {<<2, 1>>, <<2, 2>>}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {[eterm |-> 2, eleader |-> 1, elog |-> <<>>, evotes |-> {1, 3}, evoterLog |-> (1 :> <<>> @@ 3 :> <<>>)]}
/\ state = <<Leader, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = ([mtype |-> AppendEntriesToWitnessRequest, mterm |-> 2, msource |-> 1, mdest |-> 3, mentries |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlog |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlogTerm |-> 2, mlogSubterm |-> 1, mreplicationSet |-> {1, 3}, mindex |-> 2] :> 1)
/\ log = <<<<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, <<>>, <<[term |-> 2, subterm |-> 1, value |-> v1]>>>>
/\ witnessSubterm = <<1, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
18: <MCAppendEntriesToWitness(1) line 91, col 5 to line 92, col 28 of module MCextendedraft>
/\ witnessLastLogTerm = 2
/\ currentSubterm = <<1, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 1], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 1, hadNumClientRequests |-> 2, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 3}
/\ replicationSet = <<{1, 3}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 2>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 1>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 1
/\ witnessAcks = {<<2, 1>>, <<2, 2>>}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {[eterm |-> 2, eleader |-> 1, elog |-> <<>>, evotes |-> {1, 3}, evoterLog |-> (1 :> <<>> @@ 3 :> <<>>)]}
/\ state = <<Leader, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = ([mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> 3, mdest |-> 1, msuccess |-> TRUE, mmatchIndex |-> 2] :> 1 @@ [mtype |-> AppendEntriesToWitnessRequest, mterm |-> 2, msource |-> 1, mdest |-> 3, mentries |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlog |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlogTerm |-> 2, mlogSubterm |-> 1, mreplicationSet |-> {1, 3}, mindex |-> 2] :> 1)
/\ log = <<<<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, <<>>, <<[term |-> 2, subterm |-> 1, value |-> v1]>>>>
/\ witnessSubterm = <<1, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
19: <NextAppendEntriesResponse line 648, col 30 to line 648, col 101 of module extendedraft>
/\ witnessLastLogTerm = 2
/\ currentSubterm = <<1, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 1], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 1, hadNumClientRequests |-> 2, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 3}
/\ replicationSet = <<{1, 3}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 3>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 2>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 1
/\ witnessAcks = {<<2, 1>>, <<2, 2>>}
/\ commitIndex = <<0, 0, 0>>
/\ elections = {[eterm |-> 2, eleader |-> 1, elog |-> <<>>, evotes |-> {1, 3}, evoterLog |-> (1 :> <<>> @@ 3 :> <<>>)]}
/\ state = <<Leader, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = ([mtype |-> AppendEntriesToWitnessRequest, mterm |-> 2, msource |-> 1, mdest |-> 3, mentries |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlog |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlogTerm |-> 2, mlogSubterm |-> 1, mreplicationSet |-> {1, 3}, mindex |-> 2] :> 1)
/\ log = <<<<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, <<>>, <<[term |-> 2, subterm |-> 1, value |-> v1]>>>>
/\ witnessSubterm = <<1, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
20: <MCAdvanceCommitIndex(1) line 74, col 5 to line 75, col 28 of module MCextendedraft>
/\ witnessLastLogTerm = 2
/\ currentSubterm = <<1, 0, 0>>
/\ history = [server |-> <<[restarted |-> 0, timeout |-> 1, replicationSetChanged |-> 1], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0], [restarted |-> 0, timeout |-> 0, replicationSetChanged |-> 0]>>, global |-> <<>>, hadNumLeaders |-> 1, hadNumClientRequests |-> 2, hadReplicationSetChanges |-> 0]
/\ votesResponded = <<{1, 3}, {}, {}>>
/\ witnessReplicationSet = {1, 3}
/\ replicationSet = <<{1, 3}, {1, 2}, {1, 2}>>
/\ nextIndex = <<<<1, 1, 3>>, <<1, 1, 1>>, <<1, 1, 1>>>>
/\ currentTerm = <<2, 1, 2>>
/\ votedFor = <<1, Nil, 1>>
/\ matchIndex = <<<<0, 0, 2>>, <<0, 0, 0>>, <<0, 0, 0>>>>
/\ witnessLastLogSubterm = 1
/\ witnessAcks = {<<2, 1>>, <<2, 2>>}
/\ commitIndex = <<2, 0, 0>>
/\ elections = {[eterm |-> 2, eleader |-> 1, elog |-> <<>>, evotes |-> {1, 3}, evoterLog |-> (1 :> <<>> @@ 3 :> <<>>)]}
/\ state = <<Leader, Follower, Follower>>
/\ voterLog = <<(1 :> <<>> @@ 3 :> <<>>), <<>>, <<>>>>
/\ messages = ([mtype |-> AppendEntriesToWitnessRequest, mterm |-> 2, msource |-> 1, mdest |-> 3, mentries |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlog |-> <<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, mlogTerm |-> 2, mlogSubterm |-> 1, mreplicationSet |-> {1, 3}, mindex |-> 2] :> 1)
/\ log = <<<<[term |-> 2, subterm |-> 1, value |-> v1], [term |-> 2, subterm |-> 1, value |-> v1]>>, <<>>, <<[term |-> 2, subterm |-> 1, value |-> v1]>>>>
/\ witnessSubterm = <<1, 0, 0>>
/\ votesGranted = <<{1, 3}, {}, {}>>
Progress(20) at 2024-06-01 16:30:15: 28,701,606 states generated (18,946 s/min), 9,797,716 distinct states found (6,467 ds/min), 6,824,323 states left on queue.
28701606 states generated, 9797716 distinct states found, 6824323 states left on queue.
The depth of the complete state graph search is 20.
Finished in 90892950ms at (2024-06-01 16:30:15) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.