From 2babb8edcddb64ad379d1250351b9d3975310a55 Mon Sep 17 00:00:00 2001 From: Rudy Celekli Date: Sat, 24 Oct 2026 17:43:39 -0400 Subject: [PATCH] fix(pstack): write non-ASCII chart captions as strings TLC can parse --- .../statechart/scripts/chart-to-tla.mjs | 10 ++- .../scripts/test/chart-to-tla-ascii.test.mjs | 65 +++++++++++++++++++ .../statechart/scripts/chart-to-tla.mjs | 10 ++- .../scripts/test/chart-to-tla-ascii.test.mjs | 65 +++++++++++++++++++ 4 files changed, 146 insertions(+), 4 deletions(-) create mode 100644 harness/pstack/claude-code/skills/statechart/scripts/test/chart-to-tla-ascii.test.mjs create mode 100644 pstack/skills/statechart/scripts/test/chart-to-tla-ascii.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..574bfa771 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 @@ -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;", "", ]; diff --git a/harness/pstack/claude-code/skills/statechart/scripts/test/chart-to-tla-ascii.test.mjs b/harness/pstack/claude-code/skills/statechart/scripts/test/chart-to-tla-ascii.test.mjs new file mode 100644 index 000000000..90d6ee80e --- /dev/null +++ b/harness/pstack/claude-code/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/); + }, +); diff --git a/pstack/skills/statechart/scripts/chart-to-tla.mjs b/pstack/skills/statechart/scripts/chart-to-tla.mjs index 911c58698..574bfa771 100644 --- a/pstack/skills/statechart/scripts/chart-to-tla.mjs +++ b/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;", "", ]; diff --git a/pstack/skills/statechart/scripts/test/chart-to-tla-ascii.test.mjs b/pstack/skills/statechart/scripts/test/chart-to-tla-ascii.test.mjs new file mode 100644 index 000000000..90d6ee80e --- /dev/null +++ b/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/); + }, +);