ccfraft!AdvanceCommitIndex advance to the smalles possible index, whereas raft.h advances to the largest possible one. #5879
Conversation
This file contains 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
lemmy
force-pushed
the
mku-AdvanceCommitIndexOptimization
branch
from
37aea57 to
b27f894
Compare
|
mku-AdvanceCommitIndexOptimization@79936 aka 20240105.19 vs main ewma over 20 builds from 79678 to 79931 Click to see tablemain
mku-AdvanceCommitIndexOptimization
|
|
Confirmed based on commit 2d096a7 to address issue that @achamayou found in #5798. diff --git a/tests/raft_scenarios/replicate b/tests/raft_scenarios/replicate
index 68c601a8b..8d198afe2 100644
--- a/tests/raft_scenarios/replicate
+++ b/tests/raft_scenarios/replicate
@@ -13,6 +13,7 @@ dispatch_all
state_all
replicate,1,helloworld
emit_signature,1
+emit_signature,1
periodic_all,10
dispatch_all
periodic_all,1
diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
index 86d49c39e..fdb58a055 100644
--- a/tla/consensus/Traceccfraft.tla
+++ b/tla/consensus/Traceccfraft.tla
@@ -58,7 +58,7 @@ IsAppendEntriesResponse(msg, dst, src, logline) ==
ASSUME TLCGet("config").mode = "bfs"
JsonFile ==
- IF "JSON" \in DOMAIN IOEnv THEN IOEnv.JSON ELSE "traces/election.ndjson"
+ IF "JSON" \in DOMAIN IOEnv THEN IOEnv.JSON ELSE "../../tests/raft_scenarios/replicate.ndjson"
JsonLog ==
\* Deserialize the System log as a sequence of records from the log file.
diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
index f619448a4..8fd0f8b9d 100644
--- a/tla/consensus/ccfraft.tla
+++ b/tla/consensus/ccfraft.tla
@@ -689,38 +689,47 @@ ChangeConfiguration(i) ==
AdvanceCommitIndex(i) ==
/\ state[i] = Leader
/\ LET
- \* We want to get the smallest such index forward that is a signature
- \* This index must be from the current term,
- \* as explained by Figure 8 and Section 5.4.2 of https://raft.github.io/raft.pdf
- \* See find_highest_possible_committable_index in raft.h
- new_index == SelectInSubSeq(log[i], commitIndex[i]+1, Len(log[i]),
- LAMBDA e : e.contentType = TypeSignature /\ e.term = currentTerm[i])
- new_log ==
- IF new_index > 1 THEN
- [ j \in 1..new_index |-> log[i][j] ]
- ELSE
- << >>
- new_config_index == LastConfigurationToIndex(i, new_index)
- new_configurations == RestrictDomain(configurations[i], LAMBDA c : c >= new_config_index)
+ \* Select those configs that need to have a quorum to agree on this leader.
+ \* Compare https://github.com/microsoft/CCF/blob/75670480c53519fcec1a09d36aefc11b23a597f9/src/consensus/aft/raft.h#L2081
+ HasConsensusWatermark(idx) ==
+ \A config \in {c \in DOMAIN(configurations[i]) : idx >= c } :
+ \* In all of these configs, we now need a quorum in the servers that have the correct matchIndex
+ LET config_servers == configurations[i][config]
+ required_quorum == Quorums[config_servers]
+ agree_servers == {k \in config_servers : matchIndex[i][k] >= idx}
+ IN (IF i \in config_servers THEN {i} ELSE {}) \cup agree_servers \in required_quorum
+ \* The function find_highest_possible_committable_index in raft.h returns the largest committable index
+ \* in the current term (Figure 8 and Section 5.4.2 of https://raft.github.io/raft.pdf explains why it has
+ \* to be the *current* term). Finding the largest index is an (mplementation-level) optimization that
+ \* reduces the number of AdvanceCommitIndex calls, but this optimization also shrinks this spec's state-space.
+ \*
+ \* Theoretically, any committable index in the current term works, i.e., highestCommittableIndex could be
+ \* defined non-deterministically as:
+ \* \E idx \in { j \in (commitIndex[i]+1)..Len(log[i]) : /\ log[i][j].term = currentTerm[i]
+ \* /\ log[i][j].contentType = TypeSignature }
+ \* /\ HasConsensusWatermark(idx)
+ \* /\ ...
+ \*
+ \* Max({0} \cup {...}) to default to 0 if no committable index is found.
+ highestCommittableIndex == Max({0} \cup { j \in (commitIndex[i]+1)..Len(log[i]) :
+ /\ log[i][j].term = currentTerm[i]
+ /\ log[i][j].contentType = TypeSignature
+ /\ HasConsensusWatermark(j) })
IN
- /\ \* Select those configs that need to have a quorum to agree on this leader
- \A config \in {c \in DOMAIN(configurations[i]) : new_index >= c } :
- \* In all of these configs, we now need a quorum in the servers that have the correct matchIndex
- LET config_servers == configurations[i][config]
- required_quorum == Quorums[config_servers]
- agree_servers == {k \in config_servers : matchIndex[i][k] >= new_index}
- IN (IF i \in config_servers THEN {i} ELSE {}) \cup agree_servers \in required_quorum
- \* only advance if necessary (this is basically a sanity check after the Min above)
- /\ commitIndex[i] < new_index
- /\ commitIndex' = [commitIndex EXCEPT ![i] = new_index]
+ \* only advance if necessary (this is basically a sanity)
+ /\ commitIndex[i] < highestCommittableIndex
+ /\ commitIndex' = [commitIndex EXCEPT ![i] = highestCommittableIndex]
/\ committableIndices' = [ committableIndices EXCEPT ![i] = @ \ 0..commitIndex'[i] ]
\* If commit index surpasses the next configuration, pop configs, and retire as leader if removed
/\ IF /\ Cardinality(DOMAIN configurations[i]) > 1
- /\ new_index >= NextConfigurationIndex(i)
+ /\ highestCommittableIndex >= NextConfigurationIndex(i)
THEN
+ LET new_configurations == RestrictDomain(configurations[i],
+ LAMBDA c : c >= LastConfigurationToIndex(i, highestCommittableIndex))
+ IN
/\ configurations' = [configurations EXCEPT ![i] = new_configurations]
\* Retire if i is not in active configuration anymore
- /\ IF i \notin configurations[i][Min(DOMAIN new_configurations)]
+ /\ IF i \notin configurations[i][Min(DOMAIN configurations'[i])]
THEN \E j \in PlausibleSucessorNodes(i) :
/\ state' = [state EXCEPT ![i] = RetiredLeader]
/\ LET msg == [type |-> ProposeVoteRequest, |
|
@achamayou @heidihoward The first three commits in this PR are just syntactic refactorings. You can limit the review to 21f487e if you are in a hurry. |
|
Raft scenario that suggests (confirms ?) that sequenceDiagram
n[n2]->>n[n2]: [KV] initialising in term 2
n[n2]->>n[n2]: replicate 2.1 = [0 bytes] [reconfiguration]
n[n2]->>n[n2]: [ledger] appending: 2.1=[68 bytes] {"data":"eyJuMi
Note over n2: Node n2 created
n[n2]->>n[n2]: replicate 2.2 = [9 bytes] signature [raw]
n[n2]->>n[n2]: [ledger] appending: 2.2=[36 bytes] {"data":"c2lnbm
n[n2]->>n[n2]: [KV] compacting to 2
Note over n[n1]: Node n[n1] created
n[n1]-->n[n2]: connect
n[n2]-->n[n1]: connect
n[n2]->>n[n2]: replicate 2.3 = [0 bytes] [reconfiguration]
n[n2]->>n[n2]: [ledger] appending: 2.3=[96 bytes] {"data":"eyJuMS
n[n1]->>n[n1]: periodic for 30 ms
n[n2]->>n[n2]: periodic for 30 ms
n[n2]->>n[n1]: append_entries (2.2, 2.2] (term 2, commit 2)
n[n1]->>n[n1]: [KV] rolling back to 0.0, in term 2
n[n1]->>n[n1]: [ledger] truncating to 0
n[n2]->>n[n1]: append_entries (2.2, 2.3] (term 2, commit 2)
n[n1]-->>n[n2]: append_entries_response NACK for 2.0
n[n1]-->>n[n2]: append_entries_response NACK for 2.0
n[n2]->>n[n2]: replicate 2.4 = [8 bytes] txAtIdx4 [raw]
n[n2]->>n[n2]: [ledger] appending: 2.4=[36 bytes] {"data":"dHhBdE
n[n2]->>n[n2]: replicate 2.5 = [8 bytes] txAtIdx5 [raw]
n[n2]->>n[n2]: [ledger] appending: 2.5=[36 bytes] {"data":"dHhBdE
n[n2]->>n[n2]: replicate 2.6 = [8 bytes] txAtIdx6 [raw]
n[n2]->>n[n2]: [ledger] appending: 2.6=[36 bytes] {"data":"dHhBdE
n[n2]->>n[n2]: replicate 2.7 = [9 bytes] signature [raw]
n[n2]->>n[n2]: [ledger] appending: 2.7=[36 bytes] {"data":"c2lnbm
n[n1]->>n[n1]: periodic for 30 ms
n[n2]->>n[n2]: periodic for 30 ms
n[n2]->>n[n1]: append_entries (0.0, 2.7] (term 2, commit 2)
n[n1]->>n[n1]: [ledger] appending: 2.1=[68 bytes] {"data":"eyJuMi
n[n1]->>n[n1]: [ledger] appending: 2.2=[36 bytes] {"data":"c2lnbm
n[n1]->>n[n1]: [KV] compacting to 2
n[n1]->>n[n1]: [ledger] appending: 2.3=[96 bytes] {"data":"eyJuMS
n[n1]->>n[n1]: [ledger] appending: 2.4=[36 bytes] {"data":"dHhBdE
n[n1]->>n[n1]: [ledger] appending: 2.5=[36 bytes] {"data":"dHhBdE
n[n1]->>n[n1]: [ledger] appending: 2.6=[36 bytes] {"data":"dHhBdE
n[n1]->>n[n1]: [ledger] appending: 2.7=[36 bytes] {"data":"c2lnbm
n[n1]-->>n[n2]: append_entries_response ACK for 2.7
n[n2]->>n[n2]: [KV] compacting to 7
n[n1]->>n[n1]: periodic for 30 ms
n[n2]->>n[n2]: periodic for 30 ms
n[n2]->>n[n1]: append_entries (2.7, 2.7] (term 2, commit 7)
n[n1]->>n[n1]: [KV] compacting to 7
n[n1]-->>n[n2]: append_entries_response ACK for 2.7
n[n2]->>n[n2]: replicate 2.8 = [0 bytes] [reconfiguration]
n[n2]->>n[n2]: [ledger] appending: 2.8=[68 bytes] {"data":"eyJuMi
n[n1]->>n[n1]: periodic for 30 ms
n[n2]->>n[n2]: periodic for 30 ms
n[n2]->>n[n1]: append_entries (2.7, 2.8] (term 2, commit 7)
n[n1]->>n[n1]: [ledger] appending: 2.8=[68 bytes] {"data":"eyJuMi
n[n1]-->>n[n2]: append_entries_response ACK for 2.8
Note right of n[n1]: leadership F membership R @2.8 (committed 7)
Note right of n[n2]: leadership P membership A @2.8 (committed 7)
n[n2]->>n[n2]: replicate 2.9 = [9 bytes] signature [raw]
n[n2]->>n[n2]: [ledger] appending: 2.9=[36 bytes] {"data":"c2lnbm
n[n2]->>n[n2]: replicate 2.10 = [6 bytes] txAt10 [raw]
n[n2]->>n[n2]: [ledger] appending: 2.10=[32 bytes] {"data":"dHhBdD
n[n2]->>n[n2]: replicate 2.11 = [9 bytes] signature [raw]
n[n2]->>n[n2]: [ledger] appending: 2.11=[36 bytes] {"data":"c2lnbm
n[n1]->>n[n1]: periodic for 30 ms
n[n2]->>n[n2]: periodic for 30 ms
n[n2]->>n[n1]: append_entries (2.8, 2.11] (term 2, commit 7)
n[n1]->>n[n1]: [ledger] appending: 2.9=[36 bytes] {"data":"c2lnbm
n[n1]->>n[n1]: [ledger] appending: 2.10=[32 bytes] {"data":"dHhBdD
n[n1]->>n[n1]: [ledger] appending: 2.11=[36 bytes] {"data":"c2lnbm
n[n1]-->>n[n2]: append_entries_response ACK for 2.11
n[n2]->>n[n2]: [KV] compacting to 11
|
|
Same raft scenario as above, but adapted to legacy bootstrapping (commit 2d096a7 and earlier): ScenarioTraceTemporal properties were violated.
The following behavior constitutes a counter-example:
1: <TraceInit line 106, col 5 to line 113, col 110 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Follower @@ "1" :> Pending)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 0 @@ "1" :> 0)
/\ votedFor = ("0" :> Nil @@ "1" :> Nil)
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "None", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 0, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], configurations |-> <<>>, new_configuration |-> [idx |-> 0, nodes |-> [0 |-> [address |-> ":"], 1 |-> [address |-> ":"]], rid |-> 0], function |-> "add_configuration"], tag |-> "raft_trace", h_ts |-> "3", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "461"]
/\ votesGranted = ("0" :> {} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
2: <RaftDriverQuirks line 386, col 8 to line 390, col 142 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Follower @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 0 @@ "1" :> 0)
/\ votedFor = ("0" :> Nil @@ "1" :> Nil)
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "None", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 0, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], configurations |-> <<>>, new_configuration |-> [idx |-> 0, nodes |-> [0 |-> [address |-> ":"], 1 |-> [address |-> ":"]], rid |-> 0], function |-> "add_configuration"], tag |-> "raft_trace", h_ts |-> "6", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "461"]
/\ votesGranted = ("0" :> {} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
3: <IsTimeout line 159, col 5 to line 162, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Candidate @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 0)
/\ votedFor = ("0" :> "0" @@ "1" :> Nil)
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Candidate", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], configurations |-> <<[idx |-> 0, nodes |-> [0 |-> [address |-> ":"], 1 |-> [address |-> ":"]], rid |-> 0]>>, function |-> "become_candidate"], tag |-> "raft_trace", h_ts |-> "9", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1798"]
/\ votesGranted = ("0" :> {"0"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
4: <IsSendRequestVote line 270, col 5 to line 282, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Candidate @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<[type |-> RequestVoteRequest, dest |-> "1", source |-> "0", term |-> 1, lastCommittableIndex |-> 0, lastCommittableTerm |-> 0]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 0)
/\ votedFor = ("0" :> "0" @@ "1" :> Nil)
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_request_vote", term |-> 1, last_committable_idx |-> 0, term_of_last_committable_idx |-> 0], state |-> [node_id |-> "0", leadership_state |-> "Candidate", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_request_vote", to_node_id |-> "1"], tag |-> "raft_trace", h_ts |-> "12", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1527"]
/\ votesGranted = ("0" :> {"0"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> RequestVoteRequest, dest |-> "1", source |-> "0", term |-> 1, lastCommittableIndex |-> 0, lastCommittableTerm |-> 0]} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
5: <IsRcvRequestVoteRequest line 285, col 5 to line 300, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Candidate @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> RequestVoteResponse, dest |-> "0", source |-> "1", term |-> 1, voteGranted |-> TRUE]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_request_vote", term |-> 1, last_committable_idx |-> 0, term_of_last_committable_idx |-> 0], state |-> [node_id |-> "1", leadership_state |-> "None", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 0, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_request_vote", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "13", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1550"]
/\ votesGranted = ("0" :> {"0"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> RequestVoteResponse, dest |-> "0", source |-> "1", term |-> 1, voteGranted |-> TRUE]} @@ <<"1", "1">> :> {})
6: <IsBecomeFollower line 329, col 5 to line 333, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Candidate @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> RequestVoteResponse, dest |-> "0", source |-> "1", term |-> 1, voteGranted |-> TRUE]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], configurations |-> <<[idx |-> 0, nodes |-> [0 |-> [address |-> ":"], 1 |-> [address |-> ":"]], rid |-> 0]>>, function |-> "become_follower"], tag |-> "raft_trace", h_ts |-> "20", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1907"]
/\ votesGranted = ("0" :> {"0"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> RequestVoteResponse, dest |-> "0", source |-> "1", term |-> 1, voteGranted |-> TRUE]} @@ <<"1", "1">> :> {})
7: <IsRcvRequestVoteResponse line 313, col 5 to line 326, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Candidate @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_request_vote_response", term |-> 1, vote_granted |-> TRUE], state |-> [node_id |-> "0", leadership_state |-> "Candidate", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_request_vote_response", from_node_id |-> "1"], tag |-> "raft_trace", h_ts |-> "22", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1660"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
8: <IsBecomeLeader line 165, col 5 to line 168, col 100 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], configurations |-> <<[idx |-> 0, nodes |-> [0 |-> [address |-> ":"], 1 |-> [address |-> ":"]], rid |-> 0]>>, function |-> "become_leader"], tag |-> "raft_trace", h_ts |-> "27", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1851"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
9: <IsSendAppendEntries line 179, col 5 to line 193, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 0, entries |-> <<>>, prevLogIndex |-> 0]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 0, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 0, prev_term |-> 0, prev_idx |-> 0, contains_new_view |-> FALSE, term_of_idx |-> 0], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_append_entries", to_node_id |-> "1", sent_idx |-> 0, match_idx |-> 0], tag |-> "raft_trace", h_ts |-> "29", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "969"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 0, entries |-> <<>>, prevLogIndex |-> 0]} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
10: <IsRcvAppendEntriesRequest line 196, col 5 to line 206, col 57 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 0]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 0, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 0, prev_term |-> 0, prev_idx |-> 0, contains_new_view |-> FALSE, term_of_idx |-> 0], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "31", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1007"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 0]} @@ <<"1", "1">> :> {})
11: <IsSendAppendEntriesResponse line 211, col 5 to line 213, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 0]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 0], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_append_entries_response", to_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "39", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1370"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 0]} @@ <<"1", "1">> :> {})
12: <IsRcvAppendEntriesResponse line 255, col 5 to line 267, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 0], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries_response", sent_idx |-> 0, match_idx |-> 0, from_node_id |-> "1"], tag |-> "raft_trace", h_ts |-> "40", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1411"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
13: <IsSendAppendEntries line 179, col 5 to line 193, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 0, entries |-> <<>>, prevLogIndex |-> 0]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 0, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 0, prev_term |-> 0, prev_idx |-> 0, contains_new_view |-> FALSE, term_of_idx |-> 0], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_append_entries", to_node_id |-> "1", sent_idx |-> 0, match_idx |-> 0], tag |-> "raft_trace", h_ts |-> "43", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "969"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 0, entries |-> <<>>, prevLogIndex |-> 0]} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
14: <IsRcvAppendEntriesRequest line 196, col 5 to line 206, col 57 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 0]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 0, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 0, prev_term |-> 0, prev_idx |-> 0, contains_new_view |-> FALSE, term_of_idx |-> 0], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "45", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1007"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 0]} @@ <<"1", "1">> :> {})
15: <IsSendAppendEntriesResponse line 211, col 5 to line 213, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 0]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 0], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_append_entries_response", to_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "51", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1370"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 0]} @@ <<"1", "1">> :> {})
16: <IsRcvAppendEntriesResponse line 255, col 5 to line 267, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 0], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries_response", sent_idx |-> 0, match_idx |-> 0, from_node_id |-> "1"], tag |-> "raft_trace", h_ts |-> "52", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1411"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
17: <IsClientRequest line 171, col 5 to line 176, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42]>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "replicate", globally_committable |-> FALSE, seqno |-> 1, view |-> 1], tag |-> "raft_trace", h_ts |-> "56", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "600"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
18: <IsClientRequest line 171, col 5 to line 176, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 1, membership_state |-> "Active", new_view_idx |-> 0], function |-> "replicate", globally_committable |-> FALSE, seqno |-> 2, view |-> 1], tag |-> "raft_trace", h_ts |-> "61", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "600"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
19: <IsClientRequest line 171, col 5 to line 176, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 2, membership_state |-> "Active", new_view_idx |-> 0], function |-> "replicate", globally_committable |-> FALSE, seqno |-> 3, view |-> 1], tag |-> "raft_trace", h_ts |-> "66", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "600"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
20: <IsClientRequest line 171, col 5 to line 176, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 3, membership_state |-> "Active", new_view_idx |-> 0], function |-> "replicate", globally_committable |-> FALSE, seqno |-> 4, view |-> 1], tag |-> "raft_trace", h_ts |-> "71", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "600"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
21: <IsClientRequest line 171, col 5 to line 176, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 4, membership_state |-> "Active", new_view_idx |-> 0], function |-> "replicate", globally_committable |-> FALSE, seqno |-> 5, view |-> 1], tag |-> "raft_trace", h_ts |-> "76", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "600"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
22: <IsClientRequest line 171, col 5 to line 176, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 5, membership_state |-> "Active", new_view_idx |-> 0], function |-> "replicate", globally_committable |-> FALSE, seqno |-> 6, view |-> 1], tag |-> "raft_trace", h_ts |-> "81", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "600"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
23: <IsSignCommittableMessages line 222, col 5 to line 231, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 1) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 6, membership_state |-> "Active", new_view_idx |-> 0], function |-> "replicate", globally_committable |-> TRUE, seqno |-> 7, view |-> 1], tag |-> "raft_trace", h_ts |-> "86", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "600"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
24: <IsSendAppendEntries line 179, col 5 to line 193, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 6) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 0, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>, prevLogIndex |-> 0]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 5, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 0, prev_term |-> 0, prev_idx |-> 0, contains_new_view |-> FALSE, term_of_idx |-> 1], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<7>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_append_entries", to_node_id |-> "1", sent_idx |-> 0, match_idx |-> 0], tag |-> "raft_trace", h_ts |-> "91", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "969"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 0, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>, prevLogIndex |-> 0]} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
25: <IsSendAppendEntries line 179, col 5 to line 193, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 0, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>, prevLogIndex |-> 0], [type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 7, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 0, prev_term |-> 1, prev_idx |-> 5, contains_new_view |-> FALSE, term_of_idx |-> 1], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<7>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_append_entries", to_node_id |-> "1", sent_idx |-> 5, match_idx |-> 0], tag |-> "raft_trace", h_ts |-> "93", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "969"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 0, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>, prevLogIndex |-> 0]} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
26: <IsRcvAppendEntriesRequest line 196, col 5 to line 206, col 57 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 5, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 0, prev_term |-> 0, prev_idx |-> 0, contains_new_view |-> FALSE, term_of_idx |-> 1], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "95", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1007"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]} @@ <<"1", "1">> :> {})
27: <IsExecuteAppendEntries line 305, col 8 to line 310, col 81 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 0, membership_state |-> "Active", new_view_idx |-> 0], function |-> "execute_append_entries_sync", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "98", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1214"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]} @@ <<"1", "1">> :> {})
28: <IsExecuteAppendEntries line 305, col 8 to line 310, col 81 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 1, membership_state |-> "Active", new_view_idx |-> 0], function |-> "execute_append_entries_sync", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "100", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1214"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]} @@ <<"1", "1">> :> {})
29: <IsExecuteAppendEntries line 305, col 8 to line 310, col 81 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 2, membership_state |-> "Active", new_view_idx |-> 0], function |-> "execute_append_entries_sync", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "102", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1214"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]} @@ <<"1", "1">> :> {})
30: <IsExecuteAppendEntries line 305, col 8 to line 310, col 81 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 3, membership_state |-> "Active", new_view_idx |-> 0], function |-> "execute_append_entries_sync", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "104", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1214"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]} @@ <<"1", "1">> :> {})
31: <IsExecuteAppendEntries line 305, col 8 to line 310, col 81 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 4, membership_state |-> "Active", new_view_idx |-> 0], function |-> "execute_append_entries_sync", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "106", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1214"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]} @@ <<"1", "1">> :> {})
32: <IsSendAppendEntriesResponse line 211, col 5 to line 213, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 5], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 5, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_append_entries_response", to_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "111", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1370"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 0, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>, prevLogIndex |-> 5]} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]} @@ <<"1", "1">> :> {})
33: <IsRcvAppendEntriesRequest line 196, col 5 to line 206, col 57 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {7})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5], [type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 7, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 0, prev_term |-> 1, prev_idx |-> 5, contains_new_view |-> FALSE, term_of_idx |-> 1], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 5, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "113", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1007"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]} @@ <<"1", "1">> :> {})
34: <IsExecuteAppendEntries line 305, col 8 to line 310, col 81 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {7})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5], [type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 5, membership_state |-> "Active", new_view_idx |-> 0], function |-> "execute_append_entries_sync", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "116", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1214"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]} @@ <<"1", "1">> :> {})
35: <IsExecuteAppendEntries line 305, col 8 to line 310, col 81 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {7})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5], [type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 6, membership_state |-> "Active", new_view_idx |-> 0], function |-> "execute_append_entries_sync", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "118", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1214"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]} @@ <<"1", "1">> :> {})
36: <IsSendAppendEntriesResponse line 211, col 5 to line 213, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {7})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 0) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5], [type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 7], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<7>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_append_entries_response", to_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "125", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1370"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 5]} @@ <<"1", "1">> :> {})
37: <IsRcvAppendEntriesResponse line 255, col 5 to line 267, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {7})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 5) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 5], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<7>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries_response", sent_idx |-> 7, match_idx |-> 0, from_node_id |-> "1"], tag |-> "raft_trace", h_ts |-> "126", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1411"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]} @@ <<"1", "1">> :> {})
38: <IsRcvAppendEntriesResponse line 255, col 5 to line 267, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 0 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {7} @@ "1" :> {7})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 7], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<7>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries_response", sent_idx |-> 7, match_idx |-> 5, from_node_id |-> "1"], tag |-> "raft_trace", h_ts |-> "128", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1411"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
39: <IsAdvanceCommitIndex line 236, col 8 to line 241, col 85 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {7})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], configurations |-> <<[idx |-> 0, nodes |-> [0 |-> [address |-> ":"], 1 |-> [address |-> ":"]], rid |-> 0]>>, function |-> "commit"], tag |-> "raft_trace", h_ts |-> "134", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "2214"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
40: <IsSendAppendEntries line 179, col 5 to line 193, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 0)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {7})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 7, prevLogTerm |-> 1, entries |-> <<>>, prevLogIndex |-> 7]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 7, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 7, prev_term |-> 1, prev_idx |-> 7, contains_new_view |-> FALSE, term_of_idx |-> 1], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_append_entries", to_node_id |-> "1", sent_idx |-> 7, match_idx |-> 7], tag |-> "raft_trace", h_ts |-> "136", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "969"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 7, prevLogTerm |-> 1, entries |-> <<>>, prevLogIndex |-> 7]} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
41: <IsRcvAppendEntriesRequest line 196, col 5 to line 206, col 57 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 7, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 7, prev_term |-> 1, prev_idx |-> 7, contains_new_view |-> FALSE, term_of_idx |-> 1], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<7>>, commit_idx |-> 0, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "138", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1007"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]} @@ <<"1", "1">> :> {})
42: <IsAdvanceCommitIndex line 242, col 8 to line 244, col 57 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], configurations |-> <<[idx |-> 0, nodes |-> [0 |-> [address |-> ":"], 1 |-> [address |-> ":"]], rid |-> 0]>>, function |-> "commit"], tag |-> "raft_trace", h_ts |-> "144", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "2214"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]} @@ <<"1", "1">> :> {})
43: <IsSendAppendEntriesResponse line 211, col 5 to line 213, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 7], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_append_entries_response", to_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "146", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1370"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 7]} @@ <<"1", "1">> :> {})
44: <IsRcvAppendEntriesResponse line 255, col 5 to line 267, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 7], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries_response", sent_idx |-> 7, match_idx |-> 7, from_node_id |-> "1"], tag |-> "raft_trace", h_ts |-> "147", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1411"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
45: <IsClientRequest line 171, col 5 to line 176, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 0
/\ removedFromConfiguration = {}
/\ configurations = ("0" :> (0 :> {"0", "1"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "replicate", globally_committable |-> FALSE, seqno |-> 8, view |-> 1], tag |-> "raft_trace", h_ts |-> "151", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "600"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
46: <IsChangeConfiguration line 247, col 5 to line 252, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 8) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeReconfiguration, configuration |-> {"0"}]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 1
/\ removedFromConfiguration = {"1"}
/\ configurations = ("0" :> (0 :> {"0", "1"} @@ 9 :> {"0"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], configurations |-> <<[idx |-> 0, nodes |-> [0 |-> [address |-> ":"], 1 |-> [address |-> ":"]], rid |-> 0]>>, new_configuration |-> [idx |-> 8, nodes |-> [0 |-> [address |-> ":"]], rid |-> 8], function |-> "add_configuration"], tag |-> "raft_trace", h_ts |-> "153", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "461"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
47: <IsSendAppendEntries line 179, col 5 to line 193, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 9) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeReconfiguration, configuration |-> {"0"}]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature]>>)
/\ reconfigurationCount = 1
/\ removedFromConfiguration = {"1"}
/\ configurations = ("0" :> (0 :> {"0", "1"} @@ 9 :> {"0"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 7, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42]>>, prevLogIndex |-> 7]>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 8, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 7, prev_term |-> 1, prev_idx |-> 7, contains_new_view |-> FALSE, term_of_idx |-> 1], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 8, membership_state |-> "Active", new_view_idx |-> 0], function |-> "send_append_entries", to_node_id |-> "1", sent_idx |-> 7, match_idx |-> 7], tag |-> "raft_trace", h_ts |-> "157", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "969"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {[type |-> AppendEntriesRequest, dest |-> "1", source |-> "0", term |-> 1, commitIndex |-> 7, prevLogTerm |-> 1, entries |-> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42]>>, prevLogIndex |-> 7]} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
48: <IsRcvAppendEntriesRequest line 196, col 5 to line 206, col 57 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 9) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeReconfiguration, configuration |-> {"0"}]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 1
/\ removedFromConfiguration = {"1"}
/\ configurations = ("0" :> (0 :> {"0", "1"} @@ 9 :> {"0"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 8]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [idx |-> 8, msg |-> "raft_append_entries", term |-> 1, leader_commit_idx |-> 7, prev_term |-> 1, prev_idx |-> 7, contains_new_view |-> FALSE, term_of_idx |-> 1], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "159", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1007"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 8]} @@ <<"1", "1">> :> {})
49: <IsExecuteAppendEntries line 305, col 8 to line 310, col 81 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 9) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeReconfiguration, configuration |-> {"0"}]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 1
/\ removedFromConfiguration = {"1"}
/\ configurations = ("0" :> (0 :> {"0", "1"} @@ 9 :> {"0"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 8]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 7, membership_state |-> "Active", new_view_idx |-> 0], function |-> "execute_append_entries_sync", from_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "162", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1214"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 8]} @@ <<"1", "1">> :> {})
50: <IsAddConfiguration line 216, col 5 to line 219, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 9) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeReconfiguration, configuration |-> {"0"}]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 1
/\ removedFromConfiguration = {"1"}
/\ configurations = ("0" :> (0 :> {"0", "1"} @@ 9 :> {"0"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 8]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 8, membership_state |-> "Active", new_view_idx |-> 0], configurations |-> <<[idx |-> 0, nodes |-> [0 |-> [address |-> ":"], 1 |-> [address |-> ":"]], rid |-> 0]>>, new_configuration |-> [idx |-> 8, nodes |-> [0 |-> [address |-> ":"]], rid |-> 8], function |-> "add_configuration"], tag |-> "raft_trace", h_ts |-> "164", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "461"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 8]} @@ <<"1", "1">> :> {})
51: <IsSendAppendEntriesResponse line 211, col 5 to line 213, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 9) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeReconfiguration, configuration |-> {"0"}]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 1
/\ removedFromConfiguration = {"1"}
/\ configurations = ("0" :> (0 :> {"0", "1"} @@ 9 :> {"0"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 7) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 8]>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 8], state |-> [node_id |-> "1", leadership_state |-> "Follower", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 8, membership_state |-> "Retired", new_view_idx |-> 0], function |-> "send_append_entries_response", to_node_id |-> "0"], tag |-> "raft_trace", h_ts |-> "171", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1370"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {[type |-> AppendEntriesResponse, dest |-> "0", source |-> "1", term |-> 1, success |-> TRUE, lastLogIndex |-> 8]} @@ <<"1", "1">> :> {})
52: <IsRcvAppendEntriesResponse line 255, col 5 to line 267, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 9) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeReconfiguration, configuration |-> {"0"}]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 1
/\ removedFromConfiguration = {"1"}
/\ configurations = ("0" :> (0 :> {"0", "1"} @@ 9 :> {"0"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 8) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [packet |-> [msg |-> "raft_append_entries_response", term |-> 1, success |-> "OK", last_log_idx |-> 8], state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 8, membership_state |-> "Active", new_view_idx |-> 0], function |-> "recv_append_entries_response", sent_idx |-> 8, match_idx |-> 7, from_node_id |-> "1"], tag |-> "raft_trace", h_ts |-> "172", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "1411"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
53: <IsSignCommittableMessages line 222, col 5 to line 231, col 99 of module Traceccfraft>
/\ commitIndex = ("0" :> 7 @@ "1" :> 7)
/\ state = ("0" :> Leader @@ "1" :> Follower)
/\ nextIndex = ("0" :> ("0" :> 1 @@ "1" :> 9) @@ "1" :> ("0" :> 1 @@ "1" :> 1))
/\ log = ("0" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeReconfiguration, configuration |-> {"0"}], [term |-> 1, contentType |-> TypeSignature]>> @@ "1" :> <<[term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeEntry, request |-> 42], [term |-> 1, contentType |-> TypeSignature], [term |-> 1, contentType |-> TypeEntry, request |-> 42]>>)
/\ reconfigurationCount = 1
/\ removedFromConfiguration = {"1"}
/\ configurations = ("0" :> (0 :> {"0", "1"} @@ 9 :> {"0"}) @@ "1" :> (0 :> {"0", "1"}))
/\ commitsNotified = ("0" :> <<0, 0>> @@ "1" :> <<0, 0>>)
/\ committableIndices = ("0" :> {10} @@ "1" :> {})
/\ matchIndex = ("0" :> ("0" :> 0 @@ "1" :> 8) @@ "1" :> ("0" :> 0 @@ "1" :> 0))
/\ messages = ("0" :> <<>> @@ "1" :> <<>>)
/\ currentTerm = ("0" :> 1 @@ "1" :> 1)
/\ votedFor = ("0" :> "0" @@ "1" :> "0")
/\ _logline = [msg |-> [state |-> [node_id |-> "0", leadership_state |-> "Leader", committable_indices |-> <<>>, commit_idx |-> 7, current_view |-> 1, last_idx |-> 8, membership_state |-> "Active", new_view_idx |-> 0], function |-> "replicate", globally_committable |-> TRUE, seqno |-> 9, view |-> 1], tag |-> "raft_trace", h_ts |-> "176", thread_id |-> "100", level |-> "debug", file |-> "../src/consensus/aft/raft.h", number |-> "600"]
/\ votesGranted = ("0" :> {"0", "1"} @@ "1" :> {})
/\ _MessagesTo = (<<"0", "0">> :> {} @@ <<"1", "0">> :> {} @@ <<"0", "1">> :> {} @@ <<"1", "1">> :> {})
This was a red herring caused by invoking The scenario |
|
8f6d14c introduces a {"h_ts": "22", "thread_id": "100", "level": "debug", "tag": "raft_trace", "file": "../src/consensus/aft/raft.h", "number": "2214", "msg": {"configurations": [{"idx": 1, "nodes": {"0": {"address": ":"}}, "rid": 1}], "function": "bootstrap", "state": {"commit_idx": 2, "committable_indices": [], "current_view": 2, "last_idx": 2, "leadership_state": "Leader", "membership_state": "Active", "new_view_idx": 0, "node_id": "0"}}}
{"h_ts": "28", "thread_id": "100", "level": "debug", "tag": "raft_trace", "file": "../src/consensus/aft/raft.h", "number": "461", "msg": {"configurations": [{"idx": 1, "nodes": {"0": {"address": ":"}}, "rid": 1}], "function": "add_configuration", "new_configuration": {"idx": 3, "nodes": {"0": {"address": ":"}, "1": {"address": ":"}}, "rid": 3}, "state": {"commit_idx": 2, "committable_indices": [], "current_view": 2, "last_idx": 2, "leadership_state": "Leader", "membership_state": "Active", "new_view_idx": 0, "node_id": "0"}}}
{"h_ts": "30", "thread_id": "100", "level": "debug", "tag": "raft_trace", "file": "../src/consensus/aft/raft.h", "number": "969", "msg": {"function": "send_append_entries", "match_idx": 0, "packet": {"contains_new_view": false, "idx": 2, "leader_commit_idx": 2, "msg": "raft_append_entries", "prev_idx": 2, "prev_term": 2, "term": 2, "term_of_idx": 2}, "sent_idx": 3, "state": {"commit_idx": 2, "committable_indices": [], "current_view": 2, "last_idx": 2, "leadership_state": "Leader", "membership_state": "Active", "new_view_idx": 0, "node_id": "0"}, "to_node_id": "1"}} |
lemmy
force-pushed
the
mku-AdvanceCommitIndexOptimization
branch
from
68b90ec to
70ee922
Compare
[Refactor]
…reas raft.h advances to the largest possible one. Originally found in #5798.
Execute with:
```shell
.../build $ python3 ../tests/raft_scenarios_runner.py ./raft_driver ../tests/raft_scenarios/5879_deprecated
```
lemmy
force-pushed
the
mku-AdvanceCommitIndexOptimization
branch
from
70ee922 to
333369c
Compare
heidihoward
reviewed
Jan 5, 2024
Co-authored-by: Heidi Howard <[email protected]>
achamayou
reviewed
Jan 5, 2024
achamayou
approved these changes
Jan 5, 2024
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.
Originally found in #5798.