From 900f39fc950881b2d024b1ec8a2e897c5caeebb3 Mon Sep 17 00:00:00 2001
From: Dean Rie <deanalexrie@gmail.com>
Date: Fri, 23 Oct 2026 07:38:58 +0300
Subject: [PATCH 1/5] fix(pstack): statechart refuses foreign files nested
 under tlc/ or behind an owned name

foreign() matched the OWN regex against immediate entry names only, so a
user's tlc/notes.md, a folder named chart.mmd, or a folder named .DS_Store
passed the check and publish() removed them with the previous output
folder. The preservation contract from #741 is that a run refuses files
it did not write.

Only a regular file under an owned name is the run's own. tlc/ is owned
as a folder whose entries are the files this script writes there
(*.cfg, *.out, *.dot, regions-proof.mmd, regions-all.mmd; TLC's metadir
is in the system temp folder), checked one level down. A folder or link
under an owned name is foreign and is reported by its path.

Test covers tlc/notes.md, a folder named chart.mmd, a folder named
.DS_Store, a symlink named chart.mmd (refused, target untouched), and a
folder of only owned files passing to the next step. Fails on main.
Harness tree regenerated.

Fixes #773.
---
 .../skills/statechart/scripts/statechart.mjs  | 19 +++++--
 .../scripts/test/statechart.test.mjs          | 51 +++++++++++++++++++
 .../skills/statechart/scripts/statechart.mjs  | 19 +++++--
 .../scripts/test/statechart.test.mjs          | 51 +++++++++++++++++++
 4 files changed, 130 insertions(+), 10 deletions(-)

diff --git a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
index 555f10b8c..ff02115b7 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
@@ -578,15 +578,24 @@ function renderFile(input, flags, { lib, theme }) {
 
 const published = (work, out) => (file) => rel(path.join(out, path.relative(work, file)));
 
+// Files a run writes at the top of its output folder, and inside tlc/. Only a regular file with one
+// of these names is the run's own; a folder (or a link) under an owned name is not, and neither is
+// anything nested under tlc/ that TLC or this script did not write. publish() removes the previous
+// folder whole, so everything it holds must be ours.
 const OWN =
-  /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|tlc|\.DS_Store)$/;
+  /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|\.DS_Store)$/;
+const OWN_TLC = /^([^/]+\.(cfg|out|dot)|regions-(proof|all)\.mmd)$/;
 
 function foreign(dir) {
   try {
-    return fs
-      .readdirSync(dir)
-      .filter((f) => !OWN.test(f))
-      .sort();
+    const found = [];
+    for (const entry of fs.readdirSync(dir, { withFileTypes: true })) {
+      if (entry.name === "tlc" && entry.isDirectory()) {
+        for (const inner of fs.readdirSync(path.join(dir, "tlc"), { withFileTypes: true }))
+          if (!(inner.isFile() && OWN_TLC.test(inner.name))) found.push(`tlc/${inner.name}`);
+      } else if (!(entry.isFile() && OWN.test(entry.name))) found.push(entry.name);
+    }
+    return found.sort();
   } catch (e) {
     if (e.code === "ENOENT") return [];
     throw new CannotFinish(`cannot use ${rel(dir)} as the output folder: ${e.message}`);
diff --git a/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs b/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
index 543fe8d67..02f55e192 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
@@ -1536,6 +1536,57 @@ test("statechart.mjs does not use an output folder that has files that it did no
   assert.equal(readFileSync(join(out, "chart.mmd"), "utf8"), "kept\n");
 });
 
+test("statechart.mjs refuses an output folder with foreign files under tlc/ or behind an owned name", () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  writeFileSync(join(dir, "tla2tools.jar"), "");
+  writeFileSync(join(dir, "Pay.tla"), "---- MODULE Pay ----\n====\n");
+  writeFileSync(join(dir, "Pay.cfg"), "SPECIFICATION Spec\n");
+  const env = { TLA2TOOLS: join(dir, "tla2tools.jar") };
+  const refused = (out, expected) => {
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.equal(
+      r.stderr,
+      `${out} has a file that this command did not write: ${expected}. A run puts its files in place of the whole output folder, so pass --out with a new folder.\n`,
+    );
+  };
+
+  // A user's file inside the owned tlc/ folder.
+  mkdirSync(join(dir, "nested", "tlc"), { recursive: true });
+  writeFileSync(join(dir, "nested", "tlc", "Pay.out"), "");
+  writeFileSync(join(dir, "nested", "tlc", "notes.md"), "mine\n");
+  refused("nested", "tlc/notes.md");
+  assert.equal(readFileSync(join(dir, "nested", "tlc", "notes.md"), "utf8"), "mine\n");
+
+  // A folder that carries the name of a generated file.
+  mkdirSync(join(dir, "typed", "chart.mmd"), { recursive: true });
+  writeFileSync(join(dir, "typed", "chart.mmd", "notes.md"), "mine\n");
+  refused("typed", "chart.mmd");
+
+  // The same with the ignored Finder file.
+  mkdirSync(join(dir, "finder", ".DS_Store"), { recursive: true });
+  writeFileSync(join(dir, "finder", ".DS_Store", "notes.md"), "mine\n");
+  refused("finder", ".DS_Store");
+
+  // A link under an owned name is not the run's file either.
+  mkdirSync(join(dir, "linked"));
+  writeFileSync(join(dir, "elsewhere.mmd"), "theirs\n");
+  symlinkSync(join(dir, "elsewhere.mmd"), join(dir, "linked", "chart.mmd"));
+  refused("linked", "chart.mmd");
+  assert.equal(readFileSync(join(dir, "elsewhere.mmd"), "utf8"), "theirs\n");
+
+  // The run's own files, including the whole of tlc/, still pass.
+  mkdirSync(join(dir, "own", "tlc"), { recursive: true });
+  for (const f of ["chart.mmd", "stories.md", "summary.json", ".DS_Store", "bug-1.png"])
+    writeFileSync(join(dir, "own", f), "");
+  for (const f of ["Pay.cfg", "Pay.out", "Pay.dot", "Pay-Safe.cfg", "regions-proof.mmd"])
+    writeFileSync(join(dir, "own", "tlc", f), "");
+  // The run gets past the ownership check and stops at the next step, the missing mapping.
+  const own = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", "own"], dir, env);
+  assert.doesNotMatch(own.stderr, /did not write/);
+  assert.match(own.stderr, /Wrote Pay\.map\.mjs/);
+});
+
 test("statechart.mjs exits 2 and names a helper script that cannot start", () => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-"));
   writeFileSync(join(dir, "notes-app.mmd"), fixture("sync.mmd"));
diff --git a/pstack/skills/statechart/scripts/statechart.mjs b/pstack/skills/statechart/scripts/statechart.mjs
index 555f10b8c..ff02115b7 100644
--- a/pstack/skills/statechart/scripts/statechart.mjs
+++ b/pstack/skills/statechart/scripts/statechart.mjs
@@ -578,15 +578,24 @@ function renderFile(input, flags, { lib, theme }) {
 
 const published = (work, out) => (file) => rel(path.join(out, path.relative(work, file)));
 
+// Files a run writes at the top of its output folder, and inside tlc/. Only a regular file with one
+// of these names is the run's own; a folder (or a link) under an owned name is not, and neither is
+// anything nested under tlc/ that TLC or this script did not write. publish() removes the previous
+// folder whole, so everything it holds must be ours.
 const OWN =
-  /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|tlc|\.DS_Store)$/;
+  /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|\.DS_Store)$/;
+const OWN_TLC = /^([^/]+\.(cfg|out|dot)|regions-(proof|all)\.mmd)$/;
 
 function foreign(dir) {
   try {
-    return fs
-      .readdirSync(dir)
-      .filter((f) => !OWN.test(f))
-      .sort();
+    const found = [];
+    for (const entry of fs.readdirSync(dir, { withFileTypes: true })) {
+      if (entry.name === "tlc" && entry.isDirectory()) {
+        for (const inner of fs.readdirSync(path.join(dir, "tlc"), { withFileTypes: true }))
+          if (!(inner.isFile() && OWN_TLC.test(inner.name))) found.push(`tlc/${inner.name}`);
+      } else if (!(entry.isFile() && OWN.test(entry.name))) found.push(entry.name);
+    }
+    return found.sort();
   } catch (e) {
     if (e.code === "ENOENT") return [];
     throw new CannotFinish(`cannot use ${rel(dir)} as the output folder: ${e.message}`);
diff --git a/pstack/skills/statechart/scripts/test/statechart.test.mjs b/pstack/skills/statechart/scripts/test/statechart.test.mjs
index 543fe8d67..02f55e192 100644
--- a/pstack/skills/statechart/scripts/test/statechart.test.mjs
+++ b/pstack/skills/statechart/scripts/test/statechart.test.mjs
@@ -1536,6 +1536,57 @@ test("statechart.mjs does not use an output folder that has files that it did no
   assert.equal(readFileSync(join(out, "chart.mmd"), "utf8"), "kept\n");
 });
 
+test("statechart.mjs refuses an output folder with foreign files under tlc/ or behind an owned name", () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  writeFileSync(join(dir, "tla2tools.jar"), "");
+  writeFileSync(join(dir, "Pay.tla"), "---- MODULE Pay ----\n====\n");
+  writeFileSync(join(dir, "Pay.cfg"), "SPECIFICATION Spec\n");
+  const env = { TLA2TOOLS: join(dir, "tla2tools.jar") };
+  const refused = (out, expected) => {
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.equal(
+      r.stderr,
+      `${out} has a file that this command did not write: ${expected}. A run puts its files in place of the whole output folder, so pass --out with a new folder.\n`,
+    );
+  };
+
+  // A user's file inside the owned tlc/ folder.
+  mkdirSync(join(dir, "nested", "tlc"), { recursive: true });
+  writeFileSync(join(dir, "nested", "tlc", "Pay.out"), "");
+  writeFileSync(join(dir, "nested", "tlc", "notes.md"), "mine\n");
+  refused("nested", "tlc/notes.md");
+  assert.equal(readFileSync(join(dir, "nested", "tlc", "notes.md"), "utf8"), "mine\n");
+
+  // A folder that carries the name of a generated file.
+  mkdirSync(join(dir, "typed", "chart.mmd"), { recursive: true });
+  writeFileSync(join(dir, "typed", "chart.mmd", "notes.md"), "mine\n");
+  refused("typed", "chart.mmd");
+
+  // The same with the ignored Finder file.
+  mkdirSync(join(dir, "finder", ".DS_Store"), { recursive: true });
+  writeFileSync(join(dir, "finder", ".DS_Store", "notes.md"), "mine\n");
+  refused("finder", ".DS_Store");
+
+  // A link under an owned name is not the run's file either.
+  mkdirSync(join(dir, "linked"));
+  writeFileSync(join(dir, "elsewhere.mmd"), "theirs\n");
+  symlinkSync(join(dir, "elsewhere.mmd"), join(dir, "linked", "chart.mmd"));
+  refused("linked", "chart.mmd");
+  assert.equal(readFileSync(join(dir, "elsewhere.mmd"), "utf8"), "theirs\n");
+
+  // The run's own files, including the whole of tlc/, still pass.
+  mkdirSync(join(dir, "own", "tlc"), { recursive: true });
+  for (const f of ["chart.mmd", "stories.md", "summary.json", ".DS_Store", "bug-1.png"])
+    writeFileSync(join(dir, "own", f), "");
+  for (const f of ["Pay.cfg", "Pay.out", "Pay.dot", "Pay-Safe.cfg", "regions-proof.mmd"])
+    writeFileSync(join(dir, "own", "tlc", f), "");
+  // The run gets past the ownership check and stops at the next step, the missing mapping.
+  const own = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", "own"], dir, env);
+  assert.doesNotMatch(own.stderr, /did not write/);
+  assert.match(own.stderr, /Wrote Pay\.map\.mjs/);
+});
+
 test("statechart.mjs exits 2 and names a helper script that cannot start", () => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-"));
   writeFileSync(join(dir, "notes-app.mmd"), fixture("sync.mmd"));

From 68bbd507b27bafb72f350ffadbfa6333f7f12d2e Mon Sep 17 00:00:00 2001
From: kam-hak <kah411@pitt.edu>
Date: Fri, 23 Oct 2026 13:46:31 -0400
Subject: [PATCH 2/5] test(statechart): cover unrecorded TLC files and reruns

---
 .../scripts/test/statechart.test.mjs          | 73 +++++++++++++++++++
 1 file changed, 73 insertions(+)

diff --git a/pstack/skills/statechart/scripts/test/statechart.test.mjs b/pstack/skills/statechart/scripts/test/statechart.test.mjs
index 02f55e192..a5da8db5c 100644
--- a/pstack/skills/statechart/scripts/test/statechart.test.mjs
+++ b/pstack/skills/statechart/scripts/test/statechart.test.mjs
@@ -1587,6 +1587,49 @@ test("statechart.mjs refuses an output folder with foreign files under tlc/ or b
   assert.match(own.stderr, /Wrote Pay\.map\.mjs/);
 });
 
+test("statechart.mjs refuses unrecorded TLC files and invalid ownership records", () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  writeFileSync(join(dir, "tla2tools.jar"), "");
+  writeFileSync(join(dir, "Pay.tla"), "---- MODULE Pay ----\n====\n");
+  writeFileSync(join(dir, "Pay.cfg"), "SPECIFICATION Spec\n");
+  const env = { TLA2TOOLS: join(dir, "tla2tools.jar") };
+  const out = join(dir, "out");
+  const tlc = join(out, "tlc");
+  for (const name of ["owner-notes.cfg", "owner-notes.out", "owner-notes.dot", "Checkout-backup.cfg"]) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, "Checkout.cfg"), "generated\n");
+    writeFileSync(join(tlc, ".written.json"), '["Checkout.cfg"]\n');
+    writeFileSync(join(tlc, name), "mine\n");
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.ok(r.stderr.includes(`tlc/${name}`), r.stderr);
+    assert.equal(readFileSync(join(tlc, name), "utf8"), "mine\n");
+    rmSync(out, { recursive: true });
+  }
+  for (const record of [null, "{", "{}", '["Pay.cfg", 1]']) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, "Pay.cfg"), "kept\n");
+    if (record !== null) writeFileSync(join(tlc, ".written.json"), record);
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.match(r.stderr, /--out with a new folder/);
+    assert.equal(readFileSync(join(tlc, "Pay.cfg"), "utf8"), "kept\n");
+    rmSync(out, { recursive: true });
+  }
+  for (const kind of ["directory", "symlink"]) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, ".written.json"), '["Pay.cfg"]\n');
+    if (kind === "directory") mkdirSync(join(tlc, "Pay.cfg"));
+    else symlinkSync(join(dir, "Pay.cfg"), join(tlc, "Pay.cfg"));
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write: tlc\/Pay.cfg/);
+    rmSync(out, { recursive: true });
+  }
+});
+
 test("statechart.mjs exits 2 and names a helper script that cannot start", () => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-"));
   writeFileSync(join(dir, "notes-app.mmd"), fixture("sync.mmd"));
@@ -5895,6 +5938,36 @@ const writeLamp = (dir) => {
   return join(dir, "Lamp-statechart");
 };
 
+test("TLC reruns replace recorded files, remove old rule files, and preserve unrecorded files", needsTlc, () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  const out = writeLamp(dir);
+  const spec = readFileSync(join(dir, "Lamp.tla"), "utf8").replace(
+    "====",
+    "Safe == on \\in BOOLEAN\n====",
+  );
+  writeFileSync(join(dir, "Lamp.tla"), spec);
+  writeFileSync(join(dir, "Lamp.cfg"), "SPECIFICATION Spec\nINVARIANT Safe\n");
+  const run = () => node("statechart.mjs", ["from-spec", "Lamp.tla"], dir);
+  for (let i = 0; i < 2; i++) {
+    const r = run();
+    assert.equal(r.status, 0, r.stderr);
+    assert.ok(existsSync(join(out, "tlc", "Lamp-Safe.cfg")));
+  }
+  writeFileSync(join(dir, "Lamp.cfg"), "SPECIFICATION Spec\n");
+  const changed = run();
+  assert.equal(changed.status, 0, changed.stderr);
+  assert.equal(existsSync(join(out, "tlc", "Lamp-Safe.cfg")), false);
+  for (const name of ["owner-notes.cfg", "owner-notes.out", "owner-notes.dot", "Lamp-backup.cfg"]) {
+    const file = join(out, "tlc", name);
+    writeFileSync(file, "mine\n");
+    const r = run();
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.equal(readFileSync(file, "utf8"), "mine\n");
+    rmSync(file);
+  }
+});
+
 test("a rerun without --png removes the chart.png of an earlier run", needsTlc, () => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-"));
   const out = writeLamp(dir);

From ce8573e9d869c5a4e7382a3c6cff34845ef05ada Mon Sep 17 00:00:00 2001
From: kam-hak <kah411@pitt.edu>
Date: Fri, 23 Oct 2026 13:47:55 -0400
Subject: [PATCH 3/5] fix(statechart): record the TLC files each run writes

---
 .../statechart/scripts/statechart-help.mjs    |  3 +-
 .../skills/statechart/scripts/statechart.mjs  | 25 ++++--
 .../scripts/test/statechart.test.mjs          | 78 ++++++++++++++++++-
 .../statechart/scripts/statechart-help.mjs    |  3 +-
 .../skills/statechart/scripts/statechart.mjs  | 25 ++++--
 .../scripts/test/statechart.test.mjs          |  5 +-
 6 files changed, 121 insertions(+), 18 deletions(-)

diff --git a/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs b/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs
index 1a900fc51..638876da2 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs
@@ -143,7 +143,8 @@ const COMMON = `Both commands
                      files in a temporary folder, and then replaces the whole output folder with
                      it. When runs overlap, the output folder has the files of the run that
                      finished last. The command does not use an output folder that has files that
-                     it did not write. On a filesystem that cannot rename, the command copies the
+                     it did not write. Older output folders without tlc/.written.json need a new
+                     --out folder. On a filesystem that cannot rename, the command copies the
                      files into place, and overlapping runs can mix their files.
   --png              Also draw each chart as a PNG. The PNG section tells how.
   --theme NAME       The colors of each PNG: light, dark, or classic. Default: light. It needs
diff --git a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
index ff02115b7..6bf5faf37 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
@@ -548,6 +548,8 @@ function render(charts, { lib, theme }, shown) {
 function finish({ work, out, inputs }, { files, charts }, ok, renderer) {
   unchanged(inputs, out);
   const pngs = renderer ? render(charts, renderer, published(work, out)) : [];
+  const tlc = path.join(work, "tlc");
+  fs.writeFileSync(path.join(tlc, WRITTEN), `${JSON.stringify(fs.readdirSync(tlc))}\n`);
   publish(work, out, inputs);
   const written = [...charts, ...pngs, files.stories, files.summary]
     .map((f) => path.basename(f))
@@ -578,21 +580,30 @@ function renderFile(input, flags, { lib, theme }) {
 
 const published = (work, out) => (file) => rel(path.join(out, path.relative(work, file)));
 
-// Files a run writes at the top of its output folder, and inside tlc/. Only a regular file with one
-// of these names is the run's own; a folder (or a link) under an owned name is not, and neither is
-// anything nested under tlc/ that TLC or this script did not write. publish() removes the previous
-// folder whole, so everything it holds must be ours.
 const OWN =
   /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|\.DS_Store)$/;
-const OWN_TLC = /^([^/]+\.(cfg|out|dot)|regions-(proof|all)\.mmd)$/;
+const WRITTEN = ".written.json";
+
+function foreignTlc(dir) {
+  let written;
+  try {
+    written = JSON.parse(fs.readFileSync(path.join(dir, WRITTEN), "utf8"));
+  } catch {}
+  const own = new Set([".DS_Store"]);
+  if (Array.isArray(written) && written.every((f) => typeof f === "string"))
+    for (const f of [WRITTEN, ...written]) own.add(f);
+  return fs
+    .readdirSync(dir, { withFileTypes: true })
+    .filter((g) => !g.isFile() || !own.has(g.name))
+    .map((g) => `tlc/${g.name}`);
+}
 
 function foreign(dir) {
   try {
     const found = [];
     for (const entry of fs.readdirSync(dir, { withFileTypes: true })) {
       if (entry.name === "tlc" && entry.isDirectory()) {
-        for (const inner of fs.readdirSync(path.join(dir, "tlc"), { withFileTypes: true }))
-          if (!(inner.isFile() && OWN_TLC.test(inner.name))) found.push(`tlc/${inner.name}`);
+        found.push(...foreignTlc(path.join(dir, "tlc")));
       } else if (!(entry.isFile() && OWN.test(entry.name))) found.push(entry.name);
     }
     return found.sort();
diff --git a/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs b/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
index 02f55e192..988cfe0c8 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
@@ -1554,6 +1554,7 @@ test("statechart.mjs refuses an output folder with foreign files under tlc/ or b
   // A user's file inside the owned tlc/ folder.
   mkdirSync(join(dir, "nested", "tlc"), { recursive: true });
   writeFileSync(join(dir, "nested", "tlc", "Pay.out"), "");
+  writeFileSync(join(dir, "nested", "tlc", ".written.json"), '["Pay.out"]\n');
   writeFileSync(join(dir, "nested", "tlc", "notes.md"), "mine\n");
   refused("nested", "tlc/notes.md");
   assert.equal(readFileSync(join(dir, "nested", "tlc", "notes.md"), "utf8"), "mine\n");
@@ -1579,14 +1580,59 @@ test("statechart.mjs refuses an output folder with foreign files under tlc/ or b
   mkdirSync(join(dir, "own", "tlc"), { recursive: true });
   for (const f of ["chart.mmd", "stories.md", "summary.json", ".DS_Store", "bug-1.png"])
     writeFileSync(join(dir, "own", f), "");
-  for (const f of ["Pay.cfg", "Pay.out", "Pay.dot", "Pay-Safe.cfg", "regions-proof.mmd"])
+  const ownTlc = ["Pay.cfg", "Pay.out", "Pay.dot", "Pay-Safe.cfg", "regions-proof.mmd"];
+  for (const f of ownTlc)
     writeFileSync(join(dir, "own", "tlc", f), "");
+  writeFileSync(join(dir, "own", "tlc", ".written.json"), JSON.stringify(ownTlc));
   // The run gets past the ownership check and stops at the next step, the missing mapping.
   const own = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", "own"], dir, env);
   assert.doesNotMatch(own.stderr, /did not write/);
   assert.match(own.stderr, /Wrote Pay\.map\.mjs/);
 });
 
+test("statechart.mjs refuses unrecorded TLC files and invalid ownership records", () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  writeFileSync(join(dir, "tla2tools.jar"), "");
+  writeFileSync(join(dir, "Pay.tla"), "---- MODULE Pay ----\n====\n");
+  writeFileSync(join(dir, "Pay.cfg"), "SPECIFICATION Spec\n");
+  const env = { TLA2TOOLS: join(dir, "tla2tools.jar") };
+  const out = join(dir, "out");
+  const tlc = join(out, "tlc");
+  for (const name of ["owner-notes.cfg", "owner-notes.out", "owner-notes.dot", "Checkout-backup.cfg"]) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, "Checkout.cfg"), "generated\n");
+    writeFileSync(join(tlc, ".written.json"), '["Checkout.cfg"]\n');
+    writeFileSync(join(tlc, name), "mine\n");
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.ok(r.stderr.includes(`tlc/${name}`), r.stderr);
+    assert.equal(readFileSync(join(tlc, name), "utf8"), "mine\n");
+    rmSync(out, { recursive: true });
+  }
+  for (const record of [null, "{", "{}", '["Pay.cfg", 1]']) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, "Pay.cfg"), "kept\n");
+    if (record !== null) writeFileSync(join(tlc, ".written.json"), record);
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.match(r.stderr, /--out with a new folder/);
+    assert.equal(readFileSync(join(tlc, "Pay.cfg"), "utf8"), "kept\n");
+    rmSync(out, { recursive: true });
+  }
+  for (const kind of ["directory", "symlink"]) {
+    mkdirSync(tlc, { recursive: true });
+    writeFileSync(join(tlc, ".written.json"), '["Pay.cfg"]\n');
+    if (kind === "directory") mkdirSync(join(tlc, "Pay.cfg"));
+    else symlinkSync(join(dir, "Pay.cfg"), join(tlc, "Pay.cfg"));
+    const r = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write: tlc\/Pay.cfg/);
+    rmSync(out, { recursive: true });
+  }
+});
+
 test("statechart.mjs exits 2 and names a helper script that cannot start", () => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-"));
   writeFileSync(join(dir, "notes-app.mmd"), fixture("sync.mmd"));
@@ -5895,6 +5941,36 @@ const writeLamp = (dir) => {
   return join(dir, "Lamp-statechart");
 };
 
+test("TLC reruns replace recorded files, remove old rule files, and preserve unrecorded files", needsTlc, () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  const out = writeLamp(dir);
+  const spec = readFileSync(join(dir, "Lamp.tla"), "utf8").replace(
+    "====",
+    "Safe == on \\in BOOLEAN\n====",
+  );
+  writeFileSync(join(dir, "Lamp.tla"), spec);
+  writeFileSync(join(dir, "Lamp.cfg"), "SPECIFICATION Spec\nINVARIANT Safe\n");
+  const run = () => node("statechart.mjs", ["from-spec", "Lamp.tla"], dir);
+  for (let i = 0; i < 2; i++) {
+    const r = run();
+    assert.equal(r.status, 0, r.stderr);
+    assert.ok(existsSync(join(out, "tlc", "Lamp-Safe.cfg")));
+  }
+  writeFileSync(join(dir, "Lamp.cfg"), "SPECIFICATION Spec\n");
+  const changed = run();
+  assert.equal(changed.status, 0, changed.stderr);
+  assert.equal(existsSync(join(out, "tlc", "Lamp-Safe.cfg")), false);
+  for (const name of ["owner-notes.cfg", "owner-notes.out", "owner-notes.dot", "Lamp-backup.cfg"]) {
+    const file = join(out, "tlc", name);
+    writeFileSync(file, "mine\n");
+    const r = run();
+    assert.equal(r.status, 2, r.stderr);
+    assert.match(r.stderr, /did not write/);
+    assert.equal(readFileSync(file, "utf8"), "mine\n");
+    rmSync(file);
+  }
+});
+
 test("a rerun without --png removes the chart.png of an earlier run", needsTlc, () => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-"));
   const out = writeLamp(dir);
diff --git a/pstack/skills/statechart/scripts/statechart-help.mjs b/pstack/skills/statechart/scripts/statechart-help.mjs
index 1a900fc51..638876da2 100644
--- a/pstack/skills/statechart/scripts/statechart-help.mjs
+++ b/pstack/skills/statechart/scripts/statechart-help.mjs
@@ -143,7 +143,8 @@ const COMMON = `Both commands
                      files in a temporary folder, and then replaces the whole output folder with
                      it. When runs overlap, the output folder has the files of the run that
                      finished last. The command does not use an output folder that has files that
-                     it did not write. On a filesystem that cannot rename, the command copies the
+                     it did not write. Older output folders without tlc/.written.json need a new
+                     --out folder. On a filesystem that cannot rename, the command copies the
                      files into place, and overlapping runs can mix their files.
   --png              Also draw each chart as a PNG. The PNG section tells how.
   --theme NAME       The colors of each PNG: light, dark, or classic. Default: light. It needs
diff --git a/pstack/skills/statechart/scripts/statechart.mjs b/pstack/skills/statechart/scripts/statechart.mjs
index ff02115b7..6bf5faf37 100644
--- a/pstack/skills/statechart/scripts/statechart.mjs
+++ b/pstack/skills/statechart/scripts/statechart.mjs
@@ -548,6 +548,8 @@ function render(charts, { lib, theme }, shown) {
 function finish({ work, out, inputs }, { files, charts }, ok, renderer) {
   unchanged(inputs, out);
   const pngs = renderer ? render(charts, renderer, published(work, out)) : [];
+  const tlc = path.join(work, "tlc");
+  fs.writeFileSync(path.join(tlc, WRITTEN), `${JSON.stringify(fs.readdirSync(tlc))}\n`);
   publish(work, out, inputs);
   const written = [...charts, ...pngs, files.stories, files.summary]
     .map((f) => path.basename(f))
@@ -578,21 +580,30 @@ function renderFile(input, flags, { lib, theme }) {
 
 const published = (work, out) => (file) => rel(path.join(out, path.relative(work, file)));
 
-// Files a run writes at the top of its output folder, and inside tlc/. Only a regular file with one
-// of these names is the run's own; a folder (or a link) under an owned name is not, and neither is
-// anything nested under tlc/ that TLC or this script did not write. publish() removes the previous
-// folder whole, so everything it holds must be ours.
 const OWN =
   /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|\.DS_Store)$/;
-const OWN_TLC = /^([^/]+\.(cfg|out|dot)|regions-(proof|all)\.mmd)$/;
+const WRITTEN = ".written.json";
+
+function foreignTlc(dir) {
+  let written;
+  try {
+    written = JSON.parse(fs.readFileSync(path.join(dir, WRITTEN), "utf8"));
+  } catch {}
+  const own = new Set([".DS_Store"]);
+  if (Array.isArray(written) && written.every((f) => typeof f === "string"))
+    for (const f of [WRITTEN, ...written]) own.add(f);
+  return fs
+    .readdirSync(dir, { withFileTypes: true })
+    .filter((g) => !g.isFile() || !own.has(g.name))
+    .map((g) => `tlc/${g.name}`);
+}
 
 function foreign(dir) {
   try {
     const found = [];
     for (const entry of fs.readdirSync(dir, { withFileTypes: true })) {
       if (entry.name === "tlc" && entry.isDirectory()) {
-        for (const inner of fs.readdirSync(path.join(dir, "tlc"), { withFileTypes: true }))
-          if (!(inner.isFile() && OWN_TLC.test(inner.name))) found.push(`tlc/${inner.name}`);
+        found.push(...foreignTlc(path.join(dir, "tlc")));
       } else if (!(entry.isFile() && OWN.test(entry.name))) found.push(entry.name);
     }
     return found.sort();
diff --git a/pstack/skills/statechart/scripts/test/statechart.test.mjs b/pstack/skills/statechart/scripts/test/statechart.test.mjs
index a5da8db5c..988cfe0c8 100644
--- a/pstack/skills/statechart/scripts/test/statechart.test.mjs
+++ b/pstack/skills/statechart/scripts/test/statechart.test.mjs
@@ -1554,6 +1554,7 @@ test("statechart.mjs refuses an output folder with foreign files under tlc/ or b
   // A user's file inside the owned tlc/ folder.
   mkdirSync(join(dir, "nested", "tlc"), { recursive: true });
   writeFileSync(join(dir, "nested", "tlc", "Pay.out"), "");
+  writeFileSync(join(dir, "nested", "tlc", ".written.json"), '["Pay.out"]\n');
   writeFileSync(join(dir, "nested", "tlc", "notes.md"), "mine\n");
   refused("nested", "tlc/notes.md");
   assert.equal(readFileSync(join(dir, "nested", "tlc", "notes.md"), "utf8"), "mine\n");
@@ -1579,8 +1580,10 @@ test("statechart.mjs refuses an output folder with foreign files under tlc/ or b
   mkdirSync(join(dir, "own", "tlc"), { recursive: true });
   for (const f of ["chart.mmd", "stories.md", "summary.json", ".DS_Store", "bug-1.png"])
     writeFileSync(join(dir, "own", f), "");
-  for (const f of ["Pay.cfg", "Pay.out", "Pay.dot", "Pay-Safe.cfg", "regions-proof.mmd"])
+  const ownTlc = ["Pay.cfg", "Pay.out", "Pay.dot", "Pay-Safe.cfg", "regions-proof.mmd"];
+  for (const f of ownTlc)
     writeFileSync(join(dir, "own", "tlc", f), "");
+  writeFileSync(join(dir, "own", "tlc", ".written.json"), JSON.stringify(ownTlc));
   // The run gets past the ownership check and stops at the next step, the missing mapping.
   const own = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", "own"], dir, env);
   assert.doesNotMatch(own.stderr, /did not write/);

From b4f0c6eebfc68a549e3e8d52353bd6761f6c138d Mon Sep 17 00:00:00 2001
From: Dean Rie <deanalexrie@gmail.com>
Date: Sat, 24 Oct 2026 12:47:06 +0300
Subject: [PATCH 4/5] fix(statechart): record TLC files below role folders, not
 only at the top of tlc/

#791 moved a comparing run's TLC files into tlc/fixed/ or tlc/against/. A
record of the top-level names alone would list the folder, and the next
run would then report the folder as foreign and refuse. The record now
holds every regular file under tlc/ as a relative path, and the check
walks the same way: a folder is the run's own only while it holds
something recorded, and a file inside it is reported by its full path
(tlc/fixed/Pay-backup.cfg).
---
 .../skills/statechart/scripts/statechart.mjs  | 41 +++++++++++++++----
 .../scripts/test/statechart.test.mjs          | 15 +++++++
 .../skills/statechart/scripts/statechart.mjs  | 41 +++++++++++++++----
 .../scripts/test/statechart.test.mjs          | 15 +++++++
 4 files changed, 98 insertions(+), 14 deletions(-)

diff --git a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
index 6bf5faf37..fb1696ab9 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs
@@ -549,7 +549,7 @@ function finish({ work, out, inputs }, { files, charts }, ok, renderer) {
   unchanged(inputs, out);
   const pngs = renderer ? render(charts, renderer, published(work, out)) : [];
   const tlc = path.join(work, "tlc");
-  fs.writeFileSync(path.join(tlc, WRITTEN), `${JSON.stringify(fs.readdirSync(tlc))}\n`);
+  fs.writeFileSync(path.join(tlc, WRITTEN), `${JSON.stringify(filesUnder(tlc))}\n`);
   publish(work, out, inputs);
   const written = [...charts, ...pngs, files.stories, files.summary]
     .map((f) => path.basename(f))
@@ -584,18 +584,45 @@ const OWN =
   /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|\.DS_Store)$/;
 const WRITTEN = ".written.json";
 
+// The regular files under `dir`, as paths relative to it with / separators, in a stable order.
+// A comparing run writes into tlc/fixed/ or tlc/against/, so the record has to reach below the
+// first level.
+function filesUnder(dir, prefix = "") {
+  const found = [];
+  for (const entry of fs.readdirSync(dir, { withFileTypes: true }).sort((a, b) =>
+    a.name.localeCompare(b.name),
+  )) {
+    const at = `${prefix}${entry.name}`;
+    if (entry.isDirectory()) found.push(...filesUnder(path.join(dir, entry.name), `${at}/`));
+    else if (entry.isFile() && at !== WRITTEN) found.push(at);
+  }
+  return found;
+}
+
+// Everything under tlc/ that the previous run did not record. Without a valid record every entry
+// is foreign: an output folder from before the record existed needs a new --out folder, which is
+// cheaper than guessing which of its files were the user's.
 function foreignTlc(dir) {
   let written;
   try {
     written = JSON.parse(fs.readFileSync(path.join(dir, WRITTEN), "utf8"));
   } catch {}
-  const own = new Set([".DS_Store"]);
+  const own = new Set([".DS_Store", WRITTEN]);
   if (Array.isArray(written) && written.every((f) => typeof f === "string"))
-    for (const f of [WRITTEN, ...written]) own.add(f);
-  return fs
-    .readdirSync(dir, { withFileTypes: true })
-    .filter((g) => !g.isFile() || !own.has(g.name))
-    .map((g) => `tlc/${g.name}`);
+    for (const f of written) own.add(f);
+  const found = [];
+  const walk = (at, prefix) => {
+    for (const entry of fs.readdirSync(at, { withFileTypes: true })) {
+      const name = `${prefix}${entry.name}`;
+      if (entry.isDirectory()) {
+        // A folder is the run's own only when it holds something the run recorded.
+        if ([...own].some((f) => f.startsWith(`${name}/`))) walk(path.join(at, entry.name), `${name}/`);
+        else found.push(`tlc/${name}`);
+      } else if (!(entry.isFile() && own.has(name))) found.push(`tlc/${name}`);
+    }
+  };
+  walk(dir, "");
+  return found;
 }
 
 function foreign(dir) {
diff --git a/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs b/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
index 988cfe0c8..539e81850 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/test/statechart.test.mjs
@@ -1621,6 +1621,21 @@ test("statechart.mjs refuses unrecorded TLC files and invalid ownership records"
     assert.equal(readFileSync(join(tlc, "Pay.cfg"), "utf8"), "kept\n");
     rmSync(out, { recursive: true });
   }
+  // A comparing run writes into tlc/fixed/ or tlc/against/. Recorded files there pass; a file the
+  // record does not name, or a folder with nothing recorded in it, is reported by its full path.
+  mkdirSync(join(tlc, "fixed"), { recursive: true });
+  writeFileSync(join(tlc, "Pay.cfg"), "generated\n");
+  writeFileSync(join(tlc, "fixed", "Pay.cfg"), "generated\n");
+  writeFileSync(join(tlc, ".written.json"), '["Pay.cfg", "fixed/Pay.cfg"]\n');
+  const nested = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+  assert.doesNotMatch(nested.stderr, /did not write/, nested.stderr);
+  writeFileSync(join(tlc, "fixed", "Pay-backup.cfg"), "mine\n");
+  mkdirSync(join(tlc, "scratch"));
+  const nestedForeign = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+  assert.equal(nestedForeign.status, 2, nestedForeign.stderr);
+  assert.match(nestedForeign.stderr, /2 files that this command did not write, such as tlc\/fixed\/Pay-backup\.cfg/);
+  assert.equal(readFileSync(join(tlc, "fixed", "Pay-backup.cfg"), "utf8"), "mine\n");
+  rmSync(out, { recursive: true });
   for (const kind of ["directory", "symlink"]) {
     mkdirSync(tlc, { recursive: true });
     writeFileSync(join(tlc, ".written.json"), '["Pay.cfg"]\n');
diff --git a/pstack/skills/statechart/scripts/statechart.mjs b/pstack/skills/statechart/scripts/statechart.mjs
index 6bf5faf37..fb1696ab9 100644
--- a/pstack/skills/statechart/scripts/statechart.mjs
+++ b/pstack/skills/statechart/scripts/statechart.mjs
@@ -549,7 +549,7 @@ function finish({ work, out, inputs }, { files, charts }, ok, renderer) {
   unchanged(inputs, out);
   const pngs = renderer ? render(charts, renderer, published(work, out)) : [];
   const tlc = path.join(work, "tlc");
-  fs.writeFileSync(path.join(tlc, WRITTEN), `${JSON.stringify(fs.readdirSync(tlc))}\n`);
+  fs.writeFileSync(path.join(tlc, WRITTEN), `${JSON.stringify(filesUnder(tlc))}\n`);
   publish(work, out, inputs);
   const written = [...charts, ...pngs, files.stories, files.summary]
     .map((f) => path.basename(f))
@@ -584,18 +584,45 @@ const OWN =
   /^((chart|bug-\d+(-developer|-layered)?)\.(mmd|png)|stories\.md|summary\.json|\.DS_Store)$/;
 const WRITTEN = ".written.json";
 
+// The regular files under `dir`, as paths relative to it with / separators, in a stable order.
+// A comparing run writes into tlc/fixed/ or tlc/against/, so the record has to reach below the
+// first level.
+function filesUnder(dir, prefix = "") {
+  const found = [];
+  for (const entry of fs.readdirSync(dir, { withFileTypes: true }).sort((a, b) =>
+    a.name.localeCompare(b.name),
+  )) {
+    const at = `${prefix}${entry.name}`;
+    if (entry.isDirectory()) found.push(...filesUnder(path.join(dir, entry.name), `${at}/`));
+    else if (entry.isFile() && at !== WRITTEN) found.push(at);
+  }
+  return found;
+}
+
+// Everything under tlc/ that the previous run did not record. Without a valid record every entry
+// is foreign: an output folder from before the record existed needs a new --out folder, which is
+// cheaper than guessing which of its files were the user's.
 function foreignTlc(dir) {
   let written;
   try {
     written = JSON.parse(fs.readFileSync(path.join(dir, WRITTEN), "utf8"));
   } catch {}
-  const own = new Set([".DS_Store"]);
+  const own = new Set([".DS_Store", WRITTEN]);
   if (Array.isArray(written) && written.every((f) => typeof f === "string"))
-    for (const f of [WRITTEN, ...written]) own.add(f);
-  return fs
-    .readdirSync(dir, { withFileTypes: true })
-    .filter((g) => !g.isFile() || !own.has(g.name))
-    .map((g) => `tlc/${g.name}`);
+    for (const f of written) own.add(f);
+  const found = [];
+  const walk = (at, prefix) => {
+    for (const entry of fs.readdirSync(at, { withFileTypes: true })) {
+      const name = `${prefix}${entry.name}`;
+      if (entry.isDirectory()) {
+        // A folder is the run's own only when it holds something the run recorded.
+        if ([...own].some((f) => f.startsWith(`${name}/`))) walk(path.join(at, entry.name), `${name}/`);
+        else found.push(`tlc/${name}`);
+      } else if (!(entry.isFile() && own.has(name))) found.push(`tlc/${name}`);
+    }
+  };
+  walk(dir, "");
+  return found;
 }
 
 function foreign(dir) {
diff --git a/pstack/skills/statechart/scripts/test/statechart.test.mjs b/pstack/skills/statechart/scripts/test/statechart.test.mjs
index 988cfe0c8..539e81850 100644
--- a/pstack/skills/statechart/scripts/test/statechart.test.mjs
+++ b/pstack/skills/statechart/scripts/test/statechart.test.mjs
@@ -1621,6 +1621,21 @@ test("statechart.mjs refuses unrecorded TLC files and invalid ownership records"
     assert.equal(readFileSync(join(tlc, "Pay.cfg"), "utf8"), "kept\n");
     rmSync(out, { recursive: true });
   }
+  // A comparing run writes into tlc/fixed/ or tlc/against/. Recorded files there pass; a file the
+  // record does not name, or a folder with nothing recorded in it, is reported by its full path.
+  mkdirSync(join(tlc, "fixed"), { recursive: true });
+  writeFileSync(join(tlc, "Pay.cfg"), "generated\n");
+  writeFileSync(join(tlc, "fixed", "Pay.cfg"), "generated\n");
+  writeFileSync(join(tlc, ".written.json"), '["Pay.cfg", "fixed/Pay.cfg"]\n');
+  const nested = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+  assert.doesNotMatch(nested.stderr, /did not write/, nested.stderr);
+  writeFileSync(join(tlc, "fixed", "Pay-backup.cfg"), "mine\n");
+  mkdirSync(join(tlc, "scratch"));
+  const nestedForeign = node("statechart.mjs", ["from-spec", "Pay.tla", "--out", out], dir, env);
+  assert.equal(nestedForeign.status, 2, nestedForeign.stderr);
+  assert.match(nestedForeign.stderr, /2 files that this command did not write, such as tlc\/fixed\/Pay-backup\.cfg/);
+  assert.equal(readFileSync(join(tlc, "fixed", "Pay-backup.cfg"), "utf8"), "mine\n");
+  rmSync(out, { recursive: true });
   for (const kind of ["directory", "symlink"]) {
     mkdirSync(tlc, { recursive: true });
     writeFileSync(join(tlc, ".written.json"), '["Pay.cfg"]\n');

From 02ba3740693474743ac5530a2a28001fda2e905f Mon Sep 17 00:00:00 2001
From: Dean Rie <deanalexrie@gmail.com>
Date: Sun, 25 Oct 2026 20:57:21 +0300
Subject: [PATCH 5/5] docs(statechart): the regenerate loop stops on a rule
 change, not on any chart change

---
 .../claude-code/skills/statechart/scripts/statechart-help.mjs  | 3 ++-
 pstack/skills/statechart/scripts/statechart-help.mjs           | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs b/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs
index 638876da2..54e22875b 100644
--- a/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs
+++ b/harness/pstack/claude-code/skills/statechart/scripts/statechart-help.mjs
@@ -280,7 +280,8 @@ Reading a chart
 
 Regenerate
   List every rule that is known to break with --expect-broken, the goals and the known bugs. Each
-  run then exits 0 until a rule changes, so one script rebuilds every chart and stops on any change:
+  run then exits 0 until a rule changes, so one script rebuilds every chart and stops when a rule
+  breaks or heals (a chart that only redraws does not stop it):
     set -e
     node statechart.mjs from-spec Code.tla --against Agreed.tla --expect-broken NoLostUpload --png
   A run that leaves a broken rule out of --expect-broken exits 1, and set -e stops the script there.
diff --git a/pstack/skills/statechart/scripts/statechart-help.mjs b/pstack/skills/statechart/scripts/statechart-help.mjs
index 638876da2..54e22875b 100644
--- a/pstack/skills/statechart/scripts/statechart-help.mjs
+++ b/pstack/skills/statechart/scripts/statechart-help.mjs
@@ -280,7 +280,8 @@ Reading a chart
 
 Regenerate
   List every rule that is known to break with --expect-broken, the goals and the known bugs. Each
-  run then exits 0 until a rule changes, so one script rebuilds every chart and stops on any change:
+  run then exits 0 until a rule changes, so one script rebuilds every chart and stops when a rule
+  breaks or heals (a chart that only redraws does not stop it):
     set -e
     node statechart.mjs from-spec Code.tla --against Agreed.tla --expect-broken NoLostUpload --png
   A run that leaves a broken rule out of --expect-broken exits 1, and set -e stops the script there.