diff --git a/src/lib/raft/raft_sim.c b/src/lib/raft/raft_sim.c index 1adbee2..4dd54d8 100644 --- a/src/lib/raft/raft_sim.c +++ b/src/lib/raft/raft_sim.c @@ -1025,17 +1025,20 @@ void raft_sim_dump_trace(const raft_sim_cluster_t *c, FILE *fp, */ static const char *sim_tla_action_name(raft_sim_action_kind_t kind) { + /* Each return string is verbatim the raft.tla `Next` disjunct name (raft.tla:454); + * no per-case line numbers — they drift as raft.tla evolves and the name IS the + * stable spec reference. */ switch (kind) { - case RAFT_SIM_ACT_RESTART: return "Restart"; /* raft.tla:166 */ - case RAFT_SIM_ACT_TIMEOUT: return "Timeout"; /* raft.tla:178 */ - case RAFT_SIM_ACT_REQUEST_VOTE: return "RequestVote"; /* raft.tla:190 */ - case RAFT_SIM_ACT_BECOME_LEADER: return "BecomeLeader"; /* raft.tla:229 */ - case RAFT_SIM_ACT_CLIENT_REQUEST: return "ClientRequest"; /* raft.tla:246 */ - case RAFT_SIM_ACT_APPEND_ENTRIES: return "AppendEntries"; /* raft.tla:218 */ - case RAFT_SIM_ACT_ADVANCE_COMMIT: return "AdvanceCommitIndex"; /* raft.tla:259 */ - case RAFT_SIM_ACT_RECEIVE: return "Receive"; /* raft.tla:421 */ - case RAFT_SIM_ACT_DUPLICATE_MESSAGE: return "DuplicateMessage"; /* raft.tla:443 */ - case RAFT_SIM_ACT_DROP_MESSAGE: return "DropMessage"; /* raft.tla:448 */ + case RAFT_SIM_ACT_RESTART: return "Restart"; + case RAFT_SIM_ACT_TIMEOUT: return "Timeout"; + case RAFT_SIM_ACT_REQUEST_VOTE: return "RequestVote"; + case RAFT_SIM_ACT_BECOME_LEADER: return "BecomeLeader"; + case RAFT_SIM_ACT_CLIENT_REQUEST: return "ClientRequest"; + case RAFT_SIM_ACT_APPEND_ENTRIES: return "AppendEntries"; + case RAFT_SIM_ACT_ADVANCE_COMMIT: return "AdvanceCommitIndex"; + case RAFT_SIM_ACT_RECEIVE: return "Receive"; + case RAFT_SIM_ACT_DUPLICATE_MESSAGE: return "DuplicateMessage"; + case RAFT_SIM_ACT_DROP_MESSAGE: return "DropMessage"; } return "Unknown"; } diff --git a/src/lib/testsuite/test_raft.c b/src/lib/testsuite/test_raft.c index c3b8bc2..def2b22 100644 --- a/src/lib/testsuite/test_raft.c +++ b/src/lib/testsuite/test_raft.c @@ -8229,22 +8229,27 @@ static void test_sim_5_1_partition_heal(void) "post-heal cluster does not have exactly one leader"); /* Convergence is observable: the leader committed a non-trivial prefix, and - * every (formerly-isolated) node's committed entries match the leader's at the - * same index/term over their shared committed prefix. */ + * every (formerly-isolated) node's REPLICATED LOG matches the leader's at the + * same index/term over their shared log prefix. NOTE: this library uses a + * leader-only commit model (a follower's commit_index does not advance from + * AppendEntries — see Implementation Notes), so followers end at commit_index=0; + * bounding by commit_index would make this loop vacuous. Bound by log_count + * instead, which followers DO advance via replication — Log Matching (asserted + * each step via raft_sim_check_all) guarantees the shared-prefix terms agree. */ TEST_ASSERT_TRUE_MESSAGE(c.nodes[leader_idx].commit_index > 0, "leader never committed any entry across the scenario"); for (int i = 0; i < c.n; i++) { if (i == leader_idx) continue; - uint64_t shared = c.nodes[i].commit_index; - if (shared > c.nodes[leader_idx].commit_index) - shared = c.nodes[leader_idx].commit_index; + uint64_t shared = (uint64_t)c.nodes[i].log_count; + if (shared > (uint64_t)c.nodes[leader_idx].log_count) + shared = (uint64_t)c.nodes[leader_idx].log_count; for (uint64_t e = 1; e <= shared; e++) { TEST_ASSERT_EQUAL_UINT64_MESSAGE( c.nodes[leader_idx].log[e - 1].term, c.nodes[i].log[e - 1].term, - "formerly-isolated node diverges from leader committed prefix"); + "formerly-isolated node diverges from leader's replicated log prefix"); } } }