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

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

About this issue

  • Original URL
  • State: closed
  • Created 2 years ago
  • Comments: 25 (10 by maintainers)

Commits related to this issue

Most upvoted comments

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.

+1
achamayou on Jan 11, 2023

@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.

+1
achamayou on Nov 30, 2022

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

+1
heidihoward on Nov 22, 2022
Read more comments on GitHub
← CCF: code_update_test fails on CI
CCF: samples/apps/logging cmake undefined pthread  →