fix(pstack): write non-ASCII chart captions as strings TLC can parse

pstack/skills/statechart/scripts/chart-to-tla.mjs

@@ -43,7 +43,9 @@ function ident(words, lower) {
   taken.add(unique);
   return unique;
 }
-const str = (s) => `"${s.replaceAll("\\", "\\\\").replaceAll('"', '\\"')}"`;
+// SANY reads only ASCII in a string, so other characters go in as Mermaid's #code; entities.
+const ascii = (s) => s.replace(/[^\x00-\x7f]/gu, (c) => `#${c.codePointAt(0)};`);
+const str = (s) => `"${ascii(s).replaceAll("\\", "\\\\").replaceAll('"', '\\"')}"`;
 const set = (xs) => `{${[...xs].map(str).join(", ")}}`;
 
 const vars = Object.entries(regions).map(([name, r]) => {
@@ -184,14 +186,18 @@ const rules = ["TypeOK", ...invariants];
 const cfg = ["SPECIFICATION Spec", ...rules.map((r) => `INVARIANT ${r}`), ""];
 
 const labels = Object.fromEntries(actions.map((a) => [a.name, a.label]));
+const captions = Object.fromEntries(
+  vars.flatMap((x) => [...x.states].filter((s) => ascii(s) !== s).map((s) => [ascii(s), s])),
+);
 const map = [
   `// Generated by chart-to-tla.mjs from ${path.basename(args.chart)}. Reader states are the chart's own states.`,
   `export const regions = ${JSON.stringify(vars.map((x) => x.v))};`,
   `const LABELS = ${JSON.stringify(labels, null, "\t")};`,
+  `const CAPTIONS = ${JSON.stringify(captions, null, "\t")};`,
   "",
   "// The actions the reader takes. facts.settled needs them. Add cause() and detail() as the spec grows.",
   "export const readerActions = [];",
-  'export const state = (v) => regions.map((r) => v[r]).join(" | ");',
+  'export const state = (v) => regions.map((r) => CAPTIONS[v[r]] ?? v[r]).join(" | ");',
   "export const step = (action) => LABELS[action] ?? action;",
   "",
 ];

pstack/skills/statechart/scripts/test/chart-to-tla-ascii.test.mjs

@@ -0,0 +1,65 @@
+import assert from "node:assert/strict";
+import { spawnSync } from "node:child_process";
+import { mkdtempSync, readFileSync, writeFileSync } from "node:fs";
+import { tmpdir } from "node:os";
+import { dirname, join } from "node:path";
+import { test } from "node:test";
+import { fileURLToPath, pathToFileURL } from "node:url";
+import { findTlc } from "../tlc-tools.mjs";
+
+const scripts = dirname(dirname(fileURLToPath(import.meta.url)));
+const node = (script, args, cwd) =>
+  spawnSync(process.execPath, [join(scripts, script), ...args], {
+    cwd,
+    encoding: "utf8",
+    timeout: 120_000,
+  });
+const tools = (() => {
+  try {
+    return findTlc();
+  } catch {
+    return null;
+  }
+})();
+
+const chart = `stateDiagram-v2
+  state "Waiting…" as W
+  state "Don’t pay" as D
+  state "Café 🎉" as C
+  [*] --> W
+  W --> D : you tap “Cancel”
+  D --> C : you retry
+  C --> W : you leave
+  %% never NeverCafe: Café 🎉 -- You never reach the café.
+`;
+
+test("chart-to-tla writes captions with typographic characters as ASCII strings, and the map reads them back", async () => {
+  const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+  writeFileSync(join(dir, "pay.mmd"), chart);
+  const r = node("chart-to-tla.mjs", ["pay.mmd", "--module", "Pay"], dir);
+  assert.equal(r.status, 0, r.stderr);
+  const spec = readFileSync(join(dir, "Pay.tla"), "utf8");
+  const strings = spec.match(/"(?:[^"\\\n]|\\.)*"/g);
+  assert.ok(strings.length > 0);
+  for (const s of strings) assert.match(s, /^[\x20-\x7e]*$/, `SANY cannot read ${s}`);
+  const mapping = await import(pathToFileURL(join(dir, "Pay.map.mjs")).href);
+  const read = new Set(strings.map((s) => mapping.state({ main: JSON.parse(s) })));
+  for (const caption of ["Waiting…", "Don’t pay", "Café 🎉"]) assert.ok(read.has(caption), caption);
+});
+
+test(
+  "from-chart checks a chart whose captions have typographic characters and draws it back unchanged",
+  { skip: tools ? false : "cannot find TLC" },
+  () => {
+    const dir = mkdtempSync(join(tmpdir(), "statechart-"));
+    writeFileSync(join(dir, "pay.mmd"), chart);
+    const r = node(
+      "statechart.mjs",
+      ["from-chart", "pay.mmd", "--expect-broken", "NeverCafe"],
+      dir,
+    );
+    assert.equal(r.status, 0, r.stdout + r.stderr);
+    assert.match(r.stdout, /^ {2}NeverCafe is broken \(expected\)\.$/m);
+    assert.match(r.stdout, /\nThe spec draws pay\.mmd back unchanged\.\n/);
+  },
+);