Deadlock after some 20 steps with two, three, four Nodes

[lemmy]

Deadlock with four nodes:

Error: Deadlock reached.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ configurations = (n1 :> (0 :> {n1}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 0
/\ currentTerm = (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1)
/\ votedFor = (n1 :> Nil @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Follower @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 2: <Timeout line 364, col 5 to line 382, col 74 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 0
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Candidate @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 3: <BecomeLeader line 446, col 5 to line 465, col 51 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 0
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 4: <ChangeConfiguration line 516, col 5 to line 536, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}]>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 5: <SignCommittableMessages line 489, col 5 to line 505, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 6: <ClientRequest line 470, col 5 to line 481, col 58 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 7: <SignCommittableMessages line 489, col 5 to line 505, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 8: <ChangeConfiguration line 516, col 5 to line 536, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}]>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 9: <SignCommittableMessages line 489, col 5 to line 505, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 10: <AppendEntries line 412, col 5 to line 442, col 105 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<1>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n3, mprevLogIndex |-> 0, mprevLogTerm |-> 0, mentries |-> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 11: <AppendEntries line 412, col 5 to line 442, col 105 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n3, mprevLogIndex |-> 0, mprevLogTerm |-> 0, mentries |-> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 12: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n3, mprevLogIndex |-> 0, mprevLogTerm |-> 0, mentries |-> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 13: <ClientRequest line 470, col 5 to line 481, col 58 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n3, mprevLogIndex |-> 0, mprevLogTerm |-> 0, mentries |-> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2]>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 14: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n3, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 1]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}]>> @@ n4 :> <<>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 15: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 1 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}]>> @@ n4 :> <<>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 16: <AppendEntries line 412, col 5 to line 442, col 105 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 1>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 1 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n3, mprevLogIndex |-> 1, mprevLogTerm |-> 2, mentries |-> <<[contentType |-> Signature, term |-> 2, value |-> Nil]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}]>> @@ n4 :> <<>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 17: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 1>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 1 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n3, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 2]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n4 :> <<>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 18: <SignCommittableMessages line 489, col 5 to line 505, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 1>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 1 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n3, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 2]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n4 :> <<>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 19: <AppendEntries line 412, col 5 to line 442, col 105 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 1 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n3, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 2], [mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n3, mprevLogIndex |-> 1, mprevLogTerm |-> 2, mentries |-> <<[contentType |-> Signature, term |-> 2, value |-> Nil]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n4 :> <<>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 20: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 1 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n3, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 2]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n4 :> <<>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 21: <ClientRequest line 470, col 5 to line 481, col 58 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 1 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n3, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 2]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 3]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n4 :> <<>>)
/\ clientRequests = 4
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 22: <ClientRequest line 470, col 5 to line 481, col 58 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 1 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n3, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 2]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 3], [contentType |-> Entry, term |-> 2, value |-> 4]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n4 :> <<>>)
/\ clientRequests = 5
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 23: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 3 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 2 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 3], [contentType |-> Entry, term |-> 2, value |-> 4]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n4 :> <<>>)
/\ clientRequests = 5
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 24: <SignCommittableMessages line 489, col 5 to line 505, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 3 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 2 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 3], [contentType |-> Entry, term |-> 2, value |-> 4], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n4 :> <<>>)
/\ clientRequests = 5
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ Enabled_Next = TRUE

State 25: <AdvanceCommitIndex line 550, col 5 to line 589, col 80 of module ccfraft>
/\ configurations = (n1 :> (1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 3 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 2 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 3], [contentType |-> Entry, term |-> 2, value |-> 4], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n4 :> <<>>)
/\ clientRequests = 5
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 2, node |-> n1]
/\ Enabled_Next = TRUE

State 26: <CheckQuorum line 615, col 5 to line 617, col 112 of module ccfraft>
/\ configurations = (n1 :> (1 :> {n3} @@ 5 :> {n2, n4}) @@ n2 :> (0 :> {n1}) @@ n3 :> (0 :> {n1} @@ 1 :> {n3}) @@ n4 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 3 @@ n4 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1) @@ n4 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1))
/\ reconfigurationCount = 2
/\ currentTerm = (n1 :> 2 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil @@ n4 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>> @@ n4 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>) @@ n4 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>> @@ n4 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>> @@ n4 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 2 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0)
/\ state = (n1 :> Follower @@ n2 :> Pending @@ n3 :> Pending @@ n4 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0) @@ n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Reconfiguration, term |-> 2, value |-> {n2, n4}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 3], [contentType |-> Entry, term |-> 2, value |-> 4], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>> @@ n3 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n3}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n4 :> <<>>)
/\ clientRequests = 5
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {} @@ n4 :> {})
/\ committedLog = [index |-> 2, node |-> n1]
/\ Enabled_Next = FALSE

---

s/txt/tla and run with tlc -note -config SIMccfraft_TTrace_1668656587.tla SIMccfraft_TTrace_1668656587.tla.

SIMccfraft_TTrace_1668656587.txt

[lemmy]

Two Nodes:

Error: Deadlock reached.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ configurations = (n1 :> (0 :> {n1}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 0
/\ currentTerm = (n1 :> 1 @@ n2 :> 1)
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Follower @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = (n1 :> <<>> @@ n2 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 2: <Timeout line 364, col 5 to line 382, col 74 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 0
/\ currentTerm = (n1 :> 2 @@ n2 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Candidate @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = (n1 :> <<>> @@ n2 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 3: <BecomeLeader line 446, col 5 to line 465, col 51 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 0
/\ currentTerm = (n1 :> 2 @@ n2 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = (n1 :> <<>> @@ n2 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 4: <ChangeConfiguration line 516, col 5 to line 536, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>> @@ n2 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 5: <AppendEntries line 412, col 5 to line 442, col 105 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n2, mprevLogIndex |-> 0, mprevLogTerm |-> 0, mentries |-> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>> @@ n2 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 6: <SignCommittableMessages line 489, col 5 to line 505, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n2, mprevLogIndex |-> 0, mprevLogTerm |-> 0, mentries |-> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 7: <ClientRequest line 470, col 5 to line 481, col 58 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n2, mprevLogIndex |-> 0, mprevLogTerm |-> 0, mentries |-> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>> @@ n2 :> <<>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 8: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n2, mprevLogIndex |-> 0, mprevLogTerm |-> 0, mentries |-> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>> @@ n2 :> <<>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 9: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n2, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 1]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 10: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 1) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 11: <SignCommittableMessages line 489, col 5 to line 505, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 1) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 12: <AppendEntries line 412, col 5 to line 442, col 105 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 1) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n2, mprevLogIndex |-> 1, mprevLogTerm |-> 2, mentries |-> <<[contentType |-> Signature, term |-> 2, value |-> Nil]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 13: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 1) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n2, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 2]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil]>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 14: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil]>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 15: <AppendEntries line 412, col 5 to line 442, col 105 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n2, mprevLogIndex |-> 2, mprevLogTerm |-> 2, mentries |-> <<[contentType |-> Entry, term |-> 2, value |-> 1]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil]>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]
/\ ENABLED_Next = TRUE

State 16: <AdvanceCommitIndex line 550, col 5 to line 589, col 80 of module ccfraft>
/\ configurations = (n1 :> <<{n2}>> @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n2, mprevLogIndex |-> 2, mprevLogTerm |-> 2, mentries |-> <<[contentType |-> Entry, term |-> 2, value |-> 1]>>, mcommitIndex |-> 0]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil]>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 2, node |-> n1]
/\ ENABLED_Next = TRUE

State 17: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> <<{n2}>> @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n2, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 3]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>>)
/\ clientRequests = 2
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 2, node |-> n1]
/\ ENABLED_Next = TRUE

State 18: <ClientRequest line 470, col 5 to line 481, col 58 of module ccfraft>
/\ configurations = (n1 :> <<{n2}>> @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n2, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 3]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 2, node |-> n1]
/\ ENABLED_Next = TRUE

State 19: <SignCommittableMessages line 489, col 5 to line 505, col 59 of module ccfraft>
/\ configurations = (n1 :> <<{n2}>> @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n2, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 3]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 2, node |-> n1]
/\ ENABLED_Next = TRUE

State 20: <AppendEntries line 412, col 5 to line 442, col 105 of module ccfraft>
/\ configurations = (n1 :> <<{n2}>> @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1, 2>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n2, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 3], [mtype |-> AppendEntriesRequest, mterm |-> 2, msource |-> n1, mdest |-> n2, mprevLogIndex |-> 2, mprevLogTerm |-> 2, mentries |-> <<[contentType |-> Entry, term |-> 2, value |-> 1]>>, mcommitIndex |-> 2]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 2, node |-> n1]
/\ ENABLED_Next = TRUE

State 21: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> <<{n2}>> @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1, 2>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 2)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n2, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 3]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 2, node |-> n1]
/\ ENABLED_Next = TRUE

State 22: <CheckQuorum line 615, col 5 to line 617, col 112 of module ccfraft>
/\ configurations = (n1 :> <<{n2}>> @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1, 2>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 2)
/\ state = (n1 :> Follower @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {[mtype |-> AppendEntriesResponse, mterm |-> 2, msource |-> n2, mdest |-> n1, msuccess |-> TRUE, mmatchIndex |-> 3]}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 2, node |-> n1]
/\ ENABLED_Next = TRUE

State 23: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> <<{n2}>> @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 4) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1, 2>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 3) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 2)
/\ state = (n1 :> Follower @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1]>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 2, node |-> n1]
/\ ENABLED_Next = FALSE

SIMccfraft_TTrace_1668656587.txt

[lemmy]

14 steps (2 nodes) with exhaustive model-checking (no state constraints whatsoever).

@lemmy ➜ /workspaces/CCF/tla (main ✗) $ tlc MCccfraftWithReconfig.tla -config MCccfraft.cfg -workers auto -gzip
TLC2 Version 2.18 of Day Month 20?? (rev: e7c0763)
Running breadth-first search Model-Checking with fp 119 and seed -5203411067492440990 with 8 workers on 8 cores with 3559MB heap and 64MB offheap memory [pid: 6245] (Linux 5.4.0-1094-azure amd64, Microsoft 17.0.5 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspaces/CCF/tla/MCccfraftWithReconfig.tla
Parsing file /workspaces/CCF/tla/ccfraft.tla
Parsing file /tmp/tlc-12541017224359931062/TLC.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.11.1706/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-12541017224359931062/Naturals.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.11.1706/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-12541017224359931062/FiniteSets.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.11.1706/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-12541017224359931062/Sequences.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.11.1706/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-12541017224359931062/FiniteSetsExt.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.11.1706/tools/CommunityModules-deps.jar!/FiniteSetsExt.tla)
Parsing file /tmp/tlc-12541017224359931062/SequencesExt.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.11.1706/tools/CommunityModules-deps.jar!/SequencesExt.tla)
Parsing file /tmp/tlc-12541017224359931062/Functions.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.11.1706/tools/CommunityModules-deps.jar!/Functions.tla)
Parsing file /tmp/tlc-12541017224359931062/Folds.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.11.1706/tools/CommunityModules-deps.jar!/Folds.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module SequencesExt
Semantic processing of module ccfraft
Semantic processing of module MCccfraftWithReconfig
Starting... (2022-11-18 01:31:30)
Computing initial states...
Computed 2 initial states...
Finished computing initial states: 3 distinct states generated at 2022-11-18 01:31:31.
Progress(11) at 2022-11-18 01:31:34: 271,276 states generated (271,276 s/min), 204,198 distinct states found (204,198 ds/min), 149,234 states left on queue.
Progress(14) at 2022-11-18 01:32:34: 12,362,877 states generated (12,091,601 s/min), 9,045,201 distinct states found (8,841,003 ds/min), 6,638,239 states left on queue.
Progress(15) at 2022-11-18 01:33:34: 25,041,449 states generated (12,678,572 s/min), 18,074,786 distinct states found (9,029,585 ds/min), 13,280,698 states left on queue.
Progress(15) at 2022-11-18 01:34:34: 37,667,770 states generated (12,626,321 s/min), 27,018,749 distinct states found (8,943,963 ds/min), 19,843,383 states left on queue.
Progress(15) at 2022-11-18 01:35:34: 50,086,784 states generated (12,419,014 s/min), 35,801,804 distinct states found (8,783,055 ds/min), 26,300,157 states left on queue.
Error: Deadlock reached.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ configurations = (n1 :> (0 :> {n1}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 0
/\ currentTerm = (n1 :> 1 @@ n2 :> 1)
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Follower @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = (n1 :> <<>> @@ n2 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 2: <Timeout line 364, col 5 to line 382, col 74 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 0
/\ currentTerm = (n1 :> 2 @@ n2 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Candidate @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = (n1 :> <<>> @@ n2 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 3: <BecomeLeader line 446, col 5 to line 465, col 51 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 0
/\ currentTerm = (n1 :> 2 @@ n2 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = (n1 :> <<>> @@ n2 :> <<>>)
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 4: <ChangeConfiguration line 516, col 5 to line 536, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = ( n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>> @@
  n2 :> <<>> )
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 5: <SignCommittableMessages line 489, col 5 to line 505, col 59 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = ( n1 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> @@
  n2 :> <<>> )
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 6: <AppendEntries line 412, col 5 to line 442, col 105 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = { [ mtype |-> AppendEntriesRequest,
    mterm |-> 2,
    msource |-> n1,
    mdest |-> n2,
    mprevLogIndex |-> 0,
    mprevLogTerm |-> 0,
    mentries |->
        <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>>,
    mcommitIndex |-> 0 ] }
/\ log = ( n1 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> @@
  n2 :> <<>> )
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 7: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = { [ mtype |-> AppendEntriesRequest,
    mterm |-> 2,
    msource |-> n1,
    mdest |-> n2,
    mprevLogIndex |-> 0,
    mprevLogTerm |-> 0,
    mentries |->
        <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>>,
    mcommitIndex |-> 0 ] }
/\ log = ( n1 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> @@
  n2 :> <<>> )
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 8: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = { [ mtype |-> AppendEntriesResponse,
    mterm |-> 2,
    msource |-> n2,
    mdest |-> n1,
    msuccess |-> TRUE,
    mmatchIndex |-> 1 ] }
/\ log = ( n1 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> @@
  n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>> )
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 9: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 1) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = ( n1 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> @@
  n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>> )
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 10: <AppendEntries line 412, col 5 to line 442, col 105 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 1) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = { [ mtype |-> AppendEntriesRequest,
    mterm |-> 2,
    msource |-> n1,
    mdest |-> n2,
    mprevLogIndex |-> 1,
    mprevLogTerm |-> 2,
    mentries |-> <<[contentType |-> Signature, term |-> 2, value |-> Nil]>>,
    mcommitIndex |-> 0 ] }
/\ log = ( n1 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> @@
  n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}]>> )
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 11: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 1) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = { [ mtype |-> AppendEntriesResponse,
    mterm |-> 2,
    msource |-> n2,
    mdest |-> n1,
    msuccess |-> TRUE,
    mmatchIndex |-> 2 ] }
/\ log = ( n1 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> @@
  n2 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> )
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 12: <Receive line 858, col 5 to line 879, col 53 of module ccfraft>
/\ configurations = (n1 :> (0 :> {n1} @@ 1 :> {n2}) @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 0 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = ( n1 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> @@
  n2 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> )
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 0, node |-> n1]

State 13: <AdvanceCommitIndex line 550, col 5 to line 589, col 80 of module ccfraft>
/\ configurations = (n1 :> <<{n2}>> @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 0)
/\ state = (n1 :> Leader @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = ( n1 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> @@
  n2 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> )
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 2, node |-> n1]

State 14: <CheckQuorum line 615, col 5 to line 617, col 112 of module ccfraft>
/\ configurations = (n1 :> <<{n2}>> @@ n2 :> (0 :> {n1} @@ 1 :> {n2}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<1, 1>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 2) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 0)
/\ state = (n1 :> Follower @@ n2 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ messages = {}
/\ log = ( n1 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> @@
  n2 :>
      << [contentType |-> Reconfiguration, term |-> 2, value |-> {n2}],
         [contentType |-> Signature, term |-> 2, value |-> Nil] >> )
/\ clientRequests = 1
/\ votesGranted = (n1 :> {n1} @@ n2 :> {})
/\ committedLog = [index |-> 2, node |-> n1]

51044174 states generated, 36427785 distinct states found, 26761235 states left on queue.
The depth of the complete state graph search is 15.
Finished in 04min 08s at (2022-11-18 01:35:38)
Trace exploration spec path: ./MCccfraftWithReconfig_TTrace_1668735090.tla

MCccfraft.cfg

SPECIFICATION mc_spec

CONSTANTS
    Servers <- Servers_mc
    \* IsInConfigurations <- MCIsInConfigurations
    \* InTermLimit <- MCInTermLimit
    \* InRequestLimit <- MCInRequestLimit
    \* InRequestVoteLimit <- MCInRequestVoteLimit
    \* InMessagesLimit <- MCInMessagesLimit
    \* InMaxSimultaneousCandidates <- MCInMaxSimultaneousCandidates
    \* InCommitNotificationLimit <- MCInCommitNotificationLimit

    Nil = Nil

    Follower = Follower
    Candidate = Candidate
    Leader = Leader
    RetiredLeader = RetiredLeader
    Pending = Pending

    RequestVoteRequest = RequestVoteRequest
    RequestVoteResponse = RequestVoteResponse
    AppendEntriesRequest = AppendEntriesRequest
    AppendEntriesResponse = AppendEntriesResponse
    NotifyCommitMessage = NotifyCommitMessage

    TypeEntry = Entry
    TypeSignature = Signature
    TypeReconfiguration = Reconfiguration

    NodeOne = n1
    NodeTwo = n2
    NodeThree = n3
    NodeFour = n4
    NodeFive = n5

SYMMETRY Symmetry
VIEW View

CHECK_DEADLOCK 
    TRUE

[lemmy]

3 nodes:

...

State 22: <CheckQuorum line 615, col 5 to line 617, col 112 of module ccfraft>
/\ configurations = (n1 :> <<{n2}>> @@ n2 :> (0 :> {n1} @@ 1 :> {n2}) @@ n3 :> (0 :> {n1}))
/\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2 @@ n3 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1) @@ n3 :> (n1 :> 1 @@ n2 :> 1 @@ n3 :> 1))
/\ reconfigurationCount = 1
/\ currentTerm = (n1 :> 2 @@ n2 :> 2 @@ n3 :> 1)
/\ votedFor = (n1 :> n1 @@ n2 :> Nil @@ n3 :> Nil)
/\ messagesSent = (n1 :> (n1 :> <<>> @@ n2 :> <<4, 1>> @@ n3 :> <<>>) @@ n2 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>) @@ n3 :> (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>))
/\ commitsNotified = (n1 :> <<0, 0>> @@ n2 :> <<0, 0>> @@ n3 :> <<0, 0>>)
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 1 @@ n3 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 0 @@ n3 :> 0)
/\ state = (n1 :> Follower @@ n2 :> Pending @@ n3 :> Pending)
/\ votesRequested = (n1 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0))
/\ messages = {}
/\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil], [contentType |-> Entry, term |-> 2, value |-> 1], [contentType |-> Entry, term |-> 2, value |-> 2], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, value |-> {n2}], [contentType |-> Signature, term |-> 2, value |-> Nil]>> @@ n3 :> <<>>)
/\ clientRequests = 3
/\ votesGranted = (n1 :> {n1} @@ n2 :> {} @@ n3 :> {})
/\ committedLog = [index |-> 2, node |-> n1]
/\ ENABLED_Next = FALSE

SIMccfraft_TTrace_1668745748.txt

[lemmy]

The likely fix for this deadlock is the following change (will provide PR once confirmed):

diff --git a/tla/ccfraft.tla b/tla/ccfraft.tla
index 67bcff5a0..1d2269f08 100644
--- a/tla/ccfraft.tla
+++ b/tla/ccfraft.tla
@@ -363,7 +363,7 @@ Timeout(i) ==
     \* Limit the term of each server to reduce state space
     /\ InTermLimit(i)
     \* Only servers that are not already leaders can become candidates
-    /\ state[i] \in {Follower, Candidate}
+    /\ state[i] # Leader
     \* Limit number of candidates in our relevant server set
     \* (i.e., simulate that not more than a given limit of servers in each configuration times out)
     /\ InMaxSimultaneousCandidates(i)

Enabling Timeout only for followers or candidates looks like an omission stemming back from the original Raft specification that lacks the RetiredLeader and Pending node states:

https://github.com/ongardie/raft.tla/blob/974fff7236545912c035ff8041582864449d0ffe/raft.tla#L176-L178

The implementation likely suffers from the same deadlock, given that can_endorse_primary returns false for Learner (Pending) and RetiredLeaders:

https://github.com/microsoft/CCF/blob/e8adbf946428005372e2144214f08427a7c58e81/src/consensus/aft/raft.h#L964-L974

Would the tests at https://github.com/microsoft/CCF/tree/main/src/consensus/aft/test be a good start to try and reproduce the deadlock at the implementation level? Potentially blocked by https://github.com/microsoft/CCF/issues/4605.

[achamayou]

Pending isn't Learner in 1tx_reconfig raft, it's before participation: the node has passed attestation checks, but is waiting for member confirmation, and just isn't part of any configuration at all, nor has a communication channel with other nodes.

I believe ticking takes care of retired nodes, but I will check once I get to the office. The raft unit tests are a good place to reproduce this deadlock, yes.

[heidihoward]

I think the issue here is in the spec's reconfiguration logic, instead of the Timeout action.

The leader should be in the RetiredLeader state after committing a reconfiguration transaction which removes itself, however, it still seems to be in the Leader state. Because it is a leader, it can step down using CheckQuorum and become a follower. There is now no node which believes it can become a leader, as the old leader no longer believes itself to be a member of current configuration and the new nodes are waiting for the reconfiguration transaction which adds them to be committed.

I think in the implementation, newly added nodes start ticking (and thus can become a leader) once the reconfiguration transaction which added them is signed (commitable). But I need to confirm

[achamayou]

I think in the implementation, newly added nodes start ticking (and thus can become a leader) once the reconfiguration transaction which added them is signed (commitable). But I need to confirm

Yes, it's when newly added node receive the first signature that follows the transaction that makes them part of the configuration (ie. when that transaction becomes committable as far as they can tell):

https://github.com/microsoft/CCF/blob/main/src/consensus/aft/raft.h#L801 https://github.com/microsoft/CCF/blob/main/src/consensus/aft/raft.h#L1379

I am puzzled by

/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 1 @@ n3 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0) @@ n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0))
/\ commitIndex = (n1 :> 2 @@ n2 :> 0 @@ n3 :> 0)

Which seems to imply that n1 believes the commit index is 2, despite none of the nodes thinking any other node has acked 2, let alone a majority. What am I missing?

[heidihoward]

Match index is only used by the leader and is reset to 0 for all nodes when a candidate becomes a leader. The match index is then increased as the leader receives appendEntries responses. The non-zero match indexes of non-leaders like n1 are left over from when these nodes were last a leader.

This example has 3 nodes but its not using all of them. It seems to start with just n0 and then reconfigure to just n1

[lemmy]

Not saying that my proposed change is correct (I wasn't aware that Pending # Leaner), but I exhaustively checked and then simulated it, and none of the properties were violated (except known QuorumLogInv). => Strengthen properties?

Does the Leader immediately transition to RetiredLeader after the reconfiguration transaction or after the re-conf transaction has been signed?

[achamayou]

@lemmy https://microsoft.github.io/CCF/main/architecture/consensus/1tx-reconfig.html#retirement-details (and section above) detail this. A node will stop executing new transactions after having observed the first signature following the transaction that retires it, but will continue to replicate and heartbeat until it observes that transaction being committed (equivalent to the signature that follows it immediately being committed).

[lemmy]

I've started to dig into raft_scenario tests. It looks like as if driver.h/.cpp only exposes a subset of the functions in raft.h. Is this intentional or can we expose more functions if needed? Also, repeated periodic_all,NN dispatch_all statements suggest that the tests are timing sensitive. Is this a major issue? Would be good to know before I try to generate scenarios from TLA+ traces.

By the way, what is the story about the generated tests (raft_scenarios_gen.py) and the hardcoded ones?

[achamayou]

@lemmy we can and should definitely expose more. The driver is limited because it was an early effort (pre-dating signatures, reconfiguration, check quorum etc), and has only received minimal attention since. There are several reasons for this, but one is that testing effort went into end-to-end/acceptance tests that spin up full CCF nodes instead, and are both much more realistic, and cheaper in terms of infrastructure investment (nothing needs to be mocked/simulated). The downside is that they are less robust, can be tougher to debug and are definitely less efficient in terms of coverage per unit of runtime. But with limited resources, this is where we focused our efforts at first.

I don't think of the scenario tests as being timing sensitive, periodic is just a way to advance timers on the nodes, for the purpose of send retries and election timeouts, and dispatch is a way to deliver messages (to control the ordering, and to allow dropping them).

The hardcoded scenarios are things we've found interesting, generally because there were once broken, and needed fixing. They're regression tests. The generated tests are a fairly clumsy attempt at fuzzing, but have not found very many issues historically. I think that's the part we'd hope to scrap and replace with TLA inputs instead.

[lemmy]

Trying to reproduce this deadlock, the scenario below ~appears to deadlock/crash/... something~ segfaults on raft on line https://github.com/microsoft/CCF/blob/main/src/consensus/aft/test/driver.h#L168:

root@codespaces-0aefa5:/workspaces/CCF/build# python3 ../tests/raft_scenarios_runner.py ./raft_driver ../tests/raft_scenarios/4582

## 4582

### steps

nodes,0

periodic_one,0,500
dispatch_all

assert_is_primary,0
state_all

create_new_node,1

periodic_all,500
dispatch_all

assert_is_primary,0
assert_is_primary,1
state_all

replicate_new_configuration,1,1

periodic_all,500
dispatch_all

connect,0,1
connect,1,0

periodic_all,500
dispatch_all

periodic_all,500
dispatch_all

assert_is_primary,0
assert_is_primary,1

replicate,1,helloworld

periodic_all,500
dispatch_all

assert_is_primary,0
assert_is_primary,1

assert_state_sync
state_all

diagram

sequenceDiagram
  n[0]->>n[0]: periodic for 500 ms
  n[0]->>n[0]: [KV] initialising in term 1
  Note right of n[0]: P @1.0 (committed 0)
  Note over n[1]: Node n[1] created
  n[0]->>n[0]: periodic for 500 ms
  n[1]->>n[1]: periodic for 500 ms
  n[1]->>n[1]: [KV] initialising in term 1
  Note right of n[0]: P @1.0 (committed 0)
  Note right of n[1]: P @1.0 (committed 0)
  n[0]->>n[0]: replicate 1.1 = [0 bytes]  [reconfiguration]

??? success 

Is there documentation on debugging scenarios with gdb or some other debugger?

[lemmy]

The Python wrapper raft_scenario_runner.py swallows a segfault:

root@codespaces-0aefa5:/workspaces/CCF/tests/raft_scenarios# gdb ../../build/raft_driver             
GNU gdb (Ubuntu 10.2-0ubuntu1~20.04~1) 10.2
Copyright (C) 2021 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Type "show copying" and "show warranty" for details.
This GDB was configured as "x86_64-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<https://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
    <http://www.gnu.org/software/gdb/documentation/>.

For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from ../../build/raft_driver...
(gdb) r 4582
Starting program: /workspaces/CCF/build/raft_driver 4582
warning: Error disabling address space randomization: Operation not permitted
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".
<RaftDriver>  n[0]->>n[0]: periodic for 500 ms
<RaftDriver>  n[0]->>n[0]: [KV] initialising in term 1
<RaftDriver>  Note right of n[0]: P @1.0 (committed 0)
<RaftDriver>  Note over n[1]: Node n[1] created
<RaftDriver>  n[0]->>n[0]: periodic for 500 ms
<RaftDriver>  n[1]->>n[1]: periodic for 500 ms
<RaftDriver>  n[1]->>n[1]: [KV] initialising in term 1
<RaftDriver>  Note right of n[0]: P @1.0 (committed 0)
<RaftDriver>  Note right of n[1]: P @1.0 (committed 0)
<RaftDriver>  n[0]->>n[0]: replicate 1.1 = [0 bytes]  [reconfiguration]

Program received signal SIGSEGV, Segmentation fault.
0x00000000004349cc in std::__1::__tree_is_left_child<std::__1::__tree_node_base<void*>*> (__x=0x1623041) at /usr/lib/llvm-10/bin/../include/c++/v1/__tree:81
81          return __x == __x->__parent_->__left_;
(gdb) backtrace
#0  0x00000000004349cc in std::__1::__tree_is_left_child<std::__1::__tree_node_base<void*>*> (__x=0x1623041) at /usr/lib/llvm-10/bin/../include/c++/v1/__tree:81
#1  std::__1::__tree_next_iter<std::__1::__tree_end_node<std::__1::__tree_node_base<void*>*>*, std::__1::__tree_node_base<void*>*> (__x=0x1623041) at /usr/lib/llvm-10/bin/../include/c++/v1/__tree:184
#2  std::__1::__tree_iterator<std::__1::__value_type<ccf::EntityId<ccf::NodeIdFormatter>, kv::Configuration::NodeInfo>, std::__1::__tree_node<std::__1::__value_type<ccf::EntityId<ccf::NodeIdFormatter>, kv::Configuration::NodeInfo>, void*>*, long>::operator++ (this=<optimized out>) at /usr/lib/llvm-10/bin/../include/c++/v1/__tree:848
#3  std::__1::__map_iterator<std::__1::__tree_iterator<std::__1::__value_type<ccf::EntityId<ccf::NodeIdFormatter>, kv::Configuration::NodeInfo>, std::__1::__tree_node<std::__1::__value_type<ccf::EntityId<ccf::NodeIdFormatter>, kv::Configuration::NodeInfo>, void*>*, long> >::operator++ (this=<optimized out>) at /usr/lib/llvm-10/bin/../include/c++/v1/map:802
#4  aft::ConfigurationChangeHook::call (this=0x1622b20, consensus=0x16221c8) at ../src/consensus/aft/test/logging_stub.h:299
#5  0x000000000043838c in aft::Aft<LedgerStubProxy_Mermaid>::replicate (this=0x16221c8, entries=..., term=<optimized out>) at ../src/consensus/aft/raft.h:785
#6  0x000000000045b928 in RaftDriver::_replicate (this=0x161fad8, term_s=..., data=..., configuration=...) at ../src/consensus/aft/test/driver.h:168
#7  0x000000000040dc65 in RaftDriver::replicate_new_configuration (this=0x161fad8, term_s=..., node_ids=...) at ../src/consensus/aft/test/driver.h:246
#8  0x0000000000407508 in main (argc=<optimized out>, argv=<optimized out>) at ../src/consensus/aft/test/driver.cpp:166

https://github.com/microsoft/CCF/commit/5c9a103e78 introduced the lines that segfault in logging_stub.h. None of the existing scenarios exercise those lines.

[lemmy]

I think the issue here is in the spec's reconfiguration logic, instead of the Timeout action.

The leader should be in the RetiredLeader state after committing a reconfiguration transaction which removes itself, however, it still seems to be in the Leader state. Because it is a leader, it can step down using CheckQuorum and become a follower. There is now no node which believes it can become a leader, as the old leader no longer believes itself to be a member of current configuration and the new nodes are waiting for the reconfiguration transaction which adds them to be committed.

I think in the implementation, newly added nodes start ticking (and thus can become a leader) once the reconfiguration transaction which added them is signed (commitable). But I need to confirm

The scenario 4582.2 and its trace below confirm that the old leader retires upon the configuration change. What warrants further investigation is that the new node only briefly becomes leader but then steps down again (Stepping down as leader n[1]: No ack received from a majority of backups in last 100ms).

2022-12-05T16:29:24.205465Z        100 [debug] ../src/consensus/aft/raft.h:217      | reconfiguration type: 1tx
2022-12-05T16:29:24.205527Z        100 [info ] ../src/consensus/aft/raft.h:588      | Election timer has become active
2022-12-05T16:29:24.205546Z        100 [debug] ../src/consensus/aft/raft.h:471      | Configurations: add new configuration at 0: {{n[0]}}
<RaftDriver>  n[0]->>n[0]: periodic for 500 ms
2022-12-05T16:29:24.205582Z        100 [debug] ../src/consensus/aft/raft.h:2068     | Node n[0] voted for n[0] in configuration 0 with quorum 1
2022-12-05T16:29:24.205591Z        100 [debug] ../src/consensus/aft/raft.h:1893     | Election index is 0 in term 1
<RaftDriver>  n[0]->>n[0]: [KV] initialising in term 1
2022-12-05T16:29:24.205603Z        100 [info ] ../src/consensus/aft/raft.h:1917     | Becoming leader n[0]: 1
2022-12-05T16:29:24.205608Z        100 [debug] ../src/consensus/aft/raft.h:2256     | Starting commit
2022-12-05T16:29:24.205616Z        100 [info ] ../src/consensus/aft/raft.h:1862     | Becoming candidate n[0]: 1
<RaftDriver>  Note right of n[0]: ? @1.0 (committed 0)
<RaftDriver>  n[0]->>n[0]: replicate 1.1 = [10 bytes] HelloTerm1 [raw]
2022-12-05T16:29:24.206654Z        100 [debug] ../src/consensus/aft/raft.h:757      | Replicating 1 entries
2022-12-05T16:29:24.206667Z        100 [debug] ../src/consensus/aft/raft.h:776      | Replicated on leader n[0]: 1 committable (0 hooks)
2022-12-05T16:29:24.206675Z        100 [debug] ../src/consensus/aft/raft.h:790      | membership: 1 leadership: 0
<RaftDriver>  n[0]->>n[0]: [ledger] appending: 1.1=[40 bytes] {"data":"SGVsbG
2022-12-05T16:29:24.206692Z        100 [debug] ../src/consensus/aft/impl/state.h:38 | Updating view to: 1 at version: 1
2022-12-05T16:29:24.206702Z        100 [debug] ../src/consensus/aft/impl/state.h:55 | Resulting views: 1
2022-12-05T16:29:24.206708Z        100 [debug] ../src/consensus/aft/raft.h:2131     | In update_commit, new_commit_cft_idx: 1, last_idx: 1
2022-12-05T16:29:24.206716Z        100 [debug] ../src/consensus/aft/raft.h:2153     | Commit if possible 1 (ci: 0) (ti 1)
2022-12-05T16:29:24.206721Z        100 [debug] ../src/consensus/aft/raft.h:2256     | Starting commit
2022-12-05T16:29:24.206725Z        100 [debug] ../src/consensus/aft/raft.h:2272     | Compacting...
<RaftDriver>  n[0]->>n[0]: [KV] compacting to 1
2022-12-05T16:29:24.206735Z        100 [debug] ../src/consensus/aft/raft.h:2276     | Commit on n[0]: 1
<RaftDriver>  n[0]->>n[0]: periodic for 500 ms
2022-12-05T16:29:24.206760Z        100 [debug] ../src/consensus/aft/raft.h:217      | reconfiguration type: 1tx
2022-12-05T16:29:24.206768Z        100 [info ] ../src/consensus/aft/raft.h:588      | Election timer has become active
<RaftDriver>  Note over n[1]: Node n[1] created
<RaftDriver>  n[0]->>n[0]: periodic for 500 ms
<RaftDriver>  n[1]->>n[1]: periodic for 500 ms
2022-12-05T16:29:24.206788Z        100 [debug] ../src/consensus/aft/raft.h:1893     | Election index is 0 in term 1
<RaftDriver>  n[1]->>n[1]: [KV] initialising in term 1
2022-12-05T16:29:24.206799Z        100 [info ] ../src/consensus/aft/raft.h:1917     | Becoming leader n[1]: 1
2022-12-05T16:29:24.206803Z        100 [debug] ../src/consensus/aft/raft.h:2256     | Starting commit
2022-12-05T16:29:24.206807Z        100 [info ] ../src/consensus/aft/raft.h:1862     | Becoming candidate n[1]: 1
<RaftDriver>  Note right of n[0]: ? @1.1 (committed 1)
<RaftDriver>  Note right of n[1]: ? @1.0 (committed 0)
<RaftDriver>  n[0]->>n[0]: replicate 1.2 = [0 bytes]  [reconfiguration]
2022-12-05T16:29:24.206856Z        100 [debug] ../src/consensus/aft/raft.h:757      | Replicating 1 entries
2022-12-05T16:29:24.206864Z        100 [debug] ../src/consensus/aft/raft.h:776      | Replicated on leader n[0]: 2 committable (1 hooks)
2022-12-05T16:29:24.206870Z        100 [debug] ../src/consensus/aft/raft.h:471      | Configurations: add new configuration at 2: {{n[1]}}
2022-12-05T16:29:24.206879Z        100 [info ] ../src/consensus/aft/raft.h:2012     | Becoming retired, phase 1 (leadership 0): n[0]: 1 at 2
2022-12-05T16:29:24.206883Z        100 [info ] ../src/consensus/aft/raft.h:2032     | Node retiring at 2
2022-12-05T16:29:24.206890Z        100 [trace] ../src/consensus/aft/raft.h:1056     | Sending append entries to node n[1] in batches of 9, covering the range 2 -> 1
2022-12-05T16:29:24.206897Z        100 [trace] ../src/consensus/aft/raft.h:1086     | Sending sub range 2 -> 1
2022-12-05T16:29:24.206903Z        100 [debug] ../src/consensus/aft/raft.h:1110     | Send append entries from n[0] to n[1]: (1.1, 1.1] (1)
2022-12-05T16:29:24.206913Z        100 [info ] ../src/consensus/aft/raft.h:2618     | Added raft node n[1] (:)
2022-12-05T16:29:24.206922Z        100 [debug] ../src/consensus/aft/raft.h:790      | membership: 3 leadership: 0
2022-12-05T16:29:24.206930Z        100 [info ] ../src/consensus/aft/raft.h:2012     | Becoming retired, phase 2 (leadership 0): n[0]: 1 at 2
2022-12-05T16:29:24.206935Z        100 [info ] ../src/consensus/aft/raft.h:2043     | Node retirement committable at 2
<RaftDriver>  n[0]->>n[0]: [ledger] appending: 1.2=[64 bytes] {"data":"eyIxIj
2022-12-05T16:29:24.206946Z        100 [debug] ../src/consensus/aft/impl/state.h:38 | Updating view to: 1 at version: 2
2022-12-05T16:29:24.206954Z        100 [debug] ../src/consensus/aft/impl/state.h:55 | Resulting views: 1
<RaftDriver>  n[0]->>n[0]: periodic for 500 ms
2022-12-05T16:29:24.206968Z        100 [trace] ../src/consensus/aft/raft.h:1056     | Sending append entries to node n[1] in batches of 13, covering the range 2 -> 2
2022-12-05T16:29:24.206973Z        100 [trace] ../src/consensus/aft/raft.h:1086     | Sending sub range 2 -> 2
2022-12-05T16:29:24.206981Z        100 [debug] ../src/consensus/aft/raft.h:1110     | Send append entries from n[0] to n[1]: (1.1, 1.2] (1)
<RaftDriver>  n[1]->>n[1]: periodic for 500 ms
2022-12-05T16:29:24.206990Z        100 [info ] ../src/consensus/aft/raft.h:957      | Stepping down as leader n[1]: No ack received from a majority of backups in last 100ms
<RaftDriver>  n[1]->>n[1]: [KV] rolling back to 0.0, in term 1
2022-12-05T16:29:24.207001Z        100 [debug] ../src/consensus/aft/raft.h:2466     | Setting term in store to: 1
<RaftDriver>  n[1]->>n[1]: [ledger] truncating to 0
2022-12-05T16:29:24.207009Z        100 [debug] ../src/consensus/aft/raft.h:2469     | Rolled back at 0
2022-12-05T16:29:24.207016Z        100 [debug] ./src/consensus/aft/impl/state.h:127 | Resulting views from rollback: 
2022-12-05T16:29:24.207023Z        100 [info ] ../src/consensus/aft/raft.h:1969     | Becoming follower n[1]: 1.0
<RaftDriver>  n[0]-->n[1]: connect
<RaftDriver>  n[0]->>n[0]: periodic for 1000 ms
2022-12-05T16:29:24.207060Z        100 [trace] ../src/consensus/aft/raft.h:1056     | Sending append entries to node n[1] in batches of 17, covering the range 3 -> 2
2022-12-05T16:29:24.207067Z        100 [trace] ../src/consensus/aft/raft.h:1086     | Sending sub range 3 -> 2
2022-12-05T16:29:24.207072Z        100 [debug] ../src/consensus/aft/raft.h:1110     | Send append entries from n[0] to n[1]: (1.2, 1.2] (1)
<RaftDriver>  n[1]->>n[1]: periodic for 1000 ms
2022-12-05T16:29:24.207080Z        100 [debug] ../src/consensus/aft/raft.h:1893     | Election index is 0 in term 2
<RaftDriver>  n[1]->>n[1]: [KV] initialising in term 2
2022-12-05T16:29:24.207091Z        100 [info ] ../src/consensus/aft/raft.h:1917     | Becoming leader n[1]: 2
2022-12-05T16:29:24.207097Z        100 [debug] ../src/consensus/aft/raft.h:2256     | Starting commit
2022-12-05T16:29:24.207102Z        100 [info ] ../src/consensus/aft/raft.h:1862     | Becoming candidate n[1]: 2
<RaftDriver>  n[0]->>n[1]: append_entries (1.2, 1.2] (term 1, commit 1)
2022-12-05T16:29:24.207116Z        100 [debug] ../src/consensus/aft/raft.h:1151     | Received append entries: 1.2 to 1.2 (from n[0] in term 1)
2022-12-05T16:29:24.207126Z        100 [info ] ../src/consensus/aft/raft.h:1179     | Recv append entries to n[1] from n[0] but our term is later (2 > 1)
2022-12-05T16:29:24.207135Z        100 [debug] ../src/consensus/aft/raft.h:1508     | Send append entries response from n[1] to n[0] for index 0: 1
<RaftDriver>  n[1]-->>n[0]: append_entries_response NACK for 2.0
2022-12-05T16:29:24.207151Z        100 [debug] ../src/consensus/aft/raft.h:1554     | Recv append entries response to n[0] from n[1]: more recent term (2 > 1)
2022-12-05T16:29:24.207158Z        100 [debug] ../src/consensus/aft/raft.h:1982     | Becoming aware of new term 2
<RaftDriver>  n[0]->>n[0]: [KV] rolling back to 1.2, in term 2
2022-12-05T16:29:24.207169Z        100 [debug] ../src/consensus/aft/raft.h:2466     | Setting term in store to: 2
<RaftDriver>  n[0]->>n[0]: [ledger] truncating to 2
2022-12-05T16:29:24.207184Z        100 [debug] ../src/consensus/aft/raft.h:2469     | Rolled back at 2
2022-12-05T16:29:24.207192Z        100 [debug] ./src/consensus/aft/impl/state.h:127 | Resulting views from rollback: 1
<RaftDriver>  n[0]->>n[0]: periodic for 1000 ms
2022-12-05T16:29:24.207216Z        100 [trace] ../src/consensus/aft/raft.h:1056     | Sending append entries to node n[1] in batches of 21, covering the range 3 -> 2
2022-12-05T16:29:24.207226Z        100 [trace] ../src/consensus/aft/raft.h:1086     | Sending sub range 3 -> 2
2022-12-05T16:29:24.207234Z        100 [debug] ../src/consensus/aft/raft.h:1110     | Send append entries from n[0] to n[1]: (1.2, 1.2] (1)
<RaftDriver>  n[1]->>n[1]: periodic for 1000 ms
2022-12-05T16:29:24.207275Z        100 [info ] ../src/consensus/aft/raft.h:957      | Stepping down as leader n[1]: No ack received from a majority of backups in last 100ms
<RaftDriver>  n[1]->>n[1]: [KV] rolling back to 0.0, in term 2
2022-12-05T16:29:24.207290Z        100 [debug] ../src/consensus/aft/raft.h:2466     | Setting term in store to: 2
<RaftDriver>  n[1]->>n[1]: [ledger] truncating to 0
2022-12-05T16:29:24.207304Z        100 [debug] ../src/consensus/aft/raft.h:2469     | Rolled back at 0
2022-12-05T16:29:24.207317Z        100 [debug] ./src/consensus/aft/impl/state.h:127 | Resulting views from rollback: 
2022-12-05T16:29:24.207328Z        100 [info ] ../src/consensus/aft/raft.h:1969     | Becoming follower n[1]: 2.0
<RaftDriver>  n[0]->>n[1]: append_entries (1.2, 1.2] (term 2, commit 1)
2022-12-05T16:29:24.207353Z        100 [debug] ../src/consensus/aft/raft.h:1151     | Received append entries: 1.2 to 1.2 (from n[0] in term 2)
2022-12-05T16:29:24.207361Z        100 [debug] ../src/consensus/aft/raft.h:1193     | Previous term for 2 should be 0
2022-12-05T16:29:24.207366Z        100 [debug] ../src/consensus/aft/raft.h:1200     | Recv append entries to n[1] from n[0] but our log does not yet contain index 2
2022-12-05T16:29:24.207374Z        100 [debug] ../src/consensus/aft/raft.h:1508     | Send append entries response from n[1] to n[0] for index 0: 1
<RaftDriver>  n[1]-->>n[0]: append_entries_response NACK for 2.0
2022-12-05T16:29:24.207384Z        100 [trace] ../src/consensus/aft/raft.h:1001     | Looking for match with 2.0, from 1.2, best answer is 0
2022-12-05T16:29:24.207392Z        100 [debug] ../src/consensus/aft/raft.h:1622     | Recv append entries response to n[0] from n[1]: failed
<RaftDriver>  Note right of n[0]: R @2.2 (committed 1)
<RaftDriver>  Note right of n[1]: F @2.0 (committed 0)

Below is a simplified scenario:

## Create a single node and have it become leader/primary.
nodes,0

periodic_one,0,500
dispatch_all

assert_is_primary,0
state_all

periodic_all,500
dispatch_all

## create_new_node should create a node in pending state,
## i.e., no connection with other nodes and not part of
## any configuration.
create_new_node,1

connect,0,1

periodic_all,1000
dispatch_all

periodic_all,1000
dispatch_all
state_all

## Without connecting node 0 and 1, change the configuration
## in term 1 to node 1.
replicate_new_configuration,1,1

periodic_all,500
dispatch_all

## Node 0 is a retired leader and node 1 *briefly* becomes a leader/primary.
state_all
assert_is_retired,0
assert_is_primary,0
assert_is_primary,1

periodic_all,1000
dispatch_all

## After a while, 1 degrades to a follower/backup.
state_all
assert_is_retired,0
assert_is_backup,1

## assert_state_sync fails because node 1 never synced up with n0.
# assert_state_sync

[achamayou]

What warrants further investigation is that the new node only briefly becomes leader but then steps down again (Stepping down as leader n[1]: No ack received from a majority of backups in last 100ms).

I'll take a look tomorrow, but that sounds like CheckQuorum telling the primary to stand down because it hasn't seen any acks in a while.

connect,0,1 ... Without connecting node 0 and 1, change the configuration

Is connect directional?

[lemmy]

What warrants further investigation is that the new node only briefly becomes leader but then steps down again (Stepping down as leader n[1]: No ack received from a majority of backups in last 100ms).

I'll take a look tomorrow, but that sounds like CheckQuorum telling the primary to stand down because it hasn't seen any acks in a while.

Does a primary expect to receive ACKs in a single-node configuration?

connect,0,1 ... Without connecting node 0 and 1, change the configuration

Is connect directional?

No: https://github.com/microsoft/CCF/blob/1a116b75998bbdfb4072d1c65af338551ccae747/src/consensus/aft/test/driver.h#L388-L394

[achamayou]

Does a primary expect to receive ACKs in a single-node configuration?

No, but it strangely does in a zero-node configuration, because: https://github.com/microsoft/CCF/blob/main/src/consensus/aft/raft.h#L920

Given enough periodic + dispatch after the reconnect, n1 seems to able to catch up and move past that.

It still eventually steps down, not for quorum reasons, and I cannot quite figure out why right now.

[lemmy]

At the implementation level, there appears to be a liveness issue s.t. node #1 alternates between being a primary and a follower (note the repeated dispatch/periodic steps at the end):

4582.2

steps

## Create a single node, have it become leader/primary, and receive
## a write with value HelloTerm1.
nodes,0

periodic_one,0,500
dispatch_all

assert_is_primary,0
state_all

replicate,1,HelloTerm1

periodic_all,500
dispatch_all

## create_new_node should create a node in pending state,
## i.e., no connection with other nodes and not part of
## any configuration.
create_new_node,1

periodic_all,500
dispatch_all

## Both are primary at this point because the nodes 
## have not connected, and, thus, do not know each other.
assert_is_primary,0
assert_is_primary,1
## Node 0 has committed the write with HelloTerm1. Node
## 1 has *not* seen the write. 
assert_commit_idx,0,1
assert_commit_idx,1,0
state_all

## Without connecting node 0 and 1, change the configuration
## in term 1 to node 1.
replicate_new_configuration,1,1

periodic_all,500
dispatch_all

## Node 0 is a retired leader.
assert_is_retired,0
assert_is_primary,0
assert_commit_idx,0,1

## Node 1 is a follower/backup.
assert_is_backup,1
assert_commit_idx,1,0

connect,0,1

periodic_all,1000
dispatch_all

## Node 0 remains a retired leader.
assert_is_retired,0
assert_is_primary,0
assert_commit_idx,0,1

## Node 1 *briefly* becomes a leader/primary.
assert_is_primary,1
assert_commit_idx,1,0

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

periodic_all,1000
dispatch_all
state_all

diagram

sequenceDiagram
  n[0]->>n[0]: periodic for 500 ms
  n[0]->>n[0]: [KV] initialising in term 1
  Note right of n[0]: P @1.0 (committed 0)
  n[0]->>n[0]: replicate 1.1 = [10 bytes] HelloTerm1 [raw]
  n[0]->>n[0]: [ledger] appending: 1.1=[40 bytes] {"data":"SGVsbG
  n[0]->>n[0]: [KV] compacting to 1
  n[0]->>n[0]: periodic for 500 ms
  Note over n[1]: Node n[1] created
  n[0]->>n[0]: periodic for 500 ms
  n[1]->>n[1]: periodic for 500 ms
  n[1]->>n[1]: [KV] initialising in term 1
  Note right of n[0]: P @1.1 (committed 1)
  Note right of n[1]: P @1.0 (committed 0)
  n[0]->>n[0]: replicate 1.2 = [0 bytes]  [reconfiguration]
  n[0]->>n[0]: [ledger] appending: 1.2=[64 bytes] {"data":"eyIxIj
  n[0]->>n[0]: periodic for 500 ms
  n[1]->>n[1]: periodic for 500 ms
  n[1]->>n[1]: [KV] rolling back to 0.0, in term 1
  n[1]->>n[1]: [ledger] truncating to 0
  n[0]-->n[1]: connect
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] initialising in term 2
  n[0]->>n[1]: append_entries (1.2, 1.2] (term 1, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 2.0
  n[0]->>n[0]: [KV] rolling back to 1.2, in term 2
  n[0]->>n[0]: [ledger] truncating to 2
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] rolling back to 0.0, in term 2
  n[1]->>n[1]: [ledger] truncating to 0
  n[0]->>n[1]: append_entries (1.2, 1.2] (term 2, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 2.0
  Note right of n[0]: R @2.2 (committed 1)
  Note right of n[1]: F @2.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] initialising in term 3
  n[0]->>n[1]: append_entries (0.0, 1.2] (term 2, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 3.0
  n[0]->>n[0]: [KV] rolling back to 1.2, in term 3
  n[0]->>n[0]: [ledger] truncating to 2
  Note right of n[0]: R @3.2 (committed 1)
  Note right of n[1]: P @3.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] rolling back to 0.0, in term 3
  n[1]->>n[1]: [ledger] truncating to 0
  n[0]->>n[1]: append_entries (1.2, 1.2] (term 3, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 3.0
  Note right of n[0]: R @3.2 (committed 1)
  Note right of n[1]: F @3.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] initialising in term 4
  n[0]->>n[1]: append_entries (0.0, 1.2] (term 3, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 4.0
  n[0]->>n[0]: [KV] rolling back to 1.2, in term 4
  n[0]->>n[0]: [ledger] truncating to 2
  Note right of n[0]: R @4.2 (committed 1)
  Note right of n[1]: P @4.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] rolling back to 0.0, in term 4
  n[1]->>n[1]: [ledger] truncating to 0
  n[0]->>n[1]: append_entries (1.2, 1.2] (term 4, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 4.0
  Note right of n[0]: R @4.2 (committed 1)
  Note right of n[1]: F @4.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] initialising in term 5
  n[0]->>n[1]: append_entries (0.0, 1.2] (term 4, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 5.0
  n[0]->>n[0]: [KV] rolling back to 1.2, in term 5
  n[0]->>n[0]: [ledger] truncating to 2
  Note right of n[0]: R @5.2 (committed 1)
  Note right of n[1]: P @5.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] rolling back to 0.0, in term 5
  n[1]->>n[1]: [ledger] truncating to 0
  n[0]->>n[1]: append_entries (1.2, 1.2] (term 5, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 5.0
  Note right of n[0]: R @5.2 (committed 1)
  Note right of n[1]: F @5.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] initialising in term 6
  n[0]->>n[1]: append_entries (0.0, 1.2] (term 5, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 6.0
  n[0]->>n[0]: [KV] rolling back to 1.2, in term 6
  n[0]->>n[0]: [ledger] truncating to 2
  Note right of n[0]: R @6.2 (committed 1)
  Note right of n[1]: P @6.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] rolling back to 0.0, in term 6
  n[1]->>n[1]: [ledger] truncating to 0
  n[0]->>n[1]: append_entries (1.2, 1.2] (term 6, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 6.0
  Note right of n[0]: R @6.2 (committed 1)
  Note right of n[1]: F @6.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] initialising in term 7
  n[0]->>n[1]: append_entries (0.0, 1.2] (term 6, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 7.0
  n[0]->>n[0]: [KV] rolling back to 1.2, in term 7
  n[0]->>n[0]: [ledger] truncating to 2
  Note right of n[0]: R @7.2 (committed 1)
  Note right of n[1]: P @7.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] rolling back to 0.0, in term 7
  n[1]->>n[1]: [ledger] truncating to 0
  n[0]->>n[1]: append_entries (1.2, 1.2] (term 7, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 7.0
  Note right of n[0]: R @7.2 (committed 1)
  Note right of n[1]: F @7.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] initialising in term 8
  n[0]->>n[1]: append_entries (0.0, 1.2] (term 7, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 8.0
  n[0]->>n[0]: [KV] rolling back to 1.2, in term 8
  n[0]->>n[0]: [ledger] truncating to 2
  Note right of n[0]: R @8.2 (committed 1)
  Note right of n[1]: P @8.0 (committed 0)
  n[0]->>n[0]: periodic for 1000 ms
  n[1]->>n[1]: periodic for 1000 ms
  n[1]->>n[1]: [KV] rolling back to 0.0, in term 8
  n[1]->>n[1]: [ledger] truncating to 0
  n[0]->>n[1]: append_entries (1.2, 1.2] (term 8, commit 1)
  n[1]-->>n[0]: append_entries_response NACK for 8.0
  Note right of n[0]: R @8.2 (committed 1)
  Note right of n[1]: F @8.0 (committed 0)

??? success

[achamayou]

@lemmy with a periodic 1000, and an election timeout of 100 (https://github.com/microsoft/CCF/blob/main/src/consensus/aft/test/driver.h#L175), the leader is expected to step down (CheckQuorum). A single dispatch all round after that will probably also result in half an election cycle.

periodic just makes time tick in the enclave, but does not deliver any messages between the nodes.

[lemmy]

Related: https://github.com/microsoft/CCF/issues/4806

[lemmy]

@achamayou @heidihoward A spec bug causes the deadlock; the disjuncts allow for behaviors where a leader fails to retire when the leader is expected to retire. The two "Otherwise" strongly suggest that the original author meant to use if-then-else. I checked the changes for the three configs MCccfraft, MCccfraftWithReconfg, and SIMccfraft (with one to five nodes).

Out of curiosity, how will this scenario be handled under a byzantine fault model, i.e., a leader that refuses to retire?

[lemmy]

Independently of the deadlock above, the TLA+ spec misses to model the transition described in raft.h; the TLA+ action AdvanceCommitIndex is only enabled for the leader, but raft::add_configuration allows a follower to retire.

nodes,0,1,2
connect,0,1
connect,0,2
connect,2,1

periodic_one,0,110
dispatch_all

assert_is_primary,0
assert_is_backup,1
assert_is_backup,2

state_all

replicate_new_configuration,1,0,1 # New configuration: [0, 1] in term 1, 2 is expected to retire.

periodic_all,10
dispatch_all

assert_is_primary,0
assert_is_backup,1
assert_is_retired,2

state_all

sequenceDiagram
  n[0]-->n[1]: connect
  n[0]-->n[2]: connect
  n[2]-->n[1]: connect
  n[0]->>n[0]: periodic for 110 ms
  n[0]->>n[2]: request_vote for term 1, at tx 0.0
  n[2]->>n[2]: [KV] rolling back to 0.0, in term 1
  n[2]->>n[2]: [ledger] truncating to 0
  n[0]->>n[1]: request_vote for term 1, at tx 0.0
  n[1]->>n[1]: [KV] rolling back to 0.0, in term 1
  n[1]->>n[1]: [ledger] truncating to 0
  n[1]-->>n[0]: request_vote_response for term 1 = Y
  n[0]->>n[0]: [KV] initialising in term 1
  n[2]-->>n[0]: request_vote_response for term 1 = Y
  n[0]->>n[2]: append_entries (0.0, 0.0] (term 1, commit 0)
  n[0]->>n[1]: append_entries (0.0, 0.0] (term 1, commit 0)
  n[1]-->>n[0]: append_entries_response ACK for 1.0
  n[2]-->>n[0]: append_entries_response ACK for 1.0
  Note right of n[0]: leadership P membership A @1.0 (committed 0)
  Note right of n[1]: leadership F membership A @1.0 (committed 0)
  Note right of n[2]: leadership F membership A @1.0 (committed 0)
  n[0]->>n[0]: replicate 1.1 = [0 bytes]  [reconfiguration]
  n[0]->>n[0]: [ledger] appending: 1.1=[92 bytes] {"data":"eyIwIj
  n[0]->>n[0]: periodic for 10 ms
  n[1]->>n[1]: periodic for 10 ms
  n[2]->>n[2]: periodic for 10 ms
  n[0]->>n[2]: append_entries (0.0, 1.1] (term 1, commit 0)
  n[2]->>n[2]: [ledger] appending: 1.1=[92 bytes] {"data":"eyIwIj
  n[0]->>n[1]: append_entries (0.0, 1.1] (term 1, commit 0)
  n[1]->>n[1]: [ledger] appending: 1.1=[92 bytes] {"data":"eyIwIj
  n[1]-->>n[0]: append_entries_response ACK for 1.1
  n[0]->>n[0]: [KV] compacting to 1
  n[2]-->>n[0]: append_entries_response ACK for 1.1
  Note right of n[0]: leadership P membership A @1.1 (committed 1)
  Note right of n[1]: leadership F membership A @1.1 (committed 0)
  Note right of n[2]: leadership F membership R @1.1 (committed 0)

Test output requires: https://github.com/microsoft/CCF/pull/4811

[lemmy]

Fixed with 4a68e905b67805de09ed8ff537c7c15d645760e6

[achamayou]

Out of curiosity, how will this scenario be handled under a byzantine fault model, i.e., a leader that refuses to retire?

That's a good question!

Retirement is a transaction that writes to the KV the fact that the node is retired. That needs to be committed, and therefore signed. Our thinking and early implementation so far assumes that the primary needs to sign "at least this often", and that not doing that would result in the other nodes electing another node. Same thing for advancing commit.