diff --git a/.kiro/specs/raft-sim-conformance/tasks.md b/.kiro/specs/raft-sim-conformance/tasks.md index 6168dc2..bc76d04 100644 --- a/.kiro/specs/raft-sim-conformance/tasks.md +++ b/.kiro/specs/raft-sim-conformance/tasks.md @@ -201,7 +201,7 @@ ## 8. Optional TLC-consumable trace export -- [ ]* 8.1 TLC-consumable trace export (deferred; off by default) +- [x]* 8.1 TLC-consumable trace export (deferred; off by default) - Implement `raft_sim_export_trace` gated by `RAFT_SIM_EXPORT`: per step, emit the action + tracked `raft.tla` variables (`messages` summary, per-node `currentTerm`/`state`/`log`/`commitIndex`) named per `raft/raft.tla`, in a stable line-oriented format; off by default - Observable completion: with `RAFT_SIM_EXPORT` set, a run emits a stable, spec-named record stream; default runs emit nothing extra - _Requirements: 8.1, 8.2, 8.3_ diff --git a/src/lib/raft/raft.h b/src/lib/raft/raft.h index ea94d5e..1d9b846 100644 --- a/src/lib/raft/raft.h +++ b/src/lib/raft/raft.h @@ -923,6 +923,23 @@ void raft_sim_trace_record(raft_sim_cluster_t *c, raft_sim_action_t action); void raft_sim_dump_trace(const raft_sim_cluster_t *c, FILE *fp, raft_sim_invariant_t failing); +/* + * raft_sim_export_trace: optional TLC-consumable trace export (task 8.1; Req 8.1, + * 8.2, 8.3). Emits a STABLE, line-oriented, machine-readable record of the + * harness's tracked raft.tla variables to `fp`: a header line (seed, n), the + * ordered action trace (each action named per raft.tla's Next disjuncts), and the + * resulting tracked variables — per node `currentTerm`, `state` (Follower/ + * Candidate/Leader), `log` (the (term, value) sequence), `commitIndex`, plus a + * `messages` bag summary. Names match raft/raft.tla (R8.2) so the export maps to + * spec actions/variables without re-interpretation. + * + * Gated OFF by default (R8.3): a no-op (emits NOTHING) unless the RAFT_SIM_EXPORT + * environment variable is set — mirroring the RAFT_SIM_VERBOSE quiet-on-success + * idiom. The standard CI conformance run never sets it, so it incurs no export + * overhead. Output is deterministic/stable (no addresses, no wall-clock). + */ +void raft_sim_export_trace(const raft_sim_cluster_t *c, FILE *fp); + /* * raft_sim_advance_commit: drive raft_advance_commit on node_idx (task 6.1). * diff --git a/src/lib/raft/raft_sim.c b/src/lib/raft/raft_sim.c index 3967a64..1adbee2 100644 --- a/src/lib/raft/raft_sim.c +++ b/src/lib/raft/raft_sim.c @@ -1015,6 +1015,137 @@ void raft_sim_dump_trace(const raft_sim_cluster_t *c, FILE *fp, } } +/* ---------- optional TLC-consumable trace export (task 8.1) ---------- */ + +/* + * sim_tla_action_name: map a harness action kind to the corresponding raft.tla + * `Next` disjunct name (R8.2), so the export reads in the spec's own vocabulary + * (raft.tla:454). Distinct from raft_sim_action_kind_name (kebab-case, human dump): + * this is the PascalCase spec-action name a maintainer maps directly to raft.tla. + */ +static const char *sim_tla_action_name(raft_sim_action_kind_t kind) +{ + 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 */ + } + return "Unknown"; +} + +/* + * sim_tla_state_name: map the library role enum to the raft.tla `state` value name + * (Follower/Candidate/Leader, raft.tla:17/144) so the per-node export uses the spec + * name for `state[i]` directly. + */ +static const char *sim_tla_state_name(raft_role_t role) +{ + switch (role) { + case RAFT_FOLLOWER: return "Follower"; + case RAFT_CANDIDATE: return "Candidate"; + case RAFT_LEADER: return "Leader"; + } + return "Unknown"; +} + +/* + * sim_tla_msg_kind_name: map a bag message kind to the raft.tla message `mtype` + * (RequestVoteRequest/RequestVoteResponse/AppendEntriesRequest/AppendEntriesResponse, + * raft.tla:23-24) for the `messages` bag summary. + */ +static const char *sim_tla_msg_kind_name(raft_sim_msg_kind_t kind) +{ + switch (kind) { + case RAFT_SIM_MSG_VOTE_REQ: return "RequestVoteRequest"; + case RAFT_SIM_MSG_VOTE_RSP: return "RequestVoteResponse"; + case RAFT_SIM_MSG_AE_REQ: return "AppendEntriesRequest"; + case RAFT_SIM_MSG_AE_RSP: return "AppendEntriesResponse"; + } + return "Unknown"; +} + +/* + * raft_sim_export_trace: STABLE, line-oriented, machine-readable export of the + * harness's tracked raft.tla variables (R8.1) using raft.tla-consistent names (R8.2), + * gated OFF by default behind RAFT_SIM_EXPORT (R8.3 — mirrors the RAFT_SIM_VERBOSE + * idiom in raft_sim_dump_trace). Documented format (one record per line; fields are + * `key=value`; deterministic — no addresses, no wall-clock): + * + * trace-export seed= n= steps= + * action name= actor= msg_index= term= index= + * ... one per recorded c->trace[] step, in order ... + * node currentTerm= state= commitIndex= \ + * log=[(,);...] + * ... one per node ... + * messages count= []={src=..,dst=..,term=..} ... + * + * The action lines ARE the per-step sequence (R8.1's "per step"); a deterministic + * replay from (seed, n, steps) reconstructs the per-step intermediate state, while the + * node/messages lines pin the resulting tracked variables. `log` decodes each entry's + * client value with the same little-endian decode applied[] uses, so the (term, value) + * sequence matches raft.tla `log[i]`. + */ +void raft_sim_export_trace(const raft_sim_cluster_t *c, FILE *fp) +{ + /* Default-OFF gate (R8.3): emit NOTHING unless explicitly enabled. */ + if (getenv("RAFT_SIM_EXPORT") == NULL) + return; + + /* Header: run key + step count (R8.1). */ + fprintf(fp, "trace-export seed=%llu n=%d steps=%d\n", + (unsigned long long)c->seed, c->n, c->trace_len); + + /* Ordered action trace — each named per raft.tla's Next disjuncts (R8.2). */ + for (int i = 0; i < c->trace_len; i++) { + const raft_sim_action_t *a = &c->trace[i]; + fprintf(fp, + "action %d name=%s actor=%d msg_index=%d term=%llu index=%llu\n", + i, sim_tla_action_name(a->kind), a->actor, a->msg_index, + (unsigned long long)a->term, (unsigned long long)a->index); + } + + /* Per-node resulting tracked variables: currentTerm, state, commitIndex, log + * (the (term, value) sequence) — raft.tla variable names (R8.1, R8.2). */ + for (int i = 0; i < c->n; i++) { + const raft_sim_node_t *node = &c->nodes[i]; + + raft_snapshot_t snap; + raft_snapshot(&node->state, &snap); + + fprintf(fp, "node %d currentTerm=%llu state=%s commitIndex=%llu log=[", + i, (unsigned long long)snap.term, + sim_tla_state_name(snap.role), + (unsigned long long)node->commit_index); + + for (int k = 1; k <= node->log_count; k++) { + const raft_sim_entry_t *slot = &node->log[k - 1]; + uint64_t value = sim_conf_decode_value(slot); + fprintf(fp, "%s(%llu,%llu)", (k > 1) ? ";" : "", + (unsigned long long)slot->term, + (unsigned long long)value); + } + fprintf(fp, "]\n"); + } + + /* `messages` bag summary: count + per-member (type, src, dst, term). Mirrors + * raft.tla `messages` (the in-flight RPC bag). */ + fprintf(fp, "messages count=%d", c->bag_count); + for (int i = 0; i < c->bag_count; i++) { + const raft_sim_msg_t *m = &c->bag[i]; + fprintf(fp, " [%d]=%s{src=%d,dst=%d,term=%llu}", + i, sim_tla_msg_kind_name(m->kind), m->src, m->dst, + (unsigned long long)m->term); + } + fprintf(fp, "\n"); +} + int raft_sim_restart_node(raft_sim_cluster_t *c, int node_idx) { if (node_idx < 0 || node_idx >= c->n) diff --git a/src/lib/testsuite/test_raft.c b/src/lib/testsuite/test_raft.c index 5ddd28b..c3b8bc2 100644 --- a/src/lib/testsuite/test_raft.c +++ b/src/lib/testsuite/test_raft.c @@ -5362,6 +5362,98 @@ static void test_sim_4_1_trace_record_and_dump(void) setenv("RAFT_SIM_VERBOSE", saved_copy, 1); } +/* + * test_sim_8_1_export_trace_named_and_gated (raft-sim-conformance task 8.1; + * Req 8.1, 8.2, 8.3) + * + * raft_sim_export_trace emits a STABLE, line-oriented, machine-readable record of + * the harness's tracked raft.tla variables, gated OFF by default via the + * RAFT_SIM_EXPORT environment variable (mirroring the RAFT_SIM_VERBOSE idiom): + * - Export ON (RAFT_SIM_EXPORT set): a post-run cluster's export CONTAINS the + * spec-named tokens (currentTerm, state, log, commitIndex, messages — R8.2), + * the seed/n header, and at least one action name from the recorded trace + * (R8.1). Two exports of the same post-run state are byte-identical (stable). + * - Default OFF (RAFT_SIM_EXPORT unset): the export emits NOTHING (R8.3). + * The env var is saved and restored around the test so the rest of the suite is + * unperturbed. + */ +static void test_sim_8_1_export_trace_named_and_gated(void) +{ + /* Save + clear the gate so we control it deterministically. */ + char *saved_export = getenv("RAFT_SIM_EXPORT"); + char saved_copy[256]; + int had_export = (saved_export != NULL); + if (had_export) { + strncpy(saved_copy, saved_export, sizeof(saved_copy) - 1); + saved_copy[sizeof(saved_copy) - 1] = '\0'; + } + + /* Drive a short deterministic run so trace[] holds actions and nodes carry + * observable state (term/log/commit). Seed 3 is the one the 4.2 test proves + * completes a clean run on the correct library. */ + raft_sim_cluster_t c; + memset(&c, 0, sizeof(c)); + TEST_ASSERT_EQUAL_INT(0, raft_sim_conformance_init(&c, 3, 2000, 3ULL)); + for (int step = 0; step < 80; step++) { + int rc = raft_sim_step(&c); + TEST_ASSERT_TRUE(rc >= 0); + } + TEST_ASSERT_TRUE(c.trace_len > 0); /* the run recorded actions to export */ + + /* ---- Export ON (R8.1, R8.2) ---- */ + setenv("RAFT_SIM_EXPORT", "1", 1); + + char buf[8192]; + memset(buf, 0, sizeof(buf)); + FILE *fp = fmemopen(buf, sizeof(buf), "w"); + TEST_ASSERT_NOT_NULL(fp); + raft_sim_export_trace(&c, fp); + fclose(fp); + + TEST_ASSERT_TRUE(strlen(buf) > 0); + /* raft.tla-named tracked variables (R8.2). */ + TEST_ASSERT_NOT_NULL(strstr(buf, "currentTerm")); + TEST_ASSERT_NOT_NULL(strstr(buf, "state")); + TEST_ASSERT_NOT_NULL(strstr(buf, "log")); + TEST_ASSERT_NOT_NULL(strstr(buf, "commitIndex")); + TEST_ASSERT_NOT_NULL(strstr(buf, "messages")); + /* seed/n header (R8.1). */ + { + char seedtok[32]; + snprintf(seedtok, sizeof(seedtok), "%llu", (unsigned long long)c.seed); + TEST_ASSERT_NOT_NULL(strstr(buf, seedtok)); + TEST_ASSERT_NOT_NULL(strstr(buf, "seed")); + TEST_ASSERT_NOT_NULL(strstr(buf, "n=")); + } + /* At least one raft.tla Next action name appears (R8.1/R8.2). The scheduler + * always drives Timeout, so it is reliably present. */ + TEST_ASSERT_NOT_NULL(strstr(buf, "Timeout")); + + /* Stability: a second export of the same post-run state is byte-identical. */ + char buf2[8192]; + memset(buf2, 0, sizeof(buf2)); + FILE *fp2 = fmemopen(buf2, sizeof(buf2), "w"); + TEST_ASSERT_NOT_NULL(fp2); + raft_sim_export_trace(&c, fp2); + fclose(fp2); + TEST_ASSERT_EQUAL_INT(0, strcmp(buf, buf2)); /* deterministic / stable */ + + /* ---- Default OFF (R8.3): gate unset => emit NOTHING ---- */ + unsetenv("RAFT_SIM_EXPORT"); + char qbuf[256]; + memset(qbuf, 0, sizeof(qbuf)); + FILE *qfp = fmemopen(qbuf, sizeof(qbuf), "w"); + TEST_ASSERT_NOT_NULL(qfp); + raft_sim_export_trace(&c, qfp); + fclose(qfp); + TEST_ASSERT_EQUAL_INT(0, (int)strlen(qbuf)); /* silent unless explicitly enabled */ + + if (had_export) + setenv("RAFT_SIM_EXPORT", saved_copy, 1); + else + unsetenv("RAFT_SIM_EXPORT"); +} + /* ---------- Group A: Basic Election Correctness (task 5.1) ---------- */ /* @@ -9020,6 +9112,7 @@ void test_raft(void) RUN_TEST(test_sim_2_2_drop_duplicate_preserve_node_state); RUN_TEST(test_sim_2_2_reorder_prng_deterministic); RUN_TEST(test_sim_4_1_trace_record_and_dump); + RUN_TEST(test_sim_8_1_export_trace_named_and_gated); RUN_TEST(test_sim_4_2_step_liveness_and_coverage); RUN_TEST(test_sim_4_2_step_halts_on_forced_violation); RUN_TEST(test_sim_4_3_restart_preserves_persistence);