From 6760078421ce5ab3ffbcd9a076d9afb705f8c926 Mon Sep 17 00:00:00 2001
From: Rudy Celekli <rudy@gradiahq.com>
Date: Fri, 23 Oct 2026 23:38:48 -0400
Subject: [PATCH] fix(pstack): avoid reserved TLA action names

---
 .../statechart/scripts/chart-to-tla.mjs       |  2 +-
 .../test/chart-to-tla-reserved.test.mjs       | 23 +++++++++++++++++++
 .../statechart/scripts/chart-to-tla.mjs       |  2 +-
 .../test/chart-to-tla-reserved.test.mjs       | 23 +++++++++++++++++++
 4 files changed, 48 insertions(+), 2 deletions(-)
 create mode 100644 harness/pstack/claude-code/skills/statechart/scripts/test/chart-to-tla-reserved.test.mjs
 create mode 100644 pstack/skills/statechart/scripts/test/chart-to-tla-reserved.test.mjs

diff --git a/harness/pstack/claude-code/skills/statechart/scripts/chart-to-tla.mjs b/harness/pstack/claude-code/skills/statechart/scripts/chart-to-tla.mjs
index 911c58698..664d3cbbd 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/chart-to-tla.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/chart-to-tla.mjs
@@ -24,7 +24,7 @@ if (!args.chart || !/^[A-Za-z][A-Za-z0-9_]*$/.test(args.module ?? "")) {
 const dir = args.dir ?? path.dirname(args.chart);
 const { regions, nevers } = parseMermaid(fs.readFileSync(args.chart, "utf8"));
 
-const RESERVED = new Set(["vars", "Init", "Next", "Spec", "TypeOK", "Settled"]);
+const RESERVED = new Set(["vars", "Init", "Next", "Spec", "TypeOK", "Settled", "UNCHANGED"]);
 const taken = new Set(RESERVED);
 function ident(words, lower) {
   const parts = words
diff --git a/harness/pstack/claude-code/skills/statechart/scripts/test/chart-to-tla-reserved.test.mjs b/harness/pstack/claude-code/skills/statechart/scripts/test/chart-to-tla-reserved.test.mjs
new file mode 100644
index 000000000..a5257a517
--- /dev/null
+++ b/harness/pstack/claude-code/skills/statechart/scripts/test/chart-to-tla-reserved.test.mjs
@@ -0,0 +1,23 @@
+import assert from "node:assert/strict";
+import { execFileSync } from "node:child_process";
+import { mkdtempSync, readFileSync, writeFileSync } from "node:fs";
+import { tmpdir } from "node:os";
+import { dirname, join } from "node:path";
+import { fileURLToPath } from "node:url";
+import { test } from "node:test";
+
+const scripts = dirname(dirname(fileURLToPath(import.meta.url)));
+
+test("chart-to-tla avoids TLA+ keywords for generated action names", () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  writeFileSync(
+    join(dir, "chart.mmd"),
+    "stateDiagram-v2\n  [*] --> A\n  A --> B : UNCHANGED\n",
+  );
+  execFileSync(process.execPath, [join(scripts, "chart-to-tla.mjs"), "chart.mmd", "--module", "Chart"], {
+    cwd: dir,
+  });
+  const spec = readFileSync(join(dir, "Chart.tla"), "utf8");
+  assert.match(spec, /^UNCHANGED2 ==$/m);
+  assert.doesNotMatch(spec, /^UNCHANGED ==$/m);
+});
diff --git a/pstack/skills/statechart/scripts/chart-to-tla.mjs b/pstack/skills/statechart/scripts/chart-to-tla.mjs
index 911c58698..664d3cbbd 100644
--- a/pstack/skills/statechart/scripts/chart-to-tla.mjs
+++ b/pstack/skills/statechart/scripts/chart-to-tla.mjs
@@ -24,7 +24,7 @@ if (!args.chart || !/^[A-Za-z][A-Za-z0-9_]*$/.test(args.module ?? "")) {
 const dir = args.dir ?? path.dirname(args.chart);
 const { regions, nevers } = parseMermaid(fs.readFileSync(args.chart, "utf8"));
 
-const RESERVED = new Set(["vars", "Init", "Next", "Spec", "TypeOK", "Settled"]);
+const RESERVED = new Set(["vars", "Init", "Next", "Spec", "TypeOK", "Settled", "UNCHANGED"]);
 const taken = new Set(RESERVED);
 function ident(words, lower) {
   const parts = words
diff --git a/pstack/skills/statechart/scripts/test/chart-to-tla-reserved.test.mjs b/pstack/skills/statechart/scripts/test/chart-to-tla-reserved.test.mjs
new file mode 100644
index 000000000..a5257a517
--- /dev/null
+++ b/pstack/skills/statechart/scripts/test/chart-to-tla-reserved.test.mjs
@@ -0,0 +1,23 @@
+import assert from "node:assert/strict";
+import { execFileSync } from "node:child_process";
+import { mkdtempSync, readFileSync, writeFileSync } from "node:fs";
+import { tmpdir } from "node:os";
+import { dirname, join } from "node:path";
+import { fileURLToPath } from "node:url";
+import { test } from "node:test";
+
+const scripts = dirname(dirname(fileURLToPath(import.meta.url)));
+
+test("chart-to-tla avoids TLA+ keywords for generated action names", () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  writeFileSync(
+    join(dir, "chart.mmd"),
+    "stateDiagram-v2\n  [*] --> A\n  A --> B : UNCHANGED\n",
+  );
+  execFileSync(process.execPath, [join(scripts, "chart-to-tla.mjs"), "chart.mmd", "--module", "Chart"], {
+    cwd: dir,
+  });
+  const spec = readFileSync(join(dir, "Chart.tla"), "utf8");
+  assert.match(spec, /^UNCHANGED2 ==$/m);
+  assert.doesNotMatch(spec, /^UNCHANGED ==$/m);
+});