Allow term change in MCccfraft.cfg and disable abs model refinement #6498

achamayou · 2024-09-25T08:25:41Z

Experiment following discussion in #6493 (comment).

Tried to run locally, but this seems very slow either way, so offloading to the CI. On runs lasting a few minutes, it looks like refinement lowers the state exploration rate from ~1.2m to ~800k.

Goal: find out if it is practical to raise the term limit in MCccfraft.tla.

achamayou · 2024-09-25T12:03:16Z

GitHub actions seems to have lost the full log after the timeout, but the result of this experiment is that Mccfraft becomes impractically slow, at least for CI purposes:

To clarify, this is for 483b547

achamayou · 2024-09-25T12:11:22Z

While 3 nodes with MaxTermLimit=3 is impractical, 2 nodes gets to a reproduction of the refinement failure quite quickly, as I suspected:

Finished computing initial states: 2 states generated, with 1 of them distinct at 2024-09-25 12:08:59.
Progress(20) at 2024-09-25 12:09:02: 68,185 states generated (68,185 s/min), 25,551 distinct states found (25,551 ds/min), 4,658 states left on queue.
Error: Action property line 51, col 20 to line 51, col 33 of module abs is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Follower)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ commitIndex = (n1 :> 4 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 4) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 2: <MCClientRequest(n1) line 62, col 5 to line 63, col 27 of module MCccfraft>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Follower)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ commitIndex = (n1 :> 4 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 4) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 3: <AppendEntries(n1,n2) line 681, col 5 to line 716, col 105 of module ccfraft>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Follower)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ commitIndex = (n1 :> 4 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<[commitIndex |-> 4, term |-> 2, dest |-> n2, source |-> n1, type |-> M_AppendEntriesRequest, prevLogIndex |-> 4, prevLogTerm |-> 2, entries |-> <<[contentType |-> T_Entry, term |-> 2]>>]>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 5) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 4: <MCSignCommittableMessages(n1) line 70, col 5 to line 71, col 37 of module MCccfraft>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Follower)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ commitIndex = (n1 :> 4 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<[commitIndex |-> 4, term |-> 2, dest |-> n2, source |-> n1, type |-> M_AppendEntriesRequest, prevLogIndex |-> 4, prevLogTerm |-> 2, entries |-> <<[contentType |-> T_Entry, term |-> 2]>>]>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 5) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 5: <RcvAppendEntriesRequest(n2,n1) line 1223, col 5 to line 1226, col 58 of module ccfraft>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Follower)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ commitIndex = (n1 :> 4 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<[term |-> 2, dest |-> n1, source |-> n2, type |-> M_AppendEntriesResponse, success |-> TRUE, lastLogIndex |-> 5]>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 5) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 6: <RcvAppendEntriesResponse(n1,n2) line 1229, col 5 to line 1237, col 55 of module ccfraft>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Follower)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 5) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ commitIndex = (n1 :> 4 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 5) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 7: <AppendEntries(n1,n2) line 681, col 5 to line 716, col 105 of module ccfraft>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Follower)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 5) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ commitIndex = (n1 :> 4 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<[commitIndex |-> 4, term |-> 2, dest |-> n2, source |-> n1, type |-> M_AppendEntriesRequest, prevLogIndex |-> 5, prevLogTerm |-> 2, entries |-> <<[contentType |-> T_Signature, term |-> 2]>>]>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 8: <RcvAppendEntriesRequest(n2,n1) line 1223, col 5 to line 1226, col 58 of module ccfraft>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Follower)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 5) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ commitIndex = (n1 :> 4 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<[term |-> 2, dest |-> n1, source |-> n2, type |-> M_AppendEntriesResponse, success |-> TRUE, lastLogIndex |-> 6]>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 9: <RcvAppendEntriesResponse(n1,n2) line 1229, col 5 to line 1237, col 55 of module ccfraft>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Follower)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ commitIndex = (n1 :> 4 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 10: <AdvanceCommitIndex(n1) line 845, col 5 to line 900, col 100 of module ccfraft>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Follower)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> Nil)
/\ commitIndex = (n1 :> 6 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 2)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 11: <MCTimeout(n2) line 46, col 5 to line 57, col 21 of module MCccfraft>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Candidate)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> n2)
/\ commitIndex = (n1 :> 6 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 3)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {n2})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 12: <RequestVote(n2,n1) line 670, col 5 to line 676, col 87 of module ccfraft>
/\ leadershipState = (n1 :> L_Leader @@ n2 :> L_Candidate)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> n2)
/\ commitIndex = (n1 :> 6 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<[term |-> 3, dest |-> n1, source |-> n2, type |-> M_RequestVoteRequest, lastCommittableTerm |-> 2, lastCommittableIndex |-> 6]>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 2 @@ n2 :> 3)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {n2})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 13: <RcvUpdateTerm(n1,n2) line 1204, col 5 to line 1206, col 42 of module ccfraft>
/\ leadershipState = (n1 :> L_Follower @@ n2 :> L_Candidate)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> Nil @@ n2 :> n2)
/\ commitIndex = (n1 :> 6 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<[term |-> 3, dest |-> n1, source |-> n2, type |-> M_RequestVoteRequest, lastCommittableTerm |-> 2, lastCommittableIndex |-> 6]>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 3 @@ n2 :> 3)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {n2})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 14: <RcvRequestVoteRequest(n1,n2) line 1209, col 5 to line 1212, col 56 of module ccfraft>
/\ leadershipState = (n1 :> L_Follower @@ n2 :> L_Candidate)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> n2 @@ n2 :> n2)
/\ commitIndex = (n1 :> 6 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<[term |-> 3, dest |-> n2, source |-> n1, type |-> M_RequestVoteResponse, voteGranted |-> TRUE]>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 3 @@ n2 :> 3)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {n2})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 15: <RcvRequestVoteResponse(n2,n1) line 1215, col 5 to line 1220, col 52 of module ccfraft>
/\ leadershipState = (n1 :> L_Follower @@ n2 :> L_Candidate)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> n2 @@ n2 :> n2)
/\ commitIndex = (n1 :> 6 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 3 @@ n2 :> 3)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votesGranted = (n1 :> {} @@ n2 :> {n1, n2})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 16: <BecomeLeader(n2) line 721, col 5 to line 739, col 130 of module ccfraft>
/\ leadershipState = (n1 :> L_Follower @@ n2 :> L_Leader)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> n2 @@ n2 :> n2)
/\ commitIndex = (n1 :> 6 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 3 @@ n2 :> 3)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 6 @@ n2 :> 6))
/\ votesGranted = (n1 :> {} @@ n2 :> {n1, n2})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 17: <MCSignCommittableMessages(n2) line 70, col 5 to line 71, col 37 of module MCccfraft>
/\ leadershipState = (n1 :> L_Follower @@ n2 :> L_Leader)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> n2 @@ n2 :> n2)
/\ commitIndex = (n1 :> 6 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 3 @@ n2 :> 3)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Signature, term |-> 3]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 6 @@ n2 :> 6))
/\ votesGranted = (n1 :> {} @@ n2 :> {n1, n2})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 18: <AppendEntries(n2,n1) line 681, col 5 to line 716, col 105 of module ccfraft>
/\ leadershipState = (n1 :> L_Follower @@ n2 :> L_Leader)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> n2 @@ n2 :> n2)
/\ commitIndex = (n1 :> 6 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<[commitIndex |-> 4, term |-> 3, dest |-> n1, source |-> n2, type |-> M_AppendEntriesRequest, prevLogIndex |-> 6, prevLogTerm |-> 2, entries |-> <<[contentType |-> T_Signature, term |-> 3]>>]>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 3 @@ n2 :> 3)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Signature, term |-> 3]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 7 @@ n2 :> 6))
/\ votesGranted = (n1 :> {} @@ n2 :> {n1, n2})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 19: <RcvAppendEntriesRequest(n1,n2) line 1223, col 5 to line 1226, col 58 of module ccfraft>
/\ leadershipState = (n1 :> L_Follower @@ n2 :> L_Leader)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 0 @@ n2 :> 0))
/\ votedFor = (n1 :> n2 @@ n2 :> n2)
/\ commitIndex = (n1 :> 6 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<[term |-> 3, dest |-> n2, source |-> n1, type |-> M_AppendEntriesResponse, success |-> TRUE, lastLogIndex |-> 7]>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 3 @@ n2 :> 3)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Signature, term |-> 3]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Signature, term |-> 3]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 7 @@ n2 :> 6))
/\ votesGranted = (n1 :> {} @@ n2 :> {n1, n2})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 20: <RcvAppendEntriesResponse(n2,n1) line 1229, col 5 to line 1237, col 55 of module ccfraft>
/\ leadershipState = (n1 :> L_Follower @@ n2 :> L_Leader)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 7 @@ n2 :> 0))
/\ votedFor = (n1 :> n2 @@ n2 :> n2)
/\ commitIndex = (n1 :> 6 @@ n2 :> 4)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 3 @@ n2 :> 3)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Signature, term |-> 3]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Signature, term |-> 3]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 7 @@ n2 :> 6))
/\ votesGranted = (n1 :> {} @@ n2 :> {n1, n2})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

State 21: <AdvanceCommitIndex(n2) line 845, col 5 to line 900, col 100 of module ccfraft>
/\ leadershipState = (n1 :> L_Follower @@ n2 :> L_Leader)
/\ retirementCompleted = (n1 :> {} @@ n2 :> {})
/\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 6) @@ n2 :> (n1 :> 7 @@ n2 :> 0))
/\ votedFor = (n1 :> n2 @@ n2 :> n2)
/\ commitIndex = (n1 :> 6 @@ n2 :> 7)
/\ membershipState = (n1 :> R_Active @@ n2 :> R_Active)
/\ messages = (n1 :> <<>> @@ n2 :> <<>>)
/\ isNewFollower = (n1 :> TRUE @@ n2 :> TRUE)
/\ hasJoined = (n1 :> TRUE @@ n2 :> TRUE)
/\ currentTerm = (n1 :> 3 @@ n2 :> 3)
/\ log = (n1 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Signature, term |-> 3]>> @@ n2 :> <<[contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Reconfiguration, term |-> 2, configuration |-> {n1, n2}], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Entry, term |-> 2], [contentType |-> T_Signature, term |-> 2], [contentType |-> T_Signature, term |-> 3]>>)
/\ sentIndex = (n1 :> (n1 :> 4 @@ n2 :> 6) @@ n2 :> (n1 :> 7 @@ n2 :> 6))
/\ votesGranted = (n1 :> {} @@ n2 :> {n1, n2})
/\ configurations = (n1 :> (3 :> {n1, n2}) @@ n2 :> (3 :> {n1, n2}))

"CounterExample written: MCccfraft.trace.tla"
"CounterExample written: MCccfraft.json"
"Writing stats to file: MCccfraft_stats.json"
106057 states generated, 39974 distinct states found, 6508 states left on queue.
The depth of the complete state graph search is 22.
Finished in 05s at (2024-09-25 12:09:03)
Trace exploration spec path: consensus/MCccfraft_TTrace_1727266138.tla

lemmy · 2024-09-26T01:03:39Z

+1 for creating a configuration with 1 configuration, 2 nodes, and one term change. Zooming out, here are dimensions I can think off by by we can slice and dice the space space:

Number of nodes
Number of elections
Number of reconfigurations
Network semantics
- msg ordering
- msg loss
- msg duplication
Syncing of divergent suffixes atomically (optimal)
Interval between signatures
Start with all nodes joined
...

achamayou · 2024-09-26T08:49:30Z

@lemmy 100%, that is what I was contemplating. We won't quite be able to do everything, so I think we need to pick what's "interesting" and do a bit of trial and error to work out which of those run in a sensible amount of time, and how many we can run concurrently before the cost of a CI run starts to become interesting itself.

Edit: is there a way to avoid the proliferation of 99%-identical configs are we do this?

lemmy · 2024-09-26T16:22:46Z

@lemmy 100%, that is what I was contemplating. We won't quite be able to do everything, so I think we need to pick what's "interesting" and do a bit of trial and error to work out which of those run in a sensible amount of time, and how many we can run concurrently before the cost of a CI run starts to become interesting itself.

Going round robin over a collection of models in different CI runs or a scheduled (e.g. weekend) run of bigger models would provide a good compromise.

Edit: is there a way to avoid the proliferation of 99%-identical configs are we do this?

There is nothing in TLC right now, but I will look into it.

achamayou · 2024-09-27T15:12:36Z

Replaced by #6504

Allow term change in MCccfraft.cfg and disable abs model refinement

483b547

Reproduce abs refinement failure without reconfiguration

f200482

achamayou mentioned this pull request Sep 25, 2024

Check refinement of high-level spec abs for configs with reconfiguration. #6493

Closed

achamayou closed this Sep 27, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Allow term change in MCccfraft.cfg and disable abs model refinement #6498

Allow term change in MCccfraft.cfg and disable abs model refinement #6498

achamayou commented Sep 25, 2024

achamayou commented Sep 25, 2024 •

edited

Loading

achamayou commented Sep 25, 2024

lemmy commented Sep 26, 2024

achamayou commented Sep 26, 2024 •

edited

Loading

lemmy commented Sep 26, 2024

achamayou commented Sep 27, 2024

Allow term change in MCccfraft.cfg and disable abs model refinement #6498

Allow term change in MCccfraft.cfg and disable abs model refinement #6498

Conversation

achamayou commented Sep 25, 2024

achamayou commented Sep 25, 2024 • edited Loading

achamayou commented Sep 25, 2024

lemmy commented Sep 26, 2024

achamayou commented Sep 26, 2024 • edited Loading

lemmy commented Sep 26, 2024

achamayou commented Sep 27, 2024

achamayou commented Sep 25, 2024 •

edited

Loading

achamayou commented Sep 26, 2024 •

edited

Loading