From 2216b63446c21fd49daeb8adcc70e4ddba7120b5 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Thu, 22 Oct 2026 18:24:09 +0000 Subject: [PATCH] refactor(pstack): delete statechart comments that repeat the code, and rename helpers Deletes comments in the statechart scripts that say what a name or the code already says. Where a comment held a fact, a name or a shared constant holds it now: - splitComments is splitCommentsKeepingOffsets. - checkTlcOutput is tlcOutputWarning. - quote is escapeMermaidQuotes. - luminance is wcagRelativeLuminance. - declared in parseMermaid is declaredInRegion. - cited(from, to, above) takes { above }. - PRIMES_OR_UNCHANGED replaces two copies of one regex, in uncitedConditions and in the label map scaffold. The scaffold keeps the note that it lists a definition that only another action calls, though TLC names no step after it. Behavior does not change. Co-authored-by: lauren --- .../skills/statechart/scripts/lib.mjs | 43 +++++++------------ .../skills/statechart/scripts/statechart.mjs | 18 +++----- .../scripts/test/statechart.test.mjs | 22 +++++----- .../statechart/scripts/tlc-to-chart.mjs | 25 ++++++----- pstack/skills/statechart/scripts/lib.mjs | 43 +++++++------------ .../skills/statechart/scripts/statechart.mjs | 18 +++----- .../scripts/test/statechart.test.mjs | 22 +++++----- .../statechart/scripts/tlc-to-chart.mjs | 25 ++++++----- 8 files changed, 88 insertions(+), 128 deletions(-) diff --git a/harness/pstack/claude-code/skills/statechart/scripts/lib.mjs b/harness/pstack/claude-code/skills/statechart/scripts/lib.mjs index 7fad394df..49f1675bc 100644 --- a/harness/pstack/claude-code/skills/statechart/scripts/lib.mjs +++ b/harness/pstack/claude-code/skills/statechart/scripts/lib.mjs @@ -154,9 +154,7 @@ export function ruleSentences(tla) { export const tlaVariables = (code) => [...code.matchAll(/\bVARIABLES?\s+(\w+(?:\s*,\s*\w+)*)/g)].flatMap((m) => m[1].split(/\s*,\s*/)); -// Returns the code with comments blanked, and the comments with the code blanked, at the same -// offsets, so a line number means the same line in both. -function splitComments(text) { +function splitCommentsKeepingOffsets(text) { let code = ""; let notes = ""; let block = 0; @@ -206,11 +204,8 @@ const CITATION = /[\w./-]+\.[A-Za-z]\w*:\d+|#L\d+/; const DEPTH = { "(": 1, "[": 1, "{": 1, ")": -1, "]": -1, "}": -1 }; const LOOSER_THAN_AND = /^(\\\/|=>|<=>|~>|-\+->|\\equiv\b)/; const RUNS_TO_END = /^(\\[EA]|IF|LET|CASE|CHOOSE)\b/; +export const PRIMES_OR_UNCHANGED = /[\w)\]>}]'|\bUNCHANGED\b/; -// The conjuncts of a definition body, as [from, to) offsets: a bulleted /\ list, or a body that -// /\ joins outside brackets, after any leading \E x : . An IF, LET, CASE, CHOOSE, or quantifier -// runs to the end of its conjunct. null when an operator that binds looser than /\, such as \/ -// or =>, joins the body. function conjuncts(bare, from, to, lineStart) { const first = from + bare.slice(from, to).search(/\S/); if (first < from) return null; @@ -251,12 +246,8 @@ function conjuncts(bare, from, to, lineStart) { return [first, ...cuts.map((c) => c + 2)].map((a, i) => [a, cuts[i] ?? to]); } -// The enabling conditions of each action that wait on a variable the action does not change, -// and that no comment ties to a file and line. An action is a definition that primes a variable -// or has UNCHANGED. The comment sits on the condition's lines, or right above them when the -// condition does not start on the definition's line. export function uncitedConditions(text) { - const { code, notes } = splitComments(text); + const { code, notes } = splitCommentsKeepingOffsets(text); const bare = code.replace(/"(?:[^"\\\n]|\\.)*"/g, (s) => " ".repeat(s.length)); const variables = new Set(tlaVariables(bare)); const starts = [0, ...[...bare.matchAll(/\n/g)].map((m) => m.index + 1)]; @@ -289,7 +280,7 @@ export function uncitedConditions(text) { writes: [...body.matchAll(/(? m[1]) .filter((id) => variables.has(id)), - acts: /[\w)\]>}]'|\bUNCHANGED\b/.test(body), + acts: PRIMES_OR_UNCHANGED.test(body), calls: [...new Set(ids.filter((id) => defs.has(id)))], }; }; @@ -310,7 +301,7 @@ export function uncitedConditions(text) { } return out; }; - const cited = (from, to, above) => { + const cited = (from, to, { above }) => { for (let l = from; l <= to; l++) if (CITATION.test(lines.notes[l])) return true; for (let l = from - 1; above && !lines.bare[l].trim() && lines.notes[l].trim(); l--) if (CITATION.test(lines.notes[l])) return true; @@ -326,7 +317,7 @@ export function uncitedConditions(text) { if (part.acts || [...part.reads].every((v) => changes.has(v))) continue; const first = lineOf(a + bare.slice(a, b).search(/\S/)); const last = lineOf(a + bare.slice(a, b).trimEnd().length - 1); - if (cited(first, last, first > d.line)) continue; + if (cited(first, last, { above: first > d.line })) continue; found.push({ line: first + 1, action, @@ -434,9 +425,8 @@ export const BROKEN_PROPERTY = // With -continue, TLC prints "Model checking completed" even after broken invariants, and not // when it stopped early. TLC can also throw a Java exception of its own while it reports a state // that breaks a rule, and stop early. An error in the rule's formula throws one of TLC's own -// exceptions in place of java.*. Returns a warning for that crash, without the file name because -// the caller can move the file, and throws for other errors. -export function checkTlcOutput(text, file) { +// exceptions in place of java.*. +export function tlcOutputWarning(text, file) { const lines = text.split("\n"); const named = (re) => new Set(lines.map((l) => re.exec(l)?.[1]).filter(Boolean)); const broken = named(/^Error: Invariant (\S+) is violated/); @@ -514,8 +504,7 @@ const unwrap = (s) => .replace(/\s+/g, " ") .trim(); -// Mermaid ends a quoted state caption at the first ", so a caption writes " as #quot;. -export const quote = (s) => String(s).replaceAll('"', "#quot;"); +export const escapeMermaidQuotes = (s) => String(s).replaceAll('"', "#quot;"); export const LEGEND_ID = "legend"; export const FULL_LABELS = "%% labels in full"; @@ -628,15 +617,14 @@ export function parseMermaid(text) { "the chart has -- outside a composite; to make parallel regions, split one top-level composite with --", ); - // Ids are global, as in Mermaid: a transition may name a state declared inside another composite. function region(p) { const out = { states: new Set(), initial: new Set(), transitions: [] }; const info = new Map(); - const declared = new Set(); + const declaredInRegion = new Set(); (function collect(q) { for (const c of q.children) { if (c.name === LEGEND_ID) continue; - declared.add(c.name); + declaredInRegion.add(c.name); if (!c.leaf) for (const sub of c.parts) collect(sub); } })(p); @@ -650,8 +638,8 @@ export function parseMermaid(text) { const local = q.children.filter((c) => c.name !== LEGEND_ID); for (const t of q.transitions) { for (const end of [t.from, t.to]) { - if (end === "[*]" || declared.has(end)) continue; - declared.add(end); + if (end === "[*]" || declaredInRegion.has(end)) continue; + declaredInRegion.add(end); local.push({ name: end, leaf: true }); } } @@ -905,8 +893,7 @@ const rgb = (hex) => { const h = hex.length === 4 ? [...hex.slice(1)].map((c) => c + c).join("") : hex.slice(1); return [0, 2, 4].map((i) => parseInt(h.slice(i, i + 2), 16)); }; -// WCAG relative luminance: 0 for black, 1 for white. -function luminance(hex) { +function wcagRelativeLuminance(hex) { const [r, g, b] = rgb(hex).map((c) => { const s = c / 255; return s <= 0.03928 ? s / 12.92 : ((s + 0.055) / 1.055) ** 2.4; @@ -916,7 +903,7 @@ function luminance(hex) { export function groupColorProblem(color) { if (typeof color !== "string" || !/^#([0-9a-f]{3}|[0-9a-f]{6})$/i.test(color)) return 'is not "#rgb" or "#rrggbb"'; - if (luminance(color) < 0.5) return "is too dark for the status borders to show on it"; + if (wcagRelativeLuminance(color) < 0.5) return "is too dark for the status borders to show on it"; return null; } diff --git a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs index 685b60117..0ff4255c2 100644 --- a/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs +++ b/harness/pstack/claude-code/skills/statechart/scripts/statechart.mjs @@ -7,11 +7,12 @@ import process from "node:process"; import { fileURLToPath, pathToFileURL } from "node:url"; import { BROKEN_PROPERTY, - checkTlcOutput, findTlc, joinAnd, parseDot, + PRIMES_OR_UNCHANGED, tlaVariables, + tlcOutputWarning, uncitedConditions, } from "./lib.mjs"; @@ -346,7 +347,7 @@ function tlc(tools, spec, cfg, base, { dump, workers = "1" } = {}) { if (r.error) throw new CannotFinish(`cannot run TLC: ${r.error.message}`); fs.writeFileSync(`${base}.out`, r.stdout); try { - return { stdout: r.stdout, warning: checkTlcOutput(r.stdout, `${base}.out`) }; + return { stdout: r.stdout, warning: tlcOutputWarning(r.stdout, `${base}.out`) }; } catch (e) { throw new TlcStopped(e.message); } @@ -423,8 +424,6 @@ function check(tools, model, { work, out }, expected) { const said = (rule, broken) => ` ${rule} ${broken ? (expected.has(rule) ? "is broken (expected)" : "is broken") : "holds"}.`; const shown = (file) => rel(path.join(out, "tlc", path.basename(file))); - // With -continue TLC reports every bad state. The CONSTRAINT stops each path at its first bad - // state, so a rule that stays broken reports only the step that broke it, not every later state. const traces = rules.map((rule) => { const file = path.join(tlcDir, `${name}-${rule}`); const cfg = `${cfgWithoutRules}INVARIANT ${rule}\nCONSTRAINT ${rule}\n`; @@ -470,14 +469,13 @@ function rulesAsExpected(now, other, expected) { const SCAFFOLD = (name, spec) => { const text = withoutComments(spec); const vars = tlaVariables(text); - // TLC names each step after a definition that primes a variable or leaves one UNCHANGED. A - // definition that only another action calls is listed too, though TLC names no step after it. + // A definition that only another action calls is listed too, though TLC names no step after it. const actions = [ ...new Set( text .split(/\n(?=\S)/) .map((d) => /^(\w+)\s*(?:\([^)]*\))?\s*==([^]*)/.exec(d)) - .filter((d) => d && /[\w)\]>}]'|\bUNCHANGED\b/.test(d[2])) + .filter((d) => d && PRIMES_OR_UNCHANGED.test(d[2])) .map((d) => d[1]), ), ].sort(); @@ -732,7 +730,7 @@ const moved = (from, to, ...missed) => { if (!["ENOSYS", "EXDEV", "EISDIR"].includes(e.code)) throw e; } // Some filesystems, such as FUSE mounts, cannot rename a folder that has files. They fail with - // ENOSYS, or with EISDIR when the target exists. Copy, and keep rename's outcomes. + // ENOSYS, or with EISDIR when the target exists. if (!fs.existsSync(from) && missed.includes("ENOENT")) return false; if (fs.existsSync(to)) { if (fs.readdirSync(to).length && missed.includes("ENOTEMPTY")) return false; @@ -819,7 +817,6 @@ function secondModel(input, cfg, { fixed, against, label }) { } const [role, spec] = fixed ? ["fixed", fixed] : ["against", against]; const name = path.basename(input, ".tla"); - // TLC's output files are named after the spec, so a second model with the same name overwrites them. if (path.basename(spec, ".tla") === name) throw new CannotFinish( `${rel(spec)} needs its own file and module name, such as ${name}${fixed ? "Fixed" : "Agreed"}.tla.`, @@ -835,9 +832,6 @@ function warnUnchecked(now, other) { ); } -// The rule that each config beside the spec expects TLC to break, from the "\* expect:" and -// "\* module:" lines of each config. null when no config of the spec's -// module has an "\* expect:" line. function listedBreaks(spec) { const dir = path.dirname(spec); const files = fs.readdirSync(dir).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 28d1c3d96..72782e679 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 @@ -15,7 +15,6 @@ import { test } from "node:test"; import { setTimeout as sleep } from "node:timers/promises"; import { fileURLToPath } from "node:url"; import { - checkTlcOutput, findTlc, parseDot, parseMermaid, @@ -23,6 +22,7 @@ import { parseValue, ruleSentences, stateKey, + tlcOutputWarning, uncitedConditions, } from "../lib.mjs"; @@ -280,7 +280,7 @@ test("a rule broken by a start state is a counterexample of one state", () => { /\\ conn = "Offline" ${done}`; - assert.doesNotThrow(() => checkTlcOutput(text, "tlc.out")); + assert.doesNotThrow(() => tlcOutputWarning(text, "tlc.out")); assert.deepEqual(parseTraces(text), [ { invariant: "NeverSyncedWhileOffline", @@ -291,30 +291,30 @@ ${done}`; test("TLC output from a run that failed or stopped early is refused", () => { assert.doesNotThrow(() => - checkTlcOutput( + tlcOutputWarning( `Error: Invariant Small is violated.\nError: The behavior up to this point is:\nState 1: \nx = 0\n\n${done}`, "ok.out", ), ); assert.throws( () => - checkTlcOutput( + tlcOutputWarning( "Error: The invariant Nope specified in the configuration file\nis not defined in the specification.\n", "cfg.out", ), /cfg\.out: TLC stopped on an error that is not a broken rule/, ); assert.throws( - () => checkTlcOutput("Error: Parsing or semantic analysis failed.\n", "parse.out"), + () => tlcOutputWarning("Error: Parsing or semantic analysis failed.\n", "parse.out"), /not a broken rule/, ); assert.throws( - () => checkTlcOutput(evaluationError, "eval.out"), + () => tlcOutputWarning(evaluationError, "eval.out"), /TLC threw an unexpected exception/, ); assert.throws( () => - checkTlcOutput( + tlcOutputWarning( "Error: Invariant Small is violated.\nError: The behavior up to this point is:\nState 1: \nx = 0\n", "stopped.out", ), @@ -348,12 +348,12 @@ test("a rule that TLC finds broken before TLC throws a Java exception keeps its "Index 123 out of bounds for length 4", )}\n${stoppedEarly}`; assert.equal( - checkTlcOutput(oneWorker, "tlc.out"), + tlcOutputWarning(oneWorker, "tlc.out"), `TLC found that Small is broken, and then failed with ${aioobe}. TLC stopped before it checked every state, so the charts can miss states that break Small. The failure is in TLC, not in the rule. Do not weaken Small because of it. A smaller constant can let TLC finish.`, ); const workersInterleaved = `${tlcThrew("java.lang.RuntimeException", aioobe)}${smallBroken}${stoppedEarly}`; assert.match( - checkTlcOutput(workersInterleaved, "tlc.out"), + tlcOutputWarning(workersInterleaved, "tlc.out"), /failed with java\.lang\.ArrayIndexOutOfBoundsException: Index 123/, ); assert.deepEqual( @@ -362,7 +362,7 @@ test("a rule that TLC finds broken before TLC throws a Java exception keeps its ); assert.throws( () => - checkTlcOutput( + tlcOutputWarning( `${smallBroken}${tlcThrew("java.lang.RuntimeException", "util.Assert$TLCRuntimeException: Attempted to apply tuple")}${stoppedEarly}`, "formula.out", ), @@ -370,7 +370,7 @@ test("a rule that TLC finds broken before TLC throws a Java exception keeps its ); assert.throws( () => - checkTlcOutput( + tlcOutputWarning( `${tlcThrew("java.lang.ArrayIndexOutOfBoundsException", "Index 123 out of bounds for length 4")}${stoppedEarly}`, "never-broken.out", ), diff --git a/harness/pstack/claude-code/skills/statechart/scripts/tlc-to-chart.mjs b/harness/pstack/claude-code/skills/statechart/scripts/tlc-to-chart.mjs index 005c9ef7c..37ae46e33 100644 --- a/harness/pstack/claude-code/skills/statechart/scripts/tlc-to-chart.mjs +++ b/harness/pstack/claude-code/skills/statechart/scripts/tlc-to-chart.mjs @@ -8,8 +8,8 @@ import { GROUP_PALETTE, LEGEND_ID, PLAIN_FILL, - checkTlcOutput, compareCharts, + escapeMermaidQuotes, groupClassDef, groupColorProblem, isRecord, @@ -19,9 +19,9 @@ import { parseMermaid, parseTraces, productOf, - quote, ruleSentences, stateKey, + tlcOutputWarning, wrap, STATUS_CLASSES, } from "./lib.mjs"; @@ -523,7 +523,7 @@ function replaySecond(trace) { function readTraces(files, paths = []) { return files.flatMap((f) => { const text = fs.readFileSync(f, "utf8"); - const warning = checkTlcOutput(text, f); + const warning = tlcOutputWarning(text, f); if (warning) console.error(`${f}: ${warning}`); return parseTraces(text).map((t) => ({ ...t, @@ -531,7 +531,6 @@ function readTraces(files, paths = []) { })); }); } -// With -continue, TLC reports every bad state, including states after the first bad one. function firstBad(raw) { const badStates = new Map(); for (const t of raw) { @@ -827,8 +826,6 @@ const groupCounts = (drawn) => })) .filter((g) => g.states > 0); -// Mermaid shrinks a chart to the page width unless useMaxWidth is false, and rewraps labels that -// wrap() already wrapped unless markdownAutoWrap is false. const frontMatter = (title) => [ "---", ...(title ? [`title: ${JSON.stringify(title)}`] : []), @@ -861,7 +858,7 @@ function head(drawn) { } else for (const c of STATUS_CLASSES) out.push(` ${c}`); if (legend.length) { out.push(` state "Legend" as ${LEGEND_ID} {`); - for (const [id, text] of legend) out.push(` state "${quote(text)}" as ${id}`); + for (const [id, text] of legend) out.push(` state "${escapeMermaidQuotes(text)}" as ${id}`); out.push(" }"); for (const [id, , c] of legend) out.push(` class ${id} ${c}`); } @@ -899,7 +896,7 @@ function regionsChart({ states, starts, edges, classes, proofPath, allPath }) { const proof = [ ...frontMatter(), "stateDiagram-v2", - ...[...ids].map(([s, id]) => ` state "${quote(s)}" as ${id}`), + ...[...ids].map(([s, id]) => ` state "${escapeMermaidQuotes(s)}" as ${id}`), ...[...flat.Main.initial].map((s) => ` [*] --> ${ids.get(s)}`), ...steps.map((s) => ` ${ids.get(bar(s.from))} --> ${ids.get(bar(s.to))} : ${s.label}`), ]; @@ -978,10 +975,11 @@ function regionsChart({ states, starts, edges, classes, proofPath, allPath }) { if (i) out.push(" --"); const name = mapping.regionNames?.[i]; const pad = name ? " " : " "; - if (name) out.push(` state "${quote(wrap(name))}" as region${i} {`); + if (name) out.push(` state "${escapeMermaidQuotes(wrap(name))}" as region${i} {`); for (const s of new Set(starts.map((k) => split(k)[i]))) out.push(`${pad}[*] --> ${rid[i].get(s)}`); - for (const [s, id] of rid[i]) out.push(`${pad}state "${quote(wrap(s))}" as ${id}`); + for (const [s, id] of rid[i]) + out.push(`${pad}state "${escapeMermaidQuotes(wrap(s))}" as ${id}`); const shownMoves = [...moves[i]] .filter(([id]) => !only || only[i].has(id)) .map(([, m]) => m) @@ -1261,12 +1259,13 @@ for (const [box, members] of boxes) { const out = head(drawn); for (const [box, members] of boxes) { - out.push(` state "${quote(wrap(box))}" as ${boxIds.get(box)} {`); - for (const k of members) out.push(` state "${quote(wrap(caption(k)))}" as ${idOf(k)}`); + out.push(` state "${escapeMermaidQuotes(wrap(box))}" as ${boxIds.get(box)} {`); + for (const k of members) + out.push(` state "${escapeMermaidQuotes(wrap(caption(k)))}" as ${idOf(k)}`); out.push(" }"); } for (const k of sorted) - if (!boxOf.has(k)) out.push(` state "${quote(wrap(caption(k)))}" as ${idOf(k)}`); + if (!boxOf.has(k)) out.push(` state "${escapeMermaidQuotes(wrap(caption(k)))}" as ${idOf(k)}`); for (const k of sorted) if (initial.has(k) && (!args.pathOnly || k === chosen?.path[0].key)) out.push(` [*] --> ${idOf(k)}`); diff --git a/pstack/skills/statechart/scripts/lib.mjs b/pstack/skills/statechart/scripts/lib.mjs index 7fad394df..49f1675bc 100644 --- a/pstack/skills/statechart/scripts/lib.mjs +++ b/pstack/skills/statechart/scripts/lib.mjs @@ -154,9 +154,7 @@ export function ruleSentences(tla) { export const tlaVariables = (code) => [...code.matchAll(/\bVARIABLES?\s+(\w+(?:\s*,\s*\w+)*)/g)].flatMap((m) => m[1].split(/\s*,\s*/)); -// Returns the code with comments blanked, and the comments with the code blanked, at the same -// offsets, so a line number means the same line in both. -function splitComments(text) { +function splitCommentsKeepingOffsets(text) { let code = ""; let notes = ""; let block = 0; @@ -206,11 +204,8 @@ const CITATION = /[\w./-]+\.[A-Za-z]\w*:\d+|#L\d+/; const DEPTH = { "(": 1, "[": 1, "{": 1, ")": -1, "]": -1, "}": -1 }; const LOOSER_THAN_AND = /^(\\\/|=>|<=>|~>|-\+->|\\equiv\b)/; const RUNS_TO_END = /^(\\[EA]|IF|LET|CASE|CHOOSE)\b/; +export const PRIMES_OR_UNCHANGED = /[\w)\]>}]'|\bUNCHANGED\b/; -// The conjuncts of a definition body, as [from, to) offsets: a bulleted /\ list, or a body that -// /\ joins outside brackets, after any leading \E x : . An IF, LET, CASE, CHOOSE, or quantifier -// runs to the end of its conjunct. null when an operator that binds looser than /\, such as \/ -// or =>, joins the body. function conjuncts(bare, from, to, lineStart) { const first = from + bare.slice(from, to).search(/\S/); if (first < from) return null; @@ -251,12 +246,8 @@ function conjuncts(bare, from, to, lineStart) { return [first, ...cuts.map((c) => c + 2)].map((a, i) => [a, cuts[i] ?? to]); } -// The enabling conditions of each action that wait on a variable the action does not change, -// and that no comment ties to a file and line. An action is a definition that primes a variable -// or has UNCHANGED. The comment sits on the condition's lines, or right above them when the -// condition does not start on the definition's line. export function uncitedConditions(text) { - const { code, notes } = splitComments(text); + const { code, notes } = splitCommentsKeepingOffsets(text); const bare = code.replace(/"(?:[^"\\\n]|\\.)*"/g, (s) => " ".repeat(s.length)); const variables = new Set(tlaVariables(bare)); const starts = [0, ...[...bare.matchAll(/\n/g)].map((m) => m.index + 1)]; @@ -289,7 +280,7 @@ export function uncitedConditions(text) { writes: [...body.matchAll(/(? m[1]) .filter((id) => variables.has(id)), - acts: /[\w)\]>}]'|\bUNCHANGED\b/.test(body), + acts: PRIMES_OR_UNCHANGED.test(body), calls: [...new Set(ids.filter((id) => defs.has(id)))], }; }; @@ -310,7 +301,7 @@ export function uncitedConditions(text) { } return out; }; - const cited = (from, to, above) => { + const cited = (from, to, { above }) => { for (let l = from; l <= to; l++) if (CITATION.test(lines.notes[l])) return true; for (let l = from - 1; above && !lines.bare[l].trim() && lines.notes[l].trim(); l--) if (CITATION.test(lines.notes[l])) return true; @@ -326,7 +317,7 @@ export function uncitedConditions(text) { if (part.acts || [...part.reads].every((v) => changes.has(v))) continue; const first = lineOf(a + bare.slice(a, b).search(/\S/)); const last = lineOf(a + bare.slice(a, b).trimEnd().length - 1); - if (cited(first, last, first > d.line)) continue; + if (cited(first, last, { above: first > d.line })) continue; found.push({ line: first + 1, action, @@ -434,9 +425,8 @@ export const BROKEN_PROPERTY = // With -continue, TLC prints "Model checking completed" even after broken invariants, and not // when it stopped early. TLC can also throw a Java exception of its own while it reports a state // that breaks a rule, and stop early. An error in the rule's formula throws one of TLC's own -// exceptions in place of java.*. Returns a warning for that crash, without the file name because -// the caller can move the file, and throws for other errors. -export function checkTlcOutput(text, file) { +// exceptions in place of java.*. +export function tlcOutputWarning(text, file) { const lines = text.split("\n"); const named = (re) => new Set(lines.map((l) => re.exec(l)?.[1]).filter(Boolean)); const broken = named(/^Error: Invariant (\S+) is violated/); @@ -514,8 +504,7 @@ const unwrap = (s) => .replace(/\s+/g, " ") .trim(); -// Mermaid ends a quoted state caption at the first ", so a caption writes " as #quot;. -export const quote = (s) => String(s).replaceAll('"', "#quot;"); +export const escapeMermaidQuotes = (s) => String(s).replaceAll('"', "#quot;"); export const LEGEND_ID = "legend"; export const FULL_LABELS = "%% labels in full"; @@ -628,15 +617,14 @@ export function parseMermaid(text) { "the chart has -- outside a composite; to make parallel regions, split one top-level composite with --", ); - // Ids are global, as in Mermaid: a transition may name a state declared inside another composite. function region(p) { const out = { states: new Set(), initial: new Set(), transitions: [] }; const info = new Map(); - const declared = new Set(); + const declaredInRegion = new Set(); (function collect(q) { for (const c of q.children) { if (c.name === LEGEND_ID) continue; - declared.add(c.name); + declaredInRegion.add(c.name); if (!c.leaf) for (const sub of c.parts) collect(sub); } })(p); @@ -650,8 +638,8 @@ export function parseMermaid(text) { const local = q.children.filter((c) => c.name !== LEGEND_ID); for (const t of q.transitions) { for (const end of [t.from, t.to]) { - if (end === "[*]" || declared.has(end)) continue; - declared.add(end); + if (end === "[*]" || declaredInRegion.has(end)) continue; + declaredInRegion.add(end); local.push({ name: end, leaf: true }); } } @@ -905,8 +893,7 @@ const rgb = (hex) => { const h = hex.length === 4 ? [...hex.slice(1)].map((c) => c + c).join("") : hex.slice(1); return [0, 2, 4].map((i) => parseInt(h.slice(i, i + 2), 16)); }; -// WCAG relative luminance: 0 for black, 1 for white. -function luminance(hex) { +function wcagRelativeLuminance(hex) { const [r, g, b] = rgb(hex).map((c) => { const s = c / 255; return s <= 0.03928 ? s / 12.92 : ((s + 0.055) / 1.055) ** 2.4; @@ -916,7 +903,7 @@ function luminance(hex) { export function groupColorProblem(color) { if (typeof color !== "string" || !/^#([0-9a-f]{3}|[0-9a-f]{6})$/i.test(color)) return 'is not "#rgb" or "#rrggbb"'; - if (luminance(color) < 0.5) return "is too dark for the status borders to show on it"; + if (wcagRelativeLuminance(color) < 0.5) return "is too dark for the status borders to show on it"; return null; } diff --git a/pstack/skills/statechart/scripts/statechart.mjs b/pstack/skills/statechart/scripts/statechart.mjs index 685b60117..0ff4255c2 100644 --- a/pstack/skills/statechart/scripts/statechart.mjs +++ b/pstack/skills/statechart/scripts/statechart.mjs @@ -7,11 +7,12 @@ import process from "node:process"; import { fileURLToPath, pathToFileURL } from "node:url"; import { BROKEN_PROPERTY, - checkTlcOutput, findTlc, joinAnd, parseDot, + PRIMES_OR_UNCHANGED, tlaVariables, + tlcOutputWarning, uncitedConditions, } from "./lib.mjs"; @@ -346,7 +347,7 @@ function tlc(tools, spec, cfg, base, { dump, workers = "1" } = {}) { if (r.error) throw new CannotFinish(`cannot run TLC: ${r.error.message}`); fs.writeFileSync(`${base}.out`, r.stdout); try { - return { stdout: r.stdout, warning: checkTlcOutput(r.stdout, `${base}.out`) }; + return { stdout: r.stdout, warning: tlcOutputWarning(r.stdout, `${base}.out`) }; } catch (e) { throw new TlcStopped(e.message); } @@ -423,8 +424,6 @@ function check(tools, model, { work, out }, expected) { const said = (rule, broken) => ` ${rule} ${broken ? (expected.has(rule) ? "is broken (expected)" : "is broken") : "holds"}.`; const shown = (file) => rel(path.join(out, "tlc", path.basename(file))); - // With -continue TLC reports every bad state. The CONSTRAINT stops each path at its first bad - // state, so a rule that stays broken reports only the step that broke it, not every later state. const traces = rules.map((rule) => { const file = path.join(tlcDir, `${name}-${rule}`); const cfg = `${cfgWithoutRules}INVARIANT ${rule}\nCONSTRAINT ${rule}\n`; @@ -470,14 +469,13 @@ function rulesAsExpected(now, other, expected) { const SCAFFOLD = (name, spec) => { const text = withoutComments(spec); const vars = tlaVariables(text); - // TLC names each step after a definition that primes a variable or leaves one UNCHANGED. A - // definition that only another action calls is listed too, though TLC names no step after it. + // A definition that only another action calls is listed too, though TLC names no step after it. const actions = [ ...new Set( text .split(/\n(?=\S)/) .map((d) => /^(\w+)\s*(?:\([^)]*\))?\s*==([^]*)/.exec(d)) - .filter((d) => d && /[\w)\]>}]'|\bUNCHANGED\b/.test(d[2])) + .filter((d) => d && PRIMES_OR_UNCHANGED.test(d[2])) .map((d) => d[1]), ), ].sort(); @@ -732,7 +730,7 @@ const moved = (from, to, ...missed) => { if (!["ENOSYS", "EXDEV", "EISDIR"].includes(e.code)) throw e; } // Some filesystems, such as FUSE mounts, cannot rename a folder that has files. They fail with - // ENOSYS, or with EISDIR when the target exists. Copy, and keep rename's outcomes. + // ENOSYS, or with EISDIR when the target exists. if (!fs.existsSync(from) && missed.includes("ENOENT")) return false; if (fs.existsSync(to)) { if (fs.readdirSync(to).length && missed.includes("ENOTEMPTY")) return false; @@ -819,7 +817,6 @@ function secondModel(input, cfg, { fixed, against, label }) { } const [role, spec] = fixed ? ["fixed", fixed] : ["against", against]; const name = path.basename(input, ".tla"); - // TLC's output files are named after the spec, so a second model with the same name overwrites them. if (path.basename(spec, ".tla") === name) throw new CannotFinish( `${rel(spec)} needs its own file and module name, such as ${name}${fixed ? "Fixed" : "Agreed"}.tla.`, @@ -835,9 +832,6 @@ function warnUnchecked(now, other) { ); } -// The rule that each config beside the spec expects TLC to break, from the "\* expect:" and -// "\* module:" lines of each config. null when no config of the spec's -// module has an "\* expect:" line. function listedBreaks(spec) { const dir = path.dirname(spec); const files = fs.readdirSync(dir).sort(); diff --git a/pstack/skills/statechart/scripts/test/statechart.test.mjs b/pstack/skills/statechart/scripts/test/statechart.test.mjs index 28d1c3d96..72782e679 100644 --- a/pstack/skills/statechart/scripts/test/statechart.test.mjs +++ b/pstack/skills/statechart/scripts/test/statechart.test.mjs @@ -15,7 +15,6 @@ import { test } from "node:test"; import { setTimeout as sleep } from "node:timers/promises"; import { fileURLToPath } from "node:url"; import { - checkTlcOutput, findTlc, parseDot, parseMermaid, @@ -23,6 +22,7 @@ import { parseValue, ruleSentences, stateKey, + tlcOutputWarning, uncitedConditions, } from "../lib.mjs"; @@ -280,7 +280,7 @@ test("a rule broken by a start state is a counterexample of one state", () => { /\\ conn = "Offline" ${done}`; - assert.doesNotThrow(() => checkTlcOutput(text, "tlc.out")); + assert.doesNotThrow(() => tlcOutputWarning(text, "tlc.out")); assert.deepEqual(parseTraces(text), [ { invariant: "NeverSyncedWhileOffline", @@ -291,30 +291,30 @@ ${done}`; test("TLC output from a run that failed or stopped early is refused", () => { assert.doesNotThrow(() => - checkTlcOutput( + tlcOutputWarning( `Error: Invariant Small is violated.\nError: The behavior up to this point is:\nState 1: \nx = 0\n\n${done}`, "ok.out", ), ); assert.throws( () => - checkTlcOutput( + tlcOutputWarning( "Error: The invariant Nope specified in the configuration file\nis not defined in the specification.\n", "cfg.out", ), /cfg\.out: TLC stopped on an error that is not a broken rule/, ); assert.throws( - () => checkTlcOutput("Error: Parsing or semantic analysis failed.\n", "parse.out"), + () => tlcOutputWarning("Error: Parsing or semantic analysis failed.\n", "parse.out"), /not a broken rule/, ); assert.throws( - () => checkTlcOutput(evaluationError, "eval.out"), + () => tlcOutputWarning(evaluationError, "eval.out"), /TLC threw an unexpected exception/, ); assert.throws( () => - checkTlcOutput( + tlcOutputWarning( "Error: Invariant Small is violated.\nError: The behavior up to this point is:\nState 1: \nx = 0\n", "stopped.out", ), @@ -348,12 +348,12 @@ test("a rule that TLC finds broken before TLC throws a Java exception keeps its "Index 123 out of bounds for length 4", )}\n${stoppedEarly}`; assert.equal( - checkTlcOutput(oneWorker, "tlc.out"), + tlcOutputWarning(oneWorker, "tlc.out"), `TLC found that Small is broken, and then failed with ${aioobe}. TLC stopped before it checked every state, so the charts can miss states that break Small. The failure is in TLC, not in the rule. Do not weaken Small because of it. A smaller constant can let TLC finish.`, ); const workersInterleaved = `${tlcThrew("java.lang.RuntimeException", aioobe)}${smallBroken}${stoppedEarly}`; assert.match( - checkTlcOutput(workersInterleaved, "tlc.out"), + tlcOutputWarning(workersInterleaved, "tlc.out"), /failed with java\.lang\.ArrayIndexOutOfBoundsException: Index 123/, ); assert.deepEqual( @@ -362,7 +362,7 @@ test("a rule that TLC finds broken before TLC throws a Java exception keeps its ); assert.throws( () => - checkTlcOutput( + tlcOutputWarning( `${smallBroken}${tlcThrew("java.lang.RuntimeException", "util.Assert$TLCRuntimeException: Attempted to apply tuple")}${stoppedEarly}`, "formula.out", ), @@ -370,7 +370,7 @@ test("a rule that TLC finds broken before TLC throws a Java exception keeps its ); assert.throws( () => - checkTlcOutput( + tlcOutputWarning( `${tlcThrew("java.lang.ArrayIndexOutOfBoundsException", "Index 123 out of bounds for length 4")}${stoppedEarly}`, "never-broken.out", ), diff --git a/pstack/skills/statechart/scripts/tlc-to-chart.mjs b/pstack/skills/statechart/scripts/tlc-to-chart.mjs index 005c9ef7c..37ae46e33 100644 --- a/pstack/skills/statechart/scripts/tlc-to-chart.mjs +++ b/pstack/skills/statechart/scripts/tlc-to-chart.mjs @@ -8,8 +8,8 @@ import { GROUP_PALETTE, LEGEND_ID, PLAIN_FILL, - checkTlcOutput, compareCharts, + escapeMermaidQuotes, groupClassDef, groupColorProblem, isRecord, @@ -19,9 +19,9 @@ import { parseMermaid, parseTraces, productOf, - quote, ruleSentences, stateKey, + tlcOutputWarning, wrap, STATUS_CLASSES, } from "./lib.mjs"; @@ -523,7 +523,7 @@ function replaySecond(trace) { function readTraces(files, paths = []) { return files.flatMap((f) => { const text = fs.readFileSync(f, "utf8"); - const warning = checkTlcOutput(text, f); + const warning = tlcOutputWarning(text, f); if (warning) console.error(`${f}: ${warning}`); return parseTraces(text).map((t) => ({ ...t, @@ -531,7 +531,6 @@ function readTraces(files, paths = []) { })); }); } -// With -continue, TLC reports every bad state, including states after the first bad one. function firstBad(raw) { const badStates = new Map(); for (const t of raw) { @@ -827,8 +826,6 @@ const groupCounts = (drawn) => })) .filter((g) => g.states > 0); -// Mermaid shrinks a chart to the page width unless useMaxWidth is false, and rewraps labels that -// wrap() already wrapped unless markdownAutoWrap is false. const frontMatter = (title) => [ "---", ...(title ? [`title: ${JSON.stringify(title)}`] : []), @@ -861,7 +858,7 @@ function head(drawn) { } else for (const c of STATUS_CLASSES) out.push(` ${c}`); if (legend.length) { out.push(` state "Legend" as ${LEGEND_ID} {`); - for (const [id, text] of legend) out.push(` state "${quote(text)}" as ${id}`); + for (const [id, text] of legend) out.push(` state "${escapeMermaidQuotes(text)}" as ${id}`); out.push(" }"); for (const [id, , c] of legend) out.push(` class ${id} ${c}`); } @@ -899,7 +896,7 @@ function regionsChart({ states, starts, edges, classes, proofPath, allPath }) { const proof = [ ...frontMatter(), "stateDiagram-v2", - ...[...ids].map(([s, id]) => ` state "${quote(s)}" as ${id}`), + ...[...ids].map(([s, id]) => ` state "${escapeMermaidQuotes(s)}" as ${id}`), ...[...flat.Main.initial].map((s) => ` [*] --> ${ids.get(s)}`), ...steps.map((s) => ` ${ids.get(bar(s.from))} --> ${ids.get(bar(s.to))} : ${s.label}`), ]; @@ -978,10 +975,11 @@ function regionsChart({ states, starts, edges, classes, proofPath, allPath }) { if (i) out.push(" --"); const name = mapping.regionNames?.[i]; const pad = name ? " " : " "; - if (name) out.push(` state "${quote(wrap(name))}" as region${i} {`); + if (name) out.push(` state "${escapeMermaidQuotes(wrap(name))}" as region${i} {`); for (const s of new Set(starts.map((k) => split(k)[i]))) out.push(`${pad}[*] --> ${rid[i].get(s)}`); - for (const [s, id] of rid[i]) out.push(`${pad}state "${quote(wrap(s))}" as ${id}`); + for (const [s, id] of rid[i]) + out.push(`${pad}state "${escapeMermaidQuotes(wrap(s))}" as ${id}`); const shownMoves = [...moves[i]] .filter(([id]) => !only || only[i].has(id)) .map(([, m]) => m) @@ -1261,12 +1259,13 @@ for (const [box, members] of boxes) { const out = head(drawn); for (const [box, members] of boxes) { - out.push(` state "${quote(wrap(box))}" as ${boxIds.get(box)} {`); - for (const k of members) out.push(` state "${quote(wrap(caption(k)))}" as ${idOf(k)}`); + out.push(` state "${escapeMermaidQuotes(wrap(box))}" as ${boxIds.get(box)} {`); + for (const k of members) + out.push(` state "${escapeMermaidQuotes(wrap(caption(k)))}" as ${idOf(k)}`); out.push(" }"); } for (const k of sorted) - if (!boxOf.has(k)) out.push(` state "${quote(wrap(caption(k)))}" as ${idOf(k)}`); + if (!boxOf.has(k)) out.push(` state "${escapeMermaidQuotes(wrap(caption(k)))}" as ${idOf(k)}`); for (const k of sorted) if (initial.has(k) && (!args.pathOnly || k === chosen?.path[0].key)) out.push(` [*] --> ${idOf(k)}`);