From b2cb69c5eccb410c5a7ab22c534d78bf3377f1f2 Mon Sep 17 00:00:00 2001 From: Christian Bager Bach Houmann Date: Thu, 22 Oct 2026 19:51:09 +0200 Subject: [PATCH 1/4] Sync Lauren's pstack to 7698375 (#776) All three components move from eb4db2b to 7698375. Upstream changed only pstack, and only the statechart skill (pstack #776). The label map stops on a variable or field that the --fixed or --against model lacks, in place of using the current model's start value. New --config, --fixed-config, and --against-config flags mean the agreed spec is never checked with the code model's config, and a rule the agreed config does not check is marked "not checked". When TLC finds a broken rule and then throws, the command keeps the paths it printed and warns. On a file system that cannot rename into the output folder (ENOSYS, EXDEV, EISDIR, as on FUSE mounts) it copies the files into place. TLC now checks each rule with one worker per CPU and rechecks a broken rule with one worker, each PROPERTY gets its own run, and --expect-broken accepts it. With --against each story says whether a config beside the agreed spec expects the bug, and with --fixed or --against the command lists conditions with no file:line citation. SKILL.md asks for those citations, defines a valid replay, and asks the hand-off to say whether the spec already lists each bug. The test accepts Naturals.tla anywhere under TLC 1.8.0's temp folder. bun tools/sync.mjs updated SKILL.md, lib.mjs, statechart.mjs, tlc-to-chart.mjs, and the test file cleanly, and each is byte-identical to upstream at 7698375, file modes included. No substitution, fork, or hook changed. The 15 declared forks were left alone, and cursor-team-kit and thermos synced with no file changes. Upstream's copies under harness/pstack/claude-code/ sit outside every synced component. --- plugins/pstack/skills/statechart/SKILL.md | 8 +- .../pstack/skills/statechart/scripts/lib.mjs | 236 ++++++- .../skills/statechart/scripts/statechart.mjs | 382 +++++++++--- .../scripts/test/statechart.test.mjs | 589 ++++++++++++++++-- .../statechart/scripts/tlc-to-chart.mjs | 178 ++++-- tools/upstream.json | 6 +- 6 files changed, 1209 insertions(+), 190 deletions(-) diff --git a/plugins/pstack/skills/statechart/SKILL.md b/plugins/pstack/skills/statechart/SKILL.md index 1693be3b..1818f2a7 100644 --- a/plugins/pstack/skills/statechart/SKILL.md +++ b/plugins/pstack/skills/statechart/SKILL.md @@ -14,16 +14,16 @@ Run `node /scripts/statechart.mjs --help` for the commands and for ho Use `from-spec` when a TLA+ model exists or the code is concrete enough to model. Use `from-chart` when there is no model and the PM should agree on the behavior before anyone writes or changes the code. -If the code already has a TLA+ spec, start from a copy of that spec. Add the variables the user sees, and keep the spec's existing invariants. To audit the code against that spec, make the copy model what the code does, and pass the spec unchanged as `--against`. In a new spec, tie every variable and action to code that a reviewer can open, and take its name from that code. Make each action one indivisible step in the code. +If the code already has a TLA+ spec, start from a copy of that spec. Add the variables the user sees, and keep the spec's existing invariants. To audit the code against that spec, make the copy model what the code does, and pass the spec unchanged as `--against`. Check it with the config that its authors say it passes, and pass that config as `--against-config` unless it has the spec's file name. One mapping labels both models, so label states and steps only from variables that both have. In a code model or a new spec, tie every variable and action to code that a reviewer can open, and take its name from that code. Make each action one indivisible step in the code. Put the file and line of the code that checks each condition of an action in a comment on that condition, as in `\* pay.ts:120`. ## Spec to chart 1. Choose the chart's states. When the PM cares about something the screen does not show, such as a second charge while the screen still says "Paying", name the state "Paying, charged twice". Start with few states, and split a state only when the split separates two bugs. -2. Write each rule the PM agrees to as one invariant, with the PM's sentence as its comment. For a rule that applies once everything settles, define `Settled == ~ENABLED System`, where `System` is the disjunction of the actions the user does not take. Report each broken rule as a bug. Never weaken a rule to make the chart pass. +2. Write each rule the PM agrees to as one invariant, with the PM's sentence as its comment. Each rule names what the user sees on a screen or gets from a request, and the code that can change it. Refuse a rule that lacks one of them. For a rule that applies once everything settles, define `Settled == ~ENABLED System`, where `System` is the disjunction of the actions the user does not take. Report each broken rule as a bug. Never weaken a rule to make the chart pass. 3. Run `from-spec`, then fill in the mapping file it writes. Put the labels in `state` and `step`, and list the user's actions in `readerActions` by action name. When two bugs end on the same screen through different code paths, add `cause` and make it name the code path. To color the states by what the PM cares about, such as "Toast shown", return that group from `group`. The legend names the groups, and states that break a rule still get a red border. 4. If there is an open fix, model it from the code and pass that model as `--fixed`. 5. Render each chart with `--png` and look at every PNG. Check that each numbered path reads in order. If a label reads like code, fix `state` or `step` and run the command again. -6. Replay each bug's story against the real code, as a test or a live repro, one step per model action. If a bug does not reproduce, assume the model is wrong until you show otherwise. Fix the model, not the rule. +6. Replay each bug's story against the real code, as a test or a live repro, one step per model action. Drive only entry points that a user or client reaches, and assert only what they see. A test that asserts a flag that it sets, or that searches the source text, proves nothing. When a run proves part of the story and reading the code proves the rest, say which part each proves. When the test copies code that it cannot import, give the commit and line range of the copy, and list what the copy leaves out. If a bug does not reproduce, assume the model is wrong until you show otherwise. Fix the model, not the rule. ## Chart to spec @@ -33,4 +33,4 @@ If the code already has a TLA+ spec, start from a copy of that spec. Add the var ## Hand off -Give the PM the PNG and the Mermaid source of each chart. Add one line per bug with the rule it breaks, its steps as the chart numbers them, whether it reproduced, and whether the open fix fixes it. Take every count you quote from `summary.json`. Attach `stories.md` and the command that regenerates everything. Say what the model leaves out. +Give the PM the PNG and the Mermaid source of each chart. Add one line per bug with the rule it breaks, its steps as the chart numbers them, whether it reproduced, and whether the open fix fixes it. With `--against`, also say whether the spec already lists it: in the configs that `stories.md` names, in the spec's notes on what the model leaves out, or not at all. Do not report that a rule holds while the command lists conditions with no file and line. Take every count you quote from `summary.json`. Attach `stories.md` and the command that regenerates everything. Say what the model leaves out. diff --git a/plugins/pstack/skills/statechart/scripts/lib.mjs b/plugins/pstack/skills/statechart/scripts/lib.mjs index cf72d5cd..7fad394d 100644 --- a/plugins/pstack/skills/statechart/scripts/lib.mjs +++ b/plugins/pstack/skills/statechart/scripts/lib.mjs @@ -151,6 +151,192 @@ export function ruleSentences(tla) { return out; } +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) { + let code = ""; + let notes = ""; + let block = 0; + let line = false; + let string = false; + const put = (c, n) => { + code += c; + notes += n; + }; + for (let i = 0; i < text.length; i++) { + const c = text[i]; + const two = text.slice(i, i + 2); + if (c === "\n") { + line = string = false; + put(c, c); + } else if (block) { + if (two === "(*" || two === "*)") { + block += two === "(*" ? 1 : -1; + put(" ", two); + i++; + } else put(" ", c); + } else if (line) put(" ", c); + else if (string) { + if (c === "\\" && text[i + 1] && text[i + 1] !== "\n") { + put(two, " "); + i++; + } else { + string = c !== '"'; + put(c, " "); + } + } else if (two === "\\*" || two === "(*") { + if (two === "\\*") line = true; + else block = 1; + put(" ", two); + i++; + } else { + string = c === '"'; + put(c, " "); + } + } + return { code, notes }; +} + +const IDENTIFIER = /(?)/g; +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/; + +// 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; + if (/^\\E\b/.test(bare.slice(first, to))) { + for (let i = first, depth = 0; i < to; i++) { + depth += DEPTH[bare[i]] ?? 0; + if (depth === 0 && bare[i] === ":") return conjuncts(bare, i + 1, to, lineStart); + } + return null; + } + if (bare.startsWith("/\\", first)) { + const column = first - lineStart(first); + const bullets = [first]; + for (const m of bare.slice(first, to).matchAll(/\n([ \t]*)(?=\S)/g)) { + if (m[1].length < column) return null; + const at = first + m.index + m[0].length; + if (m[1].length === column && bare.startsWith("/\\", at)) bullets.push(at); + } + return bullets.flatMap((b, i) => { + const end = bullets[i + 1] ?? to; + return conjuncts(bare, b + 2, end, lineStart) ?? [[b + 2, end]]; + }); + } + const cuts = []; + let depth = 0; + for (let i = first; i < to; i++) { + const two = bare.slice(i, i + 2); + const ahead = bare.slice(i, i + 7); + if (two === "<<" || two === ">>") { + depth += two === "<<" ? 1 : -1; + i++; + } else if (DEPTH[bare[i]]) depth += DEPTH[bare[i]]; + else if (depth > 0) continue; + else if (LOOSER_THAN_AND.test(ahead)) return null; + else if (!/\w/.test(bare[i - 1] ?? "") && RUNS_TO_END.test(ahead)) break; + else if (two === "/\\") cuts.push(i++); + } + 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 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)]; + const lineOf = (at) => { + let lo = 0; + let hi = starts.length - 1; + while (lo < hi) { + const mid = (lo + hi + 1) >> 1; + if (starts[mid] <= at) lo = mid; + else hi = mid - 1; + } + return lo; + }; + const lineStart = (at) => starts[lineOf(at)]; + const lines = { bare: bare.split("\n"), notes: notes.split("\n") }; + + const defs = new Map(); + const nextItem = /^(?![ \t\n]|\/\\|\\\/)/gm; + for (const m of bare.matchAll( + /^(?:LOCAL[ \t]+)?([A-Za-z_]\w*)[ \t]*(?:\([^)]*\)|\[[^\]]*\])?[ \t]*==/gm, + )) { + const from = m.index + m[0].length; + nextItem.lastIndex = from; + defs.set(m[1], { from, to: nextItem.exec(bare)?.index ?? bare.length, line: lineOf(m.index) }); + } + const direct = (body) => { + const ids = body.match(IDENTIFIER) ?? []; + return { + reads: ids.filter((id) => variables.has(id)), + writes: [...body.matchAll(/(? m[1]) + .filter((id) => variables.has(id)), + acts: /[\w)\]>}]'|\bUNCHANGED\b/.test(body), + calls: [...new Set(ids.filter((id) => defs.has(id)))], + }; + }; + const own = new Map([...defs].map(([name, d]) => [name, direct(bare.slice(d.from, d.to))])); + const through = (start) => { + const out = { reads: new Set(start.reads), writes: new Set(start.writes), acts: start.acts }; + const seen = new Set(start.calls); + const todo = [...seen]; + while (todo.length) { + const d = own.get(todo.pop()); + d.reads.forEach((v) => out.reads.add(v)); + d.writes.forEach((v) => out.writes.add(v)); + out.acts ||= d.acts; + for (const c of d.calls.filter((c) => !seen.has(c))) { + seen.add(c); + todo.push(c); + } + } + return out; + }; + 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; + return false; + }; + + const found = []; + for (const [action, d] of defs) { + if (!own.get(action).acts) continue; + const changes = through(own.get(action)).writes; + for (const [a, b] of conjuncts(bare, d.from, d.to, lineStart) ?? []) { + const part = through(direct(bare.slice(a, b))); + 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; + found.push({ + line: first + 1, + action, + condition: code.slice(a, b).replace(/\s+/g, " ").trim(), + }); + } + } + return found; +} + function unescapeDot(s) { let out = ""; for (let i = 0; i < s.length; i++) { @@ -239,24 +425,53 @@ export function parseTraces(text) { return traces; } +// TLC words a broken PROPERTY by its form: [](state predicate) as an invariant, [][A]_v as an +// action property, a bare state predicate, which TLC checks only in the initial states, as a +// property of the initial state, and any other formula as a temporal property. +export const BROKEN_PROPERTY = + /^Error: (Invariant \S+ is violated|Action property \S+ is violated\.|Property \S+ is violated by the initial state:|Temporal properties were violated\.)/m; + // With -continue, TLC prints "Model checking completed" even after broken invariants, and not -// when it stopped early. +// 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) { - const other = text - .split("\n") - .find( - (l) => - l.startsWith("Error: ") && - !/^Error: (Invariant \S+ is violated|The behavior up to this point is)/.test(l), - ); + 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/); + const failed = [...named(/^Error: Evaluating invariant (\S+) failed\./)]; + const thrown = [...text.matchAll(/^The exception was a (\S+)\n: (?:([\w.$]+):)?(.*)$/gm)].map( + ([, cls, cause, message]) => `${cause ?? cls}: ${message.trim()}`, + ); + const crashed = + failed.length > 0 && + failed.every((r) => broken.has(r)) && + thrown.length > 0 && + thrown.every((t) => t.startsWith("java.")); + const reported = crashed + ? /^Error: (Invariant \S+ is violated|The behavior up to this point is|Evaluating invariant \S+ failed\.|TLC threw an unexpected exception\.|The error occurred when TLC was evaluating the nested)/ + : /^Error: (Invariant \S+ is violated|Action property \S+ is violated\.|Property \S+ is violated by the initial state:|The behavior up to this point is|Temporal properties were violated\.|The following behavior constitutes a counter-example:)/; + const other = lines.find((l) => l.startsWith("Error: ") && !reported.test(l)); if (other) throw new Error( `${file}: TLC stopped on an error that is not a broken rule: ${other.slice(7)}`, ); - if (!/^Model checking completed\./m.test(text)) + if (crashed) { + const rules = failed.join(", "); + return `TLC found that ${rules} ${failed.length === 1 ? "is" : "are"} broken, and then failed with ${thrown[0]}. TLC stopped before it checked every state, so the charts can miss states that break ${rules}. The failure is in TLC, not in the rule. Do not weaken ${rules} because of it. A smaller constant can let TLC finish.`; + } + // TLC stops at the first broken temporal property, and at an initial state that breaks a + // PROPERTY, and then does not print that it completed. + if ( + !/^(Model checking completed\.|Error: (Temporal properties were violated\.|Property \S+ is violated by the initial state:))/m.test( + text, + ) + ) throw new Error( `${file}: TLC did not finish, so its counterexamples are not all there; read the file`, ); + return null; } export function wrap(text, width = 26) { @@ -273,6 +488,9 @@ export function wrap(text, width = 26) { return rows.join("
"); } +export const joinAnd = (items) => + items.length < 3 ? items.join(" and ") : `${items.slice(0, -1).join(", ")}, and ${items.at(-1)}`; + const OPENS_A_PHRASE = new Set( "a an the your my our their its this that to of in on at for with from by and or".split(" "), ); diff --git a/plugins/pstack/skills/statechart/scripts/statechart.mjs b/plugins/pstack/skills/statechart/scripts/statechart.mjs index 6e2ebfcc..685b6011 100644 --- a/plugins/pstack/skills/statechart/scripts/statechart.mjs +++ b/plugins/pstack/skills/statechart/scripts/statechart.mjs @@ -5,13 +5,21 @@ import os from "node:os"; import path from "node:path"; import process from "node:process"; import { fileURLToPath, pathToFileURL } from "node:url"; -import { checkTlcOutput, findTlc, parseDot } from "./lib.mjs"; +import { + BROKEN_PROPERTY, + checkTlcOutput, + findTlc, + joinAnd, + parseDot, + tlaVariables, + uncitedConditions, +} from "./lib.mjs"; const here = path.dirname(fileURLToPath(import.meta.url)); const USAGE = { "from-spec": - "node statechart.mjs from-spec SPEC.tla [--fixed FIXED.tla | --against AGREED.tla] [--label TEXT] [--map FILE] [--expect-broken RULE]... [--title TEXT] [--out DIR] [--png]", + "node statechart.mjs from-spec SPEC.tla [--config FILE] [--fixed FIXED.tla [--fixed-config FILE] | --against AGREED.tla [--against-config FILE]] [--label TEXT] [--map FILE] [--expect-broken RULE]... [--title TEXT] [--out DIR] [--png]", "from-chart": "node statechart.mjs from-chart CHART.mmd [--module NAME] [--expect-broken RULE]... [--title TEXT] [--out DIR] [--png]", }; @@ -21,27 +29,48 @@ const FROM_SPEC = `from-spec SPEC.tla Checks each INVARIANT in SPEC.cfg in a separate TLC run. TLC stops at the first rule that a state breaks, and the separate runs find the rest. Each run also has the rule as a CONSTRAINT, so TLC stops each path at its first state that breaks the rule, and a rule that stays broken reports - only the step that broke it. SPEC.cfg sits next to the spec and has SPECIFICATION and one - INVARIANT line per rule. One more run dumps the state graph, and then the command draws the - charts. TLC names each step after the innermost named action that takes it, so give each kind of - step its own named action. The command warns when steps carry the name of the whole next-state - action. - + only the step that broke it. SPEC.cfg has SPECIFICATION and one INVARIANT line per rule. Each + PROPERTY, a rule about whole behaviors, gets one TLC run too, and the charts do not draw it. A + rule listed as both INVARIANT and PROPERTY is checked once, as an INVARIANT. One + more run dumps the state graph, and then the command draws the charts. TLC names each step after + the innermost named action that takes it, so give each kind of step its own named action. The + command warns when steps carry the name of the whole next-state action. The command prints the + config that it checks each model with, and stops when a config does not exist, with the configs + beside the spec. + + --config FILE The config for SPEC.tla. Default: SPEC.cfg next to the spec. --fixed FIXED.tla The model of the open fix. It is a copy of the spec with its own file and module name, such as SpecFixed.tla with MODULE SpecFixed. The command checks - it the same way, with FIXED.cfg, or with SPEC.cfg when there is no FIXED.cfg. - The charts then mark each bad state fixed or still wrong. + it the same way, with FIXED.cfg, or with the config of SPEC.tla when there is + no FIXED.cfg. The charts then mark each bad state fixed or still wrong. + --fixed-config FILE + The config for FIXED.tla. --against AGREED.tla The spec that SPEC.tla must follow, when SPEC.tla models the code. It needs - its own file and module name. The command checks it with AGREED.cfg, or with - SPEC.cfg when there is no AGREED.cfg. SPEC.tla may add variables, record - fields, and actions that AGREED.tla does not have. The comparison leaves them - out. Do not use it with --fixed. + its own file and module name. The command checks it with AGREED.cfg, and + never with the config of SPEC.tla. SPEC.tla may add variables, record fields, + and actions that AGREED.tla does not have. The comparison leaves them out. + Do not use it with --fixed. + --against-config FILE + The config for AGREED.tla, when it is not AGREED.cfg. Give the config that the + spec's authors say the unchanged spec passes. A rule that this config does not + check is "not checked" in the stories. --label TEXT The name of the --fixed or --against model in the charts and the stories. Default: "the fix", or "the spec". --map FILE The labels for each model state and step. Default: SPEC.map.mjs next to the - spec. When the file does not exist, the command writes one to fill in and - exits 2. Its comments say what each function gets.`; + spec. When the file does not exist, the command writes one from the spec's + VARIABLES and actions to fill in, and exits 2 before it runs TLC. Its + comments say what each function gets. + + With --fixed or --against, SPEC.tla (and FIXED.tla) models the code, and the command finds each + condition of an action that no comment ties to code with a file and line, as in \\* pay.ts:120. + A condition is a conjunct of the action that changes nothing and reads a variable that the + action does not change. A rule can hold only because the model waits for a condition that the + code does not check, so the command prints these conditions when a rule holds. + With --against, each story says whether a config beside AGREED.tla expects TLC to break the + bug's rule. A config's "\\* expect: RULE" line says what TLC finds, and "\\* module: NAME" names + the module it checks when the folder has more than one .tla file. The command warns when no + config beside AGREED.tla has an expect line for that module.`; const FROM_CHART = `from-chart CHART.mmd Writes NAME.tla, NAME.cfg, and NAME.map.mjs next to the chart. When NAME.tla already exists, it @@ -63,15 +92,16 @@ const FROM_CHART = `from-chart CHART.mmd const COMMON = `Both commands --expect-broken RULE - A rule that is known to break. Repeat it, or list rules with commas, as in - A,B. The command then exits 0 when exactly these rules break, and the --fixed - or --against model breaks no other rule. + An INVARIANT or PROPERTY that is known to break. Repeat it, or list rules + with commas, as in A,B. The command then exits 0 when exactly these rules + break, and the --fixed or --against model breaks no other rule. --title TEXT The chart title. Each bug chart adds ", bug N". --out DIR The output folder. Default: NAME-statechart next to the input. A run writes its 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. + it did not write. On a filesystem that cannot rename, the command copies the + files into place, and overlapping runs can mix their files. --png Also render each chart to PNG with npx @mermaid-js/mermaid-cli. -h, --help Print this help, and exit 0. @@ -87,7 +117,10 @@ Output detail(). stories.md One entry per bug: the rule, why it breaks, the shortest path in reader steps, and what the --fixed or --against model does instead. - summary.json The counts behind the chart. + summary.json The counts behind the chart. With --fixed or --against, uncited has the + conditions with no file and line for each code model. With --against, + second.listed has what each config beside AGREED.tla expects, and each bug + has the configs that list it. tlc/ The config and the TLC output of each run. When the overview has regions, from-spec also writes tlc/regions-all.mmd, the regions with every arrow, and tlc/regions-proof.mmd, every state and step of TLC's graph in one region. @@ -137,6 +170,13 @@ TLC TLA2TOOLS is the path to tla2tools.jar, and JAVA is the java binary (default: java, Java 11 or later). Download tla2tools.jar from https://github.com/tlaplus/tlaplus/releases. When TLA2TOOLS is not set, the command says where to get TLC and exits 2. + TLC checks each rule with one worker per CPU. When a rule is broken, TLC checks it again with one + worker, which finds the shortest bug paths, the same on every run. The command then prints how + many times TLC ran and how long that took. + TLC can find that a rule is broken and then fail with a Java exception while it reports the rule. + The command then keeps the paths that TLC printed, marks the rule broken, and warns that the + charts can miss states that break it. The failure is in TLC, so do not weaken the rule because of + it. A smaller constant can let TLC finish. Exit codes 0 Every rule holds, or exactly the --expect-broken rules break. from-chart also draws CHART.mmd @@ -150,7 +190,9 @@ Exit codes files it wrote and exits 2, whatever the rules give. Otherwise, exit 2 does not change the output folder, unless the command moved it aside and cannot put it back. Then the message names the folder's new path. When TLC stops on an error, the message names TLC's output, in a - temporary folder that the command keeps.`; + temporary folder that the command keeps. When the command cannot put its files in the output + folder, it keeps them in a temporary folder, and the message names it. The command checks + its input files again before --png renders, so a changed input stops the run before that.`; const HELP = { "": `${usage([...Object.values(USAGE), "node statechart.mjs [from-spec|from-chart] --help"])} @@ -172,10 +214,22 @@ const more = (cmd) => class CannotFinish extends Error {} class TlcStopped extends CannotFinish {} +class NotPublished extends CannotFinish {} const COMMANDS = { "from-spec": { - flags: ["--map", "--fixed", "--against", "--label", "--expect-broken", "--title", "--out"], + flags: [ + "--map", + "--config", + "--fixed", + "--fixed-config", + "--against", + "--against-config", + "--label", + "--expect-broken", + "--title", + "--out", + ], run: fromSpec, }, "from-chart": { flags: ["--module", "--expect-broken", "--title", "--out"], run: fromChart }, @@ -203,7 +257,10 @@ function parseArgs([command, ...rest]) { return { command, input, flags }; } -const rel = (file) => path.relative(process.cwd(), file) || "."; +const rel = (file) => { + const r = path.relative(process.cwd(), file) || "."; + return r === ".." || r.startsWith(`..${path.sep}`) ? path.resolve(file) : r; +}; const cfgOf = (spec) => spec.replace(/\.tla$/, ".cfg"); function findTools() { @@ -235,16 +292,28 @@ function splitRules(cfg) { .filter(Boolean); const kept = []; const rules = []; + const properties = []; let section = ""; for (const w of words) { if (KEYWORD.test(w)) section = w; - if (!/^INVARIANTS?$/.test(section)) kept.push(KEYWORD.test(w) && kept.length ? `\n${w}` : w); - else if (w !== section && !rules.includes(w)) rules.push(w); + const list = /^INVARIANTS?$/.test(section) + ? rules + : /^PROPERT(Y|IES)$/.test(section) + ? properties + : null; + if (!list) kept.push(KEYWORD.test(w) && kept.length ? `\n${w}` : w); + else if (w !== section && !list.includes(w)) list.push(w); } - return { cfgWithoutRules: `${kept.join(" ")}\n`, rules }; + // TLC takes only a state predicate as an INVARIANT, and checks a state predicate given as a + // PROPERTY only in the initial states, which the INVARIANT run checks too. + return { + cfgWithoutRules: `${kept.join(" ")}\n`, + rules, + properties: properties.filter((p) => !rules.includes(p)), + }; } -function tlc(tools, spec, cfg, base, dump) { +function tlc(tools, spec, cfg, base, { dump, workers = "1" } = {}) { fs.writeFileSync(`${base}.cfg`, cfg); const metadir = fs.mkdtempSync(path.join(os.tmpdir(), "tlc-")); // TLC writes the standard modules, such as Naturals.tla, to java.io.tmpdir under fixed names, @@ -255,10 +324,13 @@ function tlc(tools, spec, cfg, base, dump) { const r = spawnSync( tools.java, [ + "-XX:+UseParallelGC", `-Djava.io.tmpdir=${javaTmp}`, "-cp", tools.jar, "tlc2.TLC", + "-workers", + workers, "-metadir", metadir, "-deadlock", @@ -274,18 +346,20 @@ function tlc(tools, spec, cfg, base, dump) { if (r.error) throw new CannotFinish(`cannot run TLC: ${r.error.message}`); fs.writeFileSync(`${base}.out`, r.stdout); try { - checkTlcOutput(r.stdout, `${base}.out`); + return { stdout: r.stdout, warning: checkTlcOutput(r.stdout, `${base}.out`) }; } catch (e) { throw new TlcStopped(e.message); } - return r.stdout; } -function warnUnnamedSteps(spec, cfg, dot) { - const text = fs +const withoutComments = (spec) => + fs .readFileSync(spec, "utf8") .replace(/\(\*[^]*?\*\)/g, " ") .replace(/\\\*.*/g, " "); + +function warnUnnamedSteps(spec, cfg, dot) { + const text = withoutComments(spec); const specName = /^SPECIFICATION\s+(\w+)/m.exec(cfg)?.[1]; const specBody = specName && new RegExp(`^${specName}\\s*==(.*(\\n[ \\t]+.*)*)`, "m").exec(text); const next = @@ -298,50 +372,89 @@ function warnUnnamedSteps(spec, cfg, dot) { ); } -function readModel(spec, cfgFile) { +function readModel(spec, cfgFile, flag) { if (!fs.existsSync(spec)) throw new CannotFinish(`${rel(spec)} does not exist`); - if (!fs.existsSync(cfgFile)) + if (!fs.existsSync(cfgFile)) { + const beside = fs + .readdirSync(path.dirname(spec)) + .filter((f) => f.endsWith(".cfg")) + .sort(); throw new CannotFinish( - `${rel(cfgFile)} does not exist. It needs SPECIFICATION and one INVARIANT line per rule.`, + `${rel(cfgFile)} does not exist. Pass ${flag} with the config to check ${path.basename(spec)} with. ${ + beside.length + ? `The configs beside it: ${beside.join(", ")}.` + : "A config has SPECIFICATION and one INVARIANT line per rule." + }`, ); + } return { spec, cfgFile, ...splitRules(fs.readFileSync(cfgFile, "utf8")) }; } -function readInput(spec, expected) { - const model = readModel(spec, cfgOf(spec)); - const unknown = [...expected].filter((r) => !model.rules.includes(r)); +function readInput(spec, cfgFile, expected) { + const model = readModel(spec, cfgFile, "--config"); + const names = [...model.rules, ...model.properties]; + const unknown = [...expected].filter((r) => !names.includes(r)); if (unknown.length) throw new CannotFinish( - `--expect-broken ${unknown.join(", ")}: not a rule in ${rel(model.cfgFile)}, whose rules are ${model.rules.join(", ") || "none"}.`, + `--expect-broken ${unknown.join(", ")}: not a rule in ${rel(model.cfgFile)}, whose rules are ${names.join(", ") || "none"}.`, ); return model; } -function check(tools, { spec, cfgFile, cfgWithoutRules, rules }, work, expected) { +function check(tools, model, { work, out }, expected) { + const { spec, cfgFile, cfgWithoutRules, rules, properties } = model; + const started = Date.now(); + let runs = 0; + const run = (cfg, file, options) => { + runs++; + return tlc(tools, spec, cfg, file, options); + }; const name = path.basename(spec, ".tla"); const tlcDir = path.join(work, "tlc"); const dot = path.join(tlcDir, `${name}.dot`); - tlc(tools, spec, cfgWithoutRules, path.join(tlcDir, name), dot); + // One worker writes the graph in a fixed order, which breaks ties between equally short paths. + run(cfgWithoutRules, path.join(tlcDir, name), { dump: dot }); warnUnnamedSteps(spec, cfgWithoutRules, dot); - console.log(`TLC on ${path.basename(spec)}:`); + console.log(`TLC on ${path.basename(spec)} with ${rel(cfgFile)}:`); if (rules.length === 0) - console.log(` ${path.basename(cfgFile)} has no INVARIANT, so no rule is checked.`); + console.log( + ` ${path.basename(cfgFile)} has no INVARIANT, so ${properties.length ? "the chart marks no state broken" : "no rule is checked"}.`, + ); + 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`; - const broken = /^Error: Invariant /m.test(tlc(tools, spec, cfg, file)); + let result = run(cfg, file, { workers: "auto" }); + // Several workers can reach a bad state by a longer path first. One worker searches breadth + // first in a fixed order, so the chart's bug paths are the shortest, and the same every run. + if (/^Error: Invariant /m.test(result.stdout)) result = run(cfg, file); + const broken = /^Error: Invariant /m.test(result.stdout); + console.log(said(rule, broken)); + if (result.warning) console.error(`${shown(`${file}.out`)}: ${result.warning}`); + return { file: `${file}.out`, rule, broken }; + }); + const temporal = properties.map((property) => { + const file = path.join(tlcDir, `${name}-${property}`); + const { stdout } = run(`${cfgWithoutRules}PROPERTY ${property}\n`, file, { workers: "auto" }); + const broken = BROKEN_PROPERTY.test(stdout); console.log( - ` ${rule} ${broken ? (expected.has(rule) ? "is broken (expected)" : "is broken") : "holds"}.`, + `${said(property, broken)}${broken ? ` The chart draws only INVARIANT rules, so read TLC's counterexample in ${shown(`${file}.out`)}.` : ""}`, ); - return { file: `${file}.out`, rule, broken }; + return { file: `${file}.out`, rule: property, broken }; }); - return { spec, dot, traces, broken: traces.some((t) => t.broken) }; + const seconds = ((Date.now() - started) / 1000).toFixed(1); + console.log(` TLC ran ${runs} ${runs === 1 ? "time" : "times"} in ${seconds} s.`); + const broken = [...traces, ...temporal].some((t) => t.broken); + return { spec, dot, traces, properties: temporal, broken }; } function rulesAsExpected(now, other, expected) { - const brokenIn = (m) => (m?.traces ?? []).filter((t) => t.broken).map((t) => t.rule); + const brokenIn = (m) => + [...(m?.traces ?? []), ...(m?.properties ?? [])].filter((t) => t.broken).map((t) => t.rule); if (expected.size === 0) return !now.broken && !other?.broken; const unexpected = [...new Set([...brokenIn(now), ...brokenIn(other)])].filter( (r) => !expected.has(r), @@ -354,9 +467,20 @@ function rulesAsExpected(now, other, expected) { return !unexpected.length && !holds.length; } -const SCAFFOLD = (name, graph) => { - const vars = Object.keys([...graph.nodes.values()][0]?.vars ?? {}); - const actions = [...new Set([...graph.edges, ...graph.loops].map((e) => e.action))].sort(); +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. + const actions = [ + ...new Set( + text + .split(/\n(?=\S)/) + .map((d) => /^(\w+)\s*(?:\([^)]*\))?\s*==([^]*)/.exec(d)) + .filter((d) => d && /[\w)\]>}]'|\bUNCHANGED\b/.test(d[2])) + .map((d) => d[1]), + ), + ].sort(); return `// Chart labels for ${name}, for statechart.mjs. Write labels in plain words, not variable or action names. // v, before, and after map each variable to its value. Strings, numbers, and booleans keep their kind. // Sequences, tuples, and sets become arrays, indexed from 0. Records and functions become objects. @@ -416,7 +540,7 @@ export function step(action, before, after) { `; }; -async function draw({ now, other, map, work, out, title, comparing }) { +async function draw({ now, other, uncited, map, work, out, title, comparing }) { const shown = published(work, out); const mapping = await import(pathToFileURL(path.resolve(map)).href); const from = ["--dot", now.dot, "--map", map, "--spec", now.spec]; @@ -424,7 +548,10 @@ async function draw({ now, other, map, work, out, title, comparing }) { if (other) { from.push(`--${other.role}-dot`, other.dot, "--spec", other.spec); from.push(...other.traces.flatMap((t) => [`--${other.role}-traces`, t.file])); + if (other.traces.length) + from.push(`--${other.role}-rules`, other.traces.map((t) => t.rule).join(",")); if (other.label !== undefined) from.push("--label", other.label); + if (other.listed) from.push("--listed", JSON.stringify(other.listed)); } if (comparing) from.push("--full-labels", "--flat"); else if (mapping.readerActions?.length) from.push("--cover"); @@ -455,6 +582,8 @@ async function draw({ now, other, map, work, out, title, comparing }) { map, ); const summary = JSON.parse(fs.readFileSync(files.summary, "utf8")); + if (uncited) + fs.writeFileSync(files.summary, `${JSON.stringify({ ...summary, uncited }, null, 2)}\n`); const charts = [files.overview]; for (const c of summary.classes) { const views = typeof mapping.detail === "function" ? ["", "-developer", "-layered"] : [""]; @@ -496,7 +625,7 @@ async function draw({ now, other, map, work, out, title, comparing }) { console.log( summary.classes.length ? fs.readFileSync(files.stories, "utf8").trimEnd() - : "No rule is broken.", + : "No state breaks a rule.", ); return { files, charts }; } @@ -522,6 +651,7 @@ function render(charts, shown) { } function finish({ work, out, inputs }, { files, charts }, ok, png) { + unchanged(inputs, out); const pngs = png ? render(charts, published(work, out)) : []; publish(work, out, inputs); const written = [...charts, ...pngs, files.stories, files.summary] @@ -584,7 +714,9 @@ async function inWorkFolder(body) { try { return await body(work); } catch (e) { - keep = e instanceof TlcStopped; + keep = e instanceof TlcStopped || e instanceof NotPublished; + if (e instanceof NotPublished) + e.message += ` The files that this run wrote are in ${rel(work)}.`; throw e; } finally { if (!keep) fs.rmSync(work, { recursive: true, force: true }); @@ -597,10 +729,33 @@ const moved = (from, to, ...missed) => { return true; } catch (e) { if (missed.includes(e.code)) return false; + 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. + if (!fs.existsSync(from) && missed.includes("ENOENT")) return false; + if (fs.existsSync(to)) { + if (fs.readdirSync(to).length && missed.includes("ENOTEMPTY")) return false; + fs.rmdirSync(to); + } + try { + fs.cpSync(from, to, { recursive: true, errorOnExist: true, force: false }); + } catch (e) { + fs.rmSync(to, { recursive: true, force: true }); throw e; } + fs.rmSync(from, { recursive: true, force: true }); + return true; }; +function unchanged(inputs, out) { + const changed = [...inputs].find(([f, was]) => fingerprint(f) !== was)?.[0]; + if (changed) + throw new NotPublished( + `${rel(changed)} changed while this run read it, so the run left ${rel(out)} as it was. Run the command again.`, + ); +} + function publish(work, out, inputs) { const parent = path.dirname(path.resolve(out)); fs.mkdirSync(parent, { recursive: true }); @@ -609,11 +764,7 @@ function publish(work, out, inputs) { let aside = false; try { fs.cpSync(work, next, { recursive: true }); - const changed = [...inputs].find(([f, was]) => fingerprint(f) !== was)?.[0]; - if (changed) - throw new CannotFinish( - `${rel(changed)} changed while this run read it, so the run left ${rel(out)} as it was. Run the command again.`, - ); + unchanged(inputs, out); refuseForeign(out); while (!moved(next, out, "ENOTEMPTY", "EEXIST")) { if (aside) { @@ -629,12 +780,12 @@ function publish(work, out, inputs) { fs.rmSync(next, { recursive: true, force: true }); const why = e instanceof CannotFinish ? e.message : `cannot replace ${rel(out)}: ${e.message}.`; if (!back) - throw new CannotFinish( + throw new NotPublished( `${why} This run moved the previous ${rel(out)} to ${rel(old)} and could not put it back.`, ); - throw e instanceof CannotFinish - ? e - : new CannotFinish(`${why} The run left ${rel(out)} as it was.`); + throw new NotPublished( + e instanceof CannotFinish ? why : `${why} The run left ${rel(out)} as it was.`, + ); } if (aside) fs.rmSync(old, { recursive: true, force: true }); } @@ -647,7 +798,17 @@ function putBack(old, out) { } } -function secondModel(input, { fixed, against, label }) { +function secondCfg(cfg, flags) { + if (flags["fixed-config"] && !flags.fixed) + throw new CannotFinish(`--fixed-config needs --fixed. ${more("from-spec")}`); + if (flags["against-config"] && !flags.against) + throw new CannotFinish(`--against-config needs --against. ${more("from-spec")}`); + if (flags.fixed) + return flags["fixed-config"] ?? (fs.existsSync(cfgOf(flags.fixed)) ? cfgOf(flags.fixed) : cfg); + return flags.against && (flags["against-config"] ?? cfgOf(flags.against)); +} + +function secondModel(input, cfg, { fixed, against, label }) { if (fixed && against) throw new CannotFinish(`use --fixed or --against, not both. ${more("from-spec")}`); if (!fixed && !against) { @@ -663,33 +824,90 @@ function secondModel(input, { fixed, against, label }) { throw new CannotFinish( `${rel(spec)} needs its own file and module name, such as ${name}${fixed ? "Fixed" : "Agreed"}.tla.`, ); - const cfg = fs.existsSync(cfgOf(spec)) ? cfgOf(spec) : cfgOf(input); - return { role, label, model: readModel(spec, cfg) }; + return { role, label, model: readModel(spec, cfg, `--${role}-config`) }; +} + +function warnUnchecked(now, other) { + const unchecked = now.rules.filter((r) => !other.rules.includes(r)); + if (unchecked.length) + console.error( + `${rel(other.cfgFile)} does not check ${unchecked.join(", ")}, so the stories cannot say whether ${path.basename(other.spec)} keeps ${unchecked.length === 1 ? "it" : "them"}.`, + ); +} + +// 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(); + const modules = files.filter((f) => f.endsWith(".tla") && !f.includes("_TTrace_")); + const only = modules.length === 1 ? path.basename(modules[0], ".tla") : undefined; + const breaks = {}; + let headed = false; + for (const f of files.filter((f) => f.endsWith(".cfg"))) { + const cfg = fs.readFileSync(path.join(dir, f), "utf8"); + const module = /^\\\* module:[ \t]*(\w+)[ \t]*$/m.exec(cfg)?.[1] ?? only; + const expect = /^\\\* expect:[ \t]*(\w+)[ \t]*$/m.exec(cfg)?.[1]; + if (module !== path.basename(spec, ".tla") || !expect) continue; + headed = true; + if (!/^(pass|deadlock)$|^error/.test(expect)) breaks[f] = expect; + } + return headed ? { spec: path.basename(spec), breaks } : null; +} + +function warnUnlisted(now, other) { + if (other.listed || !now.traces.some((t) => t.broken)) return; + const module = path.basename(other.spec, ".tla"); + console.error( + `No config beside ${rel(other.spec)} has an "\\* expect:" line for ${module}, so the stories cannot say whether ${module} already lists each bug. When ${path.basename(other.spec)} is a copy, pass the spec in its own folder.`, + ); +} + +function warnUncited(models) { + return Object.fromEntries( + models.map(({ spec, traces, properties }) => { + const found = uncitedConditions(fs.readFileSync(spec, "utf8")); + const held = [...traces, ...properties].filter((t) => !t.broken).map((t) => t.rule); + const short = (s) => (s.length > 90 ? `${s.slice(0, 87)}...` : s); + if (found.length && held.length) + console.error( + `${rel(spec)}: ${joinAnd(held)} ${held.length === 1 ? "holds" : "hold"}, but a rule can also hold because the model waits for a condition that the code does not check. No comment gives the file and line of the code that checks ${found.length === 1 ? "this condition" : "these conditions"}:\n${found.map((c) => ` ${rel(spec)}:${c.line} ${c.action}: ${short(c.condition)}`).join("\n")}\nPut that file and line in a comment on each condition, as in \\* pay.ts:120, or remove the condition when no code checks it.`, + ); + return [path.basename(spec), found]; + }), + ); } async function fromSpec(input, { "expect-broken": expected, ...flags }) { const name = path.basename(input, ".tla"); const map = flags.map ?? path.join(path.dirname(input), `${name}.map.mjs`); - const secondSpec = flags.fixed ?? flags.against; - const inputs = snapshot([input, cfgOf(input), map, secondSpec, secondSpec && cfgOf(secondSpec)]); - const second = secondModel(input, flags); - const tools = findTools(); - const model = readInput(input, expected); + const cfg = flags.config ?? cfgOf(input); + const otherCfg = secondCfg(cfg, flags); + const inputs = snapshot([input, cfg, map, flags.fixed ?? flags.against, otherCfg]); + const second = secondModel(input, otherCfg, flags); + const model = readInput(input, cfg, expected); const out = outDir(flags.out, input, name); + if (!fs.existsSync(map)) { + fs.writeFileSync(map, SCAFFOLD(name, input)); + throw new CannotFinish(`Wrote ${rel(map)}. Fill in its labels, then run this command again.`); + } + const tools = findTools(); return inWorkFolder(async (work) => { - const now = check(tools, model, work, expected); - if (!fs.existsSync(map)) { - fs.writeFileSync(map, SCAFFOLD(name, parseDot(fs.readFileSync(now.dot, "utf8")))); - throw new CannotFinish( - `\nWrote ${rel(map)}. Fill in its labels, then run this command again.`, - ); - } + const now = check(tools, model, { work, out }, expected); const other = second && { role: second.role, label: second.label, - ...check(tools, second.model, work, expected), + listed: second.role === "against" ? listedBreaks(second.model.spec) : undefined, + ...check(tools, second.model, { work, out }, expected), }; - const drawn = await draw({ now, other, map, work, out, title: flags.title }); + let uncited; + if (second) { + warnUnchecked(model, second.model); + if (second.role === "against") warnUnlisted(now, other); + uncited = warnUncited(second.role === "fixed" ? [now, other] : [now]); + } + const drawn = await draw({ now, other, uncited, map, work, out, title: flags.title }); return finish({ work, out, inputs }, drawn, rulesAsExpected(now, other, expected), flags.png); }); } @@ -713,10 +931,10 @@ async function fromChart(input, { "expect-broken": expected, ...flags }) { } snapshot([spec, cfgOf(spec), map], inputs); const tools = findTools(); - const model = readInput(spec, expected); + const model = readInput(spec, cfgOf(spec), expected); const out = outDir(flags.out, input, name); return inWorkFolder(async (work) => { - const now = check(tools, model, work, expected); + const now = check(tools, model, { work, out }, expected); const drawn = await draw({ now, map, work, out, title: flags.title, comparing: true }); const compared = script("compare-charts.mjs", [input, drawn.files.overview], input, { okExits: [0, 1], diff --git a/plugins/pstack/skills/statechart/scripts/test/statechart.test.mjs b/plugins/pstack/skills/statechart/scripts/test/statechart.test.mjs index a90c7e4a..28d1c3d9 100644 --- a/plugins/pstack/skills/statechart/scripts/test/statechart.test.mjs +++ b/plugins/pstack/skills/statechart/scripts/test/statechart.test.mjs @@ -23,19 +23,23 @@ import { parseValue, ruleSentences, stateKey, + uncitedConditions, } from "../lib.mjs"; const here = dirname(fileURLToPath(import.meta.url)); const scripts = dirname(here); const fixture = (name) => readFileSync(join(here, name), "utf8"); const edges = (r) => r.transitions.map((t) => `${t.from} -> ${t.to} : ${t.label}`).sort(); -const node = (script, args, cwd, env = {}) => - spawnSync(process.execPath, [join(scripts, script), ...args], { +const node = (script, args, cwd, env = {}) => { + const r = spawnSync(process.execPath, [join(scripts, script), ...args], { cwd, encoding: "utf8", env: { ...process.env, ...env }, timeout: 120_000, }); + r.stdout = r.stdout?.replace(/^( {2}TLC ran \d+ times? in )\d+\.\d s\.$/gm, "$1N s."); + return r; +}; test("a transition on a composite leaves from every state inside it", () => { const { regions } = parseMermaid(fixture("upload.mmd")); @@ -109,6 +113,38 @@ Bare == TRUE assert.equal(stateKey({ b: 1, a: { d: 2, c: [3] } }), stateKey({ a: { c: [3], d: 2 }, b: 1 })); }); +test("an action's condition on a variable that the action does not change needs a file and line", () => { + const found = uncitedConditions(`---- MODULE Pay ---- +CONSTANT MaxAge +VARIABLES screen, sent, + paid, clock +Ready == sent > 0 +Tick == clock' = clock + 1 /\\ UNCHANGED <> +Pay == + /\\ screen = "Cart \\* not a comment" + /\\ MaxAge > 0 + /\\ clock < MaxAge (* pay.ts:120 *) + /\\ Ready + \\* checkout.ts:88 + /\\ sent < 3 + /\\ screen' = IF clock > 0 /\\ sent > 0 THEN "Paid" ELSE screen /\\ paid' = TRUE + /\\ UNCHANGED <> +\\* fill.ts:10 +Fill == \\E o \\in 1..3 : /\\ paid = TRUE + /\\ clock > 0 /\\ sent' = o + 1 + /\\ sent = o + /\\ paid => clock > 0 /\\ screen = "Cart" + /\\ UNCHANGED <> +Next == Tick \\/ Pay \\/ Fill +====`); + assert.deepEqual(found, [ + { line: 11, action: "Pay", condition: "Ready" }, + { line: 17, action: "Fill", condition: "paid = TRUE" }, + { line: 18, action: "Fill", condition: "clock > 0" }, + { line: 20, action: "Fill", condition: 'paid => clock > 0 /\\ screen = "Cart"' }, + ]); +}); + test("the legend is not part of the machine", () => { const { regions } = parseMermaid(`stateDiagram-v2 state "Legend" as legend { @@ -290,6 +326,58 @@ test("TLC output from a run that failed or stopped early is refused", () => { ); }); +const tlcThrew = (cls, message) => `Error: Evaluating invariant Small failed. +Index 123 out of bounds for length 4 +Error: TLC threw an unexpected exception. +This was probably caused by an error in the spec or model. +See the User Output or TLC Console for clues to what happened. +The exception was a ${cls} +: ${message} +Error: The error occurred when TLC was evaluating the nested +expressions at the following positions: + The error call stack is empty. +`; +const smallBroken = + "Error: Invariant Small is violated.\nError: The behavior up to this point is:\nState 1: \nx = 0\n\n"; +const stoppedEarly = "9 states generated, 9 distinct states found, 4 states left on queue.\n"; + +test("a rule that TLC finds broken before TLC throws a Java exception keeps its paths, with a warning", () => { + const aioobe = "java.lang.ArrayIndexOutOfBoundsException: Index 123 out of bounds for length 4"; + const oneWorker = `${smallBroken}Error: Invariant Small is violated.\n${tlcThrew( + "java.lang.ArrayIndexOutOfBoundsException", + "Index 123 out of bounds for length 4", + )}\n${stoppedEarly}`; + assert.equal( + checkTlcOutput(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"), + /failed with java\.lang\.ArrayIndexOutOfBoundsException: Index 123/, + ); + assert.deepEqual( + parseTraces(workersInterleaved).map((t) => t.invariant), + ["Small"], + ); + assert.throws( + () => + checkTlcOutput( + `${smallBroken}${tlcThrew("java.lang.RuntimeException", "util.Assert$TLCRuntimeException: Attempted to apply tuple")}${stoppedEarly}`, + "formula.out", + ), + /formula\.out: TLC stopped on an error that is not a broken rule: Evaluating invariant Small failed\./, + ); + assert.throws( + () => + checkTlcOutput( + `${tlcThrew("java.lang.ArrayIndexOutOfBoundsException", "Index 123 out of bounds for length 4")}${stoppedEarly}`, + "never-broken.out", + ), + /not a broken rule: Evaluating invariant Small failed\./, + ); +}); + test("a step that changes nothing keeps a state unsettled, and a quote in a reader label survives the chart", () => { const dir = mkdtempSync(join(tmpdir(), "statechart-")); writeFileSync( @@ -713,7 +801,7 @@ const NO_TLC = `Cannot find TLC. Download tla2tools.jar from a TLA+ release: Then set TLA2TOOLS to the path of tla2tools.jar, and JAVA to a java binary (Java 11 or later). `; const FROM_SPEC_USAGE = - "node statechart.mjs from-spec SPEC.tla [--fixed FIXED.tla | --against AGREED.tla] [--label TEXT] [--map FILE] [--expect-broken RULE]... [--title TEXT] [--out DIR] [--png]"; + "node statechart.mjs from-spec SPEC.tla [--config FILE] [--fixed FIXED.tla [--fixed-config FILE] | --against AGREED.tla [--against-config FILE]] [--label TEXT] [--map FILE] [--expect-broken RULE]... [--title TEXT] [--out DIR] [--png]"; const FROM_CHART_USAGE = "node statechart.mjs from-chart CHART.mmd [--module NAME] [--expect-broken RULE]... [--title TEXT] [--out DIR] [--png]"; const noTlc = { TLA2TOOLS: "", JAVA: "" }; @@ -989,13 +1077,14 @@ test("from-chart checks the agreed chart and draws it back unchanged", needsTlc, assert.equal( r.stdout, `Wrote Upload.tla, Upload.cfg, and Upload.map.mjs from upload.mmd. -TLC on Upload.tla: +TLC on Upload.tla with Upload.cfg: TypeOK holds. + TLC ran 2 times in N s. Chart: 5 states and 8 transitions from 5 model states. 5 work, 0 break a rule. -No rule is broken. +No state breaks a rule. The spec draws upload.mmd back unchanged. @@ -1031,9 +1120,10 @@ test("from-chart finds the design bug, and from-spec with the fix marks it fixed assert.equal( today.stdout, `Wrote Sync.tla, Sync.cfg, and Sync.map.mjs from sync.mmd. -TLC on Sync.tla: +TLC on Sync.tla with Sync.cfg: TypeOK holds. NeverSyncedWhileOffline is broken. + TLC ran 4 times in N s. Chart: 4 states and 8 transitions from 4 model states. 3 work, 1 breaks a rule. @@ -1059,12 +1149,14 @@ Wrote chart.mmd, bug-1.mmd, stories.md, summary.json in Sync-statechart. assert.equal(fixed.status, 1, fixed.stderr); assert.equal( fixed.stdout, - `TLC on Sync.tla: + `TLC on Sync.tla with Sync.cfg: TypeOK holds. NeverSyncedWhileOffline is broken. -TLC on SyncFixed.tla: + TLC ran 4 times in N s. +TLC on SyncFixed.tla with Sync.cfg: TypeOK holds. NeverSyncedWhileOffline holds. + TLC ran 3 times in N s. Chart: 4 states and 9 transitions from 4 model states. 3 work today, 0 still wrong with the fix, 1 fixed or new with the fix. @@ -1113,14 +1205,15 @@ Wrote chart.mmd, bug-1.mmd, stories.md, summary.json in Sync-statechart. assert.equal( coded.stdout, `Kept Sync.tla. Delete it to write the spec again from sync.mmd. -TLC on Sync.tla: +TLC on Sync.tla with Sync.cfg: TypeOK holds. NeverSyncedWhileOffline holds. + TLC ran 3 times in N s. Chart: 3 states and 5 transitions from 3 model states. 3 work, 0 break a rule. -No rule is broken. +No state breaks a rule. The spec does not draw sync.mmd: states only in EXPECTED (no path from the start reaches them in the spec, or the spec renamed them): @@ -1216,6 +1309,126 @@ export const step = (action) => ({ Pay: "you pay", Charge: "the bank charges you export const cause = () => "each charge request charges again"; `; +test( + "from-spec checks each PROPERTY in its own TLC run, and names the counterexample of a broken one", + needsTlc, + () => { + const dir = mkdtempSync(join(tmpdir(), "statechart-")); + writeFileSync( + join(dir, "Pay.tla"), + pay("Pay", `screen = "Paying" /\\ charges = 0 /\\ charges' = 1 /\\ UNCHANGED screen`).replace( + "====", + 'ChargedAtMostOnce == [](charges <= 1)\nEventuallyPaying == <>(screen = "Paying")\n====', + ), + ); + writeFileSync( + join(dir, "Pay.cfg"), + "SPECIFICATION Spec\nINVARIANT NoDoubleCharge\nPROPERTIES ChargedAtMostOnce EventuallyPaying\n", + ); + writeFileSync(join(dir, "Pay.map.mjs"), payMap); + const r = node("statechart.mjs", ["from-spec", "Pay.tla"], dir); + assert.equal(r.status, 1, r.stderr); + assert.equal( + r.stdout.split("\n\n")[0], + `TLC on Pay.tla with Pay.cfg: + NoDoubleCharge holds. + ChargedAtMostOnce holds. + EventuallyPaying is broken. The chart draws only INVARIANT rules, so read TLC's counterexample in ${join("Pay-statechart", "tlc", "Pay-EventuallyPaying.out")}. + TLC ran 4 times in N s.`, + ); + assert.match(r.stdout, /\nNo state breaks a rule\.\n/); + const tlcDir = join(dir, "Pay-statechart", "tlc"); + assert.match( + readFileSync(join(tlcDir, "Pay-EventuallyPaying.out"), "utf8"), + /^Error: Temporal properties were violated\./m, + ); + assert.deepEqual( + readdirSync(tlcDir) + .filter((f) => f.endsWith(".cfg") && /PROPERT/.test(readFileSync(join(tlcDir, f), "utf8"))) + .sort(), + ["Pay-ChargedAtMostOnce.cfg", "Pay-EventuallyPaying.cfg"], + ); + const expected = node( + "statechart.mjs", + ["from-spec", "Pay.tla", "--expect-broken", "EventuallyPaying"], + dir, + ); + assert.equal(expected.status, 0, expected.stderr); + assert.match(expected.stdout, /\n {2}EventuallyPaying is broken \(expected\)\. /); + }, +); + +test( + "from-spec checks a rule that the config lists as both PROPERTY and INVARIANT once, as the INVARIANT, and charts its bug", + needsTlc, + () => { + const dir = mkdtempSync(join(tmpdir(), "statechart-")); + writeFileSync( + join(dir, "Pay.tla"), + pay( + "Pay", + `screen = "Paying" /\\ charges < 2 /\\ charges' = charges + 1 /\\ UNCHANGED screen`, + ), + ); + writeFileSync( + join(dir, "Pay.cfg"), + "SPECIFICATION Spec\nPROPERTY NoDoubleCharge\nINVARIANT NoDoubleCharge\n", + ); + writeFileSync(join(dir, "Pay.map.mjs"), payMap); + const r = node("statechart.mjs", ["from-spec", "Pay.tla"], dir); + assert.equal(r.status, 1, r.stderr); + assert.equal( + r.stdout.split("\n\n")[0], + `TLC on Pay.tla with Pay.cfg: + NoDoubleCharge is broken. + TLC ran 3 times in N s.`, + ); + assert.match(r.stdout, /\nRule broken: `NoDoubleCharge`\n/); + assert.equal( + r.stdout.split("\n").at(-2), + "Wrote chart.mmd, bug-1.mmd, stories.md, summary.json in Pay-statechart.", + ); + const unknown = node( + "statechart.mjs", + ["from-spec", "Pay.tla", "--expect-broken", "Nope"], + dir, + ); + assert.match(unknown.stderr, /, whose rules are NoDoubleCharge\.\n/); + }, +); + +test("from-spec reports a broken PROPERTY in each form that TLC reports it in", needsTlc, () => { + const dir = mkdtempSync(join(tmpdir(), "statechart-")); + writeFileSync( + join(dir, "Pay.tla"), + pay( + "Pay", + `screen = "Paying" /\\ charges < 2 /\\ charges' = charges + 1 /\\ UNCHANGED screen`, + ).replace( + "====", + `ChargedAtMostOnce == [](charges <= 1)\nNeverChargedAgain == [][charges' <= 1]_charges\nStartsPaying == screen = "Paying"\n====`, + ), + ); + writeFileSync( + join(dir, "Pay.cfg"), + "SPECIFICATION Spec\nPROPERTIES ChargedAtMostOnce NeverChargedAgain StartsPaying\n", + ); + writeFileSync(join(dir, "Pay.map.mjs"), payMap); + const r = node("statechart.mjs", ["from-spec", "Pay.tla"], dir); + assert.equal(r.status, 1, r.stderr); + const broken = (p) => + ` ${p} is broken. The chart draws only INVARIANT rules, so read TLC's counterexample in ${join("Pay-statechart", "tlc", `Pay-${p}.out`)}.`; + assert.equal( + r.stdout.split("\n\n")[0], + `TLC on Pay.tla with Pay.cfg: + Pay.cfg has no INVARIANT, so the chart marks no state broken. +${broken("ChargedAtMostOnce")} +${broken("NeverChargedAgain")} +${broken("StartsPaying")} + TLC ran 4 times in N s.`, + ); +}); + test( "a state reached only after a bug takes the bug's color, and the fix edge leaves the state before the changed step", needsTlc, @@ -1274,7 +1487,15 @@ test( "Refunded, charged": "wrong", }); - const withFix = [...args, "--fixed-dot", "PayFixed.dot", "--fixed-traces", "PayFixed.out"]; + const withFix = [ + ...args, + "--fixed-dot", + "PayFixed.dot", + "--fixed-traces", + "PayFixed.out", + "--fixed-rules", + "NoDoubleCharge", + ]; assert.equal(node("tlc-to-chart.mjs", withFix, dir).status, 0); const chart = readFileSync(join(dir, "chart.mmd"), "utf8"); assert.deepEqual(statusOf(chart), { @@ -1301,7 +1522,7 @@ test( ); test( - "from-spec writes a mapping to fill in, then draws each bug in every view the mapping has", + "a rule that the second model does not check reads not checked, and a rule it checks reads unchanged", needsTlc, () => { const dir = mkdtempSync(join(tmpdir(), "statechart-")); @@ -1312,22 +1533,78 @@ test( `screen = "Paying" /\\ charges < 2 /\\ charges' = charges + 1 /\\ UNCHANGED screen`, ), ); + writeFileSync(join(dir, "Pay.cfg"), "SPECIFICATION Spec\nINVARIANT NoDoubleCharge\n"); + writeFileSync(join(dir, "pay.map.mjs"), payMap); + assert.match(tlc(dir, "Pay").stdout, /Invariant NoDoubleCharge is violated/); + const story = (...extra) => { + const r = node( + "tlc-to-chart.mjs", + [ + ...["--dot", "Pay.dot", "--map", "pay.map.mjs", "--traces", "Pay.out"], + ...["--against-dot", "Pay.dot", ...extra, "--story", "story.md", "--out", "chart.mmd"], + ], + dir, + ); + assert.equal(r.status, 0, r.stderr); + return readFileSync(join(dir, "story.md"), "utf8"); + }; + assert.match( + story(), + /^In the spec you see the same screens and steps, but the spec does not check this rule\.$/m, + ); + assert.match( + story("--against-traces", "Pay.out", "--against-rules", "NoDoubleCharge"), + /^In the spec you see the same screens and steps, so the spec does not change this path\.$/m, + ); + const alone = node( + "tlc-to-chart.mjs", + [ + "--dot", + "Pay.dot", + "--map", + "pay.map.mjs", + "--against-dot", + "Pay.dot", + "--against-traces", + "Pay.out", + ], + dir, + ); + assert.equal(alone.status, 2); + assert.match(alone.stderr, /^--against-traces and --against-rules go together\./); + }, +); + +test( + "from-spec writes a mapping to fill in, then draws each bug in every view the mapping has", + needsTlc, + () => { + const dir = mkdtempSync(join(tmpdir(), "statechart-")); + writeFileSync( + join(dir, "Pay.tla"), + pay( + "Pay", + `screen = "Paying" /\\ charges < 2 /\\ charges' = charges + 1 /\\ UNCHANGED screen`, + ).replace("Next ==", 'Wait == screen = "Paying" /\\ UNCHANGED vars\nNext =='), + ); writeFileSync( join(dir, "Pay.cfg"), "SPECIFICATION Spec\n\\* The reader's rule.\nINVARIANTS\n NoDoubleCharge\n", ); - const first = node("statechart.mjs", ["from-spec", "Pay.tla"], dir); + const first = node("statechart.mjs", ["from-spec", "Pay.tla"], dir, { + TLA2TOOLS: join(dir, "no-tlc.jar"), + }); assert.equal(first.status, 2); - assert.equal(first.stdout, "TLC on Pay.tla:\n NoDoubleCharge is broken.\n"); + assert.equal(first.stdout, ""); assert.equal( first.stderr, - "\nWrote Pay.map.mjs. Fill in its labels, then run this command again.\n", + "Wrote Pay.map.mjs. Fill in its labels, then run this command again.\n", ); const scaffold = readFileSync(join(dir, "Pay.map.mjs"), "utf8"); assert.match(scaffold, /^\/\/ Variables: screen, charges\.$/m); assert.match( scaffold, - /^const STEPS = \{\n\tCharge: "Charge",\n\tPay: "Pay",\n\tRefund: "Refund",\n\};$/m, + /^const STEPS = \{\n\tCharge: "Charge",\n\tPay: "Pay",\n\tRefund: "Refund",\n\tWait: "Wait",\n\};$/m, ); assert.equal(existsSync(join(dir, "Pay-statechart")), false); @@ -1339,8 +1616,9 @@ test( assert.equal(r.status, 1, r.stderr); assert.equal( r.stdout, - `TLC on Pay.tla: + `TLC on Pay.tla with Pay.cfg: NoDoubleCharge is broken. + TLC ran 3 times in N s. Chart: 5 states and 4 transitions from 5 model states. 3 work, 2 break a rule. @@ -1469,6 +1747,8 @@ test( "EditFixed.dot", "--fixed-traces", "EditFixed.out", + "--fixed-rules", + "NoLostEdit", ]; const r = node( "tlc-to-chart.mjs", @@ -1629,20 +1909,22 @@ export const step = (a) => ({ Save: "you press Save", Retry: "the app tries agai export const cause = () => "the app stops after one retry and shows Saved anyway"; `, ); + const base = [ + "from-spec", + "SaveCode.tla", + "--against", + "SaveAgreed.tla", + "--label", + "the agreed chart", + ]; + const noCfg = node("statechart.mjs", base, dir); + assert.equal(noCfg.status, 2); + assert.equal( + noCfg.stderr, + "SaveAgreed.cfg does not exist. Pass --against-config with the config to check SaveAgreed.tla with. The configs beside it: SaveCode.cfg.\n", + ); const run = (...extra) => - node( - "statechart.mjs", - [ - "from-spec", - "SaveCode.tla", - "--against", - "SaveAgreed.tla", - "--label", - "the agreed chart", - ...extra, - ], - dir, - ); + node("statechart.mjs", [...base, "--against-config", "SaveCode.cfg", ...extra], dir); const unknown = run("--expect-broken", "NoLostNote"); assert.equal(unknown.status, 2); @@ -1655,12 +1937,14 @@ export const cause = () => "the app stops after one retry and shows Saved anyway assert.equal(expected.status, 0, expected.stderr); assert.equal( expected.stdout, - `TLC on SaveCode.tla: + `TLC on SaveCode.tla with SaveCode.cfg: TypeOK holds. NoFalseSaved is broken (expected). -TLC on SaveAgreed.tla: + TLC ran 4 times in N s. +TLC on SaveAgreed.tla with SaveCode.cfg: TypeOK holds. NoFalseSaved holds. + TLC ran 3 times in N s. Chart: 4 states and 4 transitions from 10 model states. 3 work, 1 breaks a rule, 0 only in the agreed chart. @@ -1682,6 +1966,14 @@ Broken as expected: NoFalseSaved. Wrote chart.mmd, bug-1.mmd, stories.md, summary.json in SaveCode-statechart. `, ); + const uncitedWarning = `SaveCode.tla: TypeOK holds, but a rule can also hold because the model waits for a condition that the code does not check. No comment gives the file and line of the code that checks these conditions: + SaveCode.tla:8 Retry: screen = "Saving" + SaveCode.tla:9 TimeOut: retries = 1 +Put that file and line in a comment on each condition, as in \\* pay.ts:120, or remove the condition when no code checks it. +`; + const warnings = `No config beside SaveAgreed.tla has an "\\* expect:" line for SaveAgreed, so the stories cannot say whether SaveAgreed already lists each bug. When SaveAgreed.tla is a copy, pass the spec in its own folder. +${uncitedWarning}`; + assert.equal(expected.stderr, warnings); const out = join(dir, "SaveCode-statechart"); const chart = readFileSync(join(out, "chart.mmd"), "utf8"); assert.match(chart, /^stateDiagram-v2\n {2}%% second model \(against\): the agreed chart\n/m); @@ -1704,6 +1996,13 @@ Wrote chart.mmd, bug-1.mmd, stories.md, summary.json in SaveCode-statechart. assert.deepEqual(summary.second.lacks.sort(), ["note.rev", "retries"]); assert.equal(summary.classes[0].against, "Saving, draft"); assert.deepEqual(summary.codeLike, []); + assert.deepEqual(summary.uncited, { + "SaveCode.tla": [ + { line: 8, action: "Retry", condition: 'screen = "Saving"' }, + { line: 9, action: "TimeOut", condition: "retries = 1" }, + ], + }); + assert.equal(summary.second.listed, undefined); const unexpected = run(); assert.equal(unexpected.status, 1, unexpected.stderr); @@ -1731,6 +2030,92 @@ Wrote chart.mmd, bug-1.mmd, stories.md, summary.json in SaveCode-statechart. coded.stdout, /These labels or causes read like code\. Write them in the reader's words in code\.map\.mjs:\n {2}retryCount hit maxRetries\n/, ); + + writeFileSync( + join(dir, "rev.map.mjs"), + readFileSync(join(dir, "SaveCode.map.mjs"), "utf8").replace( + "${v.note.text}`", + "${v.note.text} r${v.note.rev}`", + ), + ); + const lacks = run("--map", "rev.map.mjs", "--expect-broken", "NoFalseSaved"); + assert.equal(lacks.status, 2); + assert.equal( + lacks.stderr, + `${warnings}rev.map.mjs: the agreed chart has no note.rev, and the mapping reads v.note.rev on its states. Label states and steps only from what both models have, or test "rev" in v.note first.\n`, + ); + writeFileSync( + join(dir, "rev.map.mjs"), + readFileSync(join(dir, "SaveCode.map.mjs"), "utf8").replace( + "${v.note.text}`", + '${v.note.text}${"rev" in v.note ? ` r${v.note.rev}` : ""}`', + ), + ); + const tested = run("--map", "rev.map.mjs", "--expect-broken", "NoFalseSaved"); + assert.equal(tested.status, 0, tested.stderr); + + writeFileSync( + join(dir, "SaveBoth.cfg"), + "SPECIFICATION Spec\nINVARIANT TypeOK\nINVARIANT NoFalseSaved\nPROPERTY NoFalseSaved\n", + ); + const both = node( + "statechart.mjs", + [ + ...base, + "--config", + "SaveBoth.cfg", + "--against-config", + "SaveBoth.cfg", + "--expect-broken", + "NoFalseSaved", + ], + dir, + ); + assert.equal(both.status, 0, both.stderr); + assert.equal(both.stderr, warnings); + + writeFileSync(join(dir, "SaveAgreedType.cfg"), "SPECIFICATION Spec\nINVARIANT TypeOK\n"); + const unchecked = node( + "statechart.mjs", + [...base, "--against-config", "SaveAgreedType.cfg", "--expect-broken", "NoFalseSaved"], + dir, + ); + assert.equal(unchecked.status, 0, unchecked.stderr); + assert.match( + unchecked.stdout, + /^TLC on SaveAgreed\.tla with SaveAgreedType\.cfg:\n {2}TypeOK holds\.\n/m, + ); + assert.equal( + unchecked.stderr, + `SaveAgreedType.cfg does not check NoFalseSaved, so the stories cannot say whether SaveAgreed.tla keeps it.\n${warnings}`, + ); + + const listedCfg = (rule) => + writeFileSync( + join(dir, "SaveAgreedBug.cfg"), + `\\* module: SaveAgreed\n\\* expect: ${rule}\nSPECIFICATION Spec\nINVARIANT ${rule}\n`, + ); + listedCfg("NoFalseSaved"); + const known = run("--expect-broken", "NoFalseSaved"); + assert.equal(known.status, 0, known.stderr); + assert.equal(known.stderr, uncitedWarning); + assert.match( + known.stdout, + /\nWhy: .*\nListed: SaveAgreedBug\.cfg, a config of SaveAgreed\.tla, expects TLC to break this rule\.\n/, + ); + const listedSummary = JSON.parse(readFileSync(join(out, "summary.json"), "utf8")); + assert.deepEqual(listedSummary.second.listed, { + spec: "SaveAgreed.tla", + breaks: { "SaveAgreedBug.cfg": "NoFalseSaved" }, + }); + assert.deepEqual(listedSummary.classes[0].listed, ["SaveAgreedBug.cfg"]); + listedCfg("TypeOK"); + const fresh = run("--expect-broken", "NoFalseSaved"); + assert.equal(fresh.status, 0, fresh.stderr); + assert.match( + fresh.stdout, + /\nNot listed: no config of SaveAgreed\.tla expects TLC to break this rule\. Its configs expect TLC to break `TypeOK`\.\n/, + ); }, ); @@ -2455,7 +2840,11 @@ test( writeSlowPay(dir, 200, "Receipt"); const second = node("statechart.mjs", ["from-spec", "Pay.tla"], dir); - process.kill(-first.child.pid, "SIGKILL"); + try { + process.kill(-first.child.pid, "SIGKILL"); + } catch (error) { + if (error.code !== "ESRCH") throw error; + } assert.equal(second.status, 0, second.stderr); for (const file of ["chart.mmd", join("tlc", "Pay.dot")]) { const text = readFileSync(join(out, file), "utf8"); @@ -2478,10 +2867,10 @@ const changedMidRun = async ({ wrap = [], env = {} }) => { const [paid, receipt] = await Promise.all([first.done, second.done]); assert.equal(receipt.status, 0, receipt.stderr); assert.equal(paid.status, 2, paid.stderr); - assert.equal( - paid.stderr, - "Pay.tla changed while this run read it, so the run left Pay-statechart as it was. Run the command again.\n", + const [, kept] = paid.stderr.match( + /^Pay\.tla changed while this run read it, so the run left Pay-statechart as it was\. Run the command again\. The files that this run wrote are in (tmp-a\/statechart-\w+)\.\n$/, ); + assert.match(readFileSync(join(dir, kept, "chart.mmd"), "utf8"), /Paid/); const chart = readFileSync(join(out, "chart.mmd"), "utf8"); assert.match(chart, /Receipt/); assert.doesNotMatch(chart, /Paid/); @@ -2538,9 +2927,9 @@ test( writeFileSync(join(out, "notes.md"), "mine\n"); const r = await run.done; assert.equal(r.status, 2); - assert.equal( + assert.match( r.stderr, - "Pay-statechart has a file that this command did not write: notes.md. A run puts its files in place of the whole output folder, so pass --out with a new folder.\n", + /^Pay-statechart has a file that this command did not write: notes\.md\. A run puts its files in place of the whole output folder, so pass --out with a new folder\. The files that this run wrote are in tmp\/statechart-\w+\.\n$/, ); assert.deepEqual(readdirSync(out), ["notes.md"]); assert.deepEqual(staged(dir), []); @@ -2552,12 +2941,18 @@ const failRenames = `#define _GNU_SOURCE #include #include #include +#include static size_t hits; int rename(const char *from, const char *to) { static int (*real)(const char *, const char *); if (!real) real = dlsym(RTLD_NEXT, "rename"); const char *base = strrchr(to, '/'), *fails = getenv("RENAME_FAILS"); + const char *cannot = getenv("RENAME_CANNOT"); base = base ? base + 1 : to; + if (cannot && strstr(base, "shared")) { + errno = strcmp(cannot, "EXDEV") == 0 ? EXDEV : access(to, F_OK) == 0 ? EISDIR : ENOSYS; + return -1; + } if (fails && strcmp(base, "shared") == 0 && hits < strlen(fails)) { errno = fails[hits++] == 'N' ? ENOTEMPTY : EIO; return -1; @@ -2588,17 +2983,17 @@ test( const back = run("NI"); assert.equal(back.status, 2, back.stderr); - assert.match( - back.stderr, - /^cannot replace shared: EIO: .*\. The run left shared as it was\.\n$/, + const [, kept] = back.stderr.match( + /^cannot replace shared: EIO: .*\. The run left shared as it was\. The files that this run wrote are in (\/\S+)\.\n$/, ); + assert.equal(readFileSync(join(kept, "chart.mmd"), "utf8"), chart); assert.equal(readFileSync(join(shared, "chart.mmd"), "utf8"), chart); assert.deepEqual(staged(dir), []); const stuck = run("NII"); assert.equal(stuck.status, 2, stuck.stderr); const named = stuck.stderr.match( - /^cannot replace shared: EIO: .*\. This run moved the previous shared to (\.shared-\w+-old) and could not put it back\.\n$/, + /^cannot replace shared: EIO: .*\. This run moved the previous shared to (\.shared-\w+-old) and could not put it back\. The files that this run wrote are in \/\S+\.\n$/, ); assert.ok(named, stuck.stderr); const aside = named[1]; @@ -2608,6 +3003,112 @@ test( }, ); +test( + "a run on a filesystem that cannot rename copies its files into place", + { skip: needsTlc.skip || (!failingRenames && "cannot compile a rename preload") }, + () => { + const dir = mkdtempSync(join(tmpdir(), "statechart-")); + writeLamp(dir); + const args = ["from-spec", "Lamp.tla", "--out", "shared"]; + for (const [cannot, label] of [ + ["ENOSYS", "you flip the switch"], + ["EXDEV", "you press the switch"], + ["ENOSYS", "you tap the switch"], + ]) { + writeFileSync( + join(dir, "Lamp.map.mjs"), + `export const state = (v) => (v.on ? "On" : "Off");\nexport const step = () => "${label}";\n`, + ); + const r = node("statechart.mjs", args, dir, { + LD_PRELOAD: failingRenames, + RENAME_CANNOT: cannot, + }); + assert.equal(r.status, 0, r.stderr); + assert.match(readFileSync(join(dir, "shared", "chart.mmd"), "utf8"), new RegExp(label)); + assert.deepEqual(staged(dir), []); + } + }, +); + +test( + "a run whose input changes before --png renders stops before it renders, and keeps its files", + needsTlc, + async () => { + const dir = mkdtempSync(join(tmpdir(), "statechart-")); + writeSlowPay(dir, 20000); + const bin = ownTmp(dir, "bin"); + const rendered = join(dir, "rendered"); + writeFileSync(join(bin, "npx"), `#!/bin/sh\ntouch "${rendered}"\nexit 1\n`, { mode: 0o755 }); + const tmp = ownTmp(dir, "tmp"); + const run = startRun(dir, { + args: ["from-spec", "Pay.tla", "--png"], + env: { TMPDIR: tmp, PATH: `${bin}${delimiter}${process.env.PATH}` }, + }); + await until(() => tlcStarted(tmp)); + const map = join(dir, "Pay.map.mjs"); + writeFileSync(map, `${readFileSync(map, "utf8")}// edited\n`); + const r = await run.done; + assert.equal(r.status, 2, r.stderr); + const [, kept] = r.stderr.match( + /^Pay\.map\.mjs changed while this run read it, so the run left Pay-statechart as it was\. Run the command again\. The files that this run wrote are in (tmp\/statechart-\w+)\.\n$/, + ); + assert.ok(existsSync(join(dir, kept, "chart.mmd"))); + assert.equal(existsSync(rendered), false); + }, +); + +test( + "a rule that TLC finds broken before TLC throws a Java exception is broken, and the run draws the paths TLC printed", + needsTlc, + () => { + const dir = mkdtempSync(join(tmpdir(), "statechart-")); + writeFileSync( + join(dir, "Pay.tla"), + pay( + "Pay", + `screen = "Paying" /\\ charges < 2 /\\ charges' = charges + 1 /\\ UNCHANGED screen`, + ), + ); + writeFileSync(join(dir, "Pay.cfg"), "SPECIFICATION Spec\nINVARIANT NoDoubleCharge\n"); + writeFileSync(join(dir, "Pay.map.mjs"), payMap); + writeFileSync( + join(dir, "crash.txt"), + `Error: Invariant NoDoubleCharge is violated.\n${tlcThrew( + "java.lang.ArrayIndexOutOfBoundsException", + "Index 123 out of bounds for length 4", + ).replaceAll("Small", "NoDoubleCharge")}\n${stoppedEarly}`, + ); + const java = join(dir, "java"); + writeFileSync( + java, + `#!/bin/sh +"$REAL_JAVA" "$@" > "$0.$$.out"; s=$? +if grep -q '^Error: Invariant' "$0.$$.out"; then + sed '/^Model checking completed/,$d' "$0.$$.out"; cat "$CRASH"; s=75 +else + cat "$0.$$.out" +fi +rm "$0.$$.out" +exit $s +`, + { mode: 0o755 }, + ); + const r = node( + "statechart.mjs", + ["from-spec", "Pay.tla", "--expect-broken", "NoDoubleCharge"], + dir, + { JAVA: java, TLA2TOOLS: tools.jar, REAL_JAVA: tools.java, CRASH: join(dir, "crash.txt") }, + ); + assert.equal(r.status, 0, r.stderr); + assert.match(r.stdout, /^ {2}NoDoubleCharge is broken \(expected\)\.$/m); + assert.match( + r.stderr, + /^Pay-statechart\/tlc\/Pay-NoDoubleCharge\.out: TLC found that NoDoubleCharge is broken, and then failed with java\.lang\.ArrayIndexOutOfBoundsException: Index 123 out of bounds for length 4\. .* Do not weaken NoDoubleCharge because of it\./m, + ); + assert.match(r.stdout, /^## 1\. Paying, charged twice$/m); + }, +); + test( "each TLC run writes the standard modules in its own temp folder, so overlapping runs cannot rewrite them under each other", needsTlc, @@ -2643,7 +3144,7 @@ exit $s for (const line of runs) { const [folder, parsed] = line.split(": "); assert.ok(folder.startsWith(join(tmp, "tlc-")), line); - assert.equal(parsed, `Parsing file ${join(folder, "Naturals.tla")}`); + assert.ok(parsed.startsWith(`Parsing file ${folder}/`), line); folders.add(folder); } assert.equal(folders.size, runs.length); @@ -2739,7 +3240,7 @@ test( dir, ); assert.equal(r.status, 0, r.stdout + r.stderr); - assert.match(r.stdout, /\nNo rule is broken\.\n/); + assert.match(r.stdout, /\nNo state breaks a rule\.\n/); for (const [i, [rule, guard, without, story]] of [ [ "ChartsOneSpec", diff --git a/plugins/pstack/skills/statechart/scripts/tlc-to-chart.mjs b/plugins/pstack/skills/statechart/scripts/tlc-to-chart.mjs index ccb68fd7..005c9ef7 100644 --- a/plugins/pstack/skills/statechart/scripts/tlc-to-chart.mjs +++ b/plugins/pstack/skills/statechart/scripts/tlc-to-chart.mjs @@ -13,6 +13,7 @@ import { groupClassDef, groupColorProblem, isRecord, + joinAnd, joinLabels, parseDot, parseMermaid, @@ -52,16 +53,30 @@ statechart.mjs runs it once for the overview and once for each bug chart. the reader acts. --traces FILE TLC output that holds counterexamples. Repeat it. TLC -continue gives one per bad state. It refuses a file from a TLC run that stopped early or hit - an error other than a broken rule. + an error other than a broken rule. When TLC found a rule broken and then + failed with a Java exception, it keeps the paths that TLC printed and + warns that the chart can miss states that break the rule. --fixed-dot FILE The state graph of the model with the open fix. Each bug's steps replay on it. --fixed-traces FILE TLC output for the same invariants on the fixed model. Repeat it. It marks states fixed or still wrong, and adds the bugs that only the fixed model has after the current model's bugs. + --fixed-rules LIST The invariants that the fixed model's TLC runs check, as in A,B. It goes + with --fixed-traces. A rule that the fixed model does not check stays + as wrong as it is today, and its stories say "not checked". --against-dot FILE The state graph of the spec that the current code must follow. Each bug's steps replay on it. Do not use it with --fixed-dot. --against-traces FILE TLC output for the spec. Repeat it. Its bugs are drawn wrong, and the bugs that only the spec has number after the code's bugs. + --against-rules LIST The invariants that the spec's TLC runs check. It goes with + --against-traces. Stories of a rule that the spec does not check say + "not checked". + --listed JSON What the spec's configs expect, as in + {"spec":"Spec.tla","breaks":{"A.cfg":"Rule"}}: each config whose + "\\* expect:" line names a rule, and that rule. It goes with + --against-dot. Each story then says whether a config of the spec already + expects TLC to break its rule, and summary.json has second.listed and + each bug's listed configs. --label TEXT The name of the second model in the chart and the stories. Default: "the fix" with --fixed-dot, "the spec" with --against-dot. --spec FILE A TLA+ file whose \\* comment lines above a rule are the rule's sentence in @@ -100,10 +115,11 @@ take a step that the reader sees. The second model may have other variables and actions than the current model. Variables and record fields that one start state has and the other does not are left out when the two models -are compared. The second model's states take the current model's start values for the variables -it does not have, so one mapping draws both. A step of an action that the second model does not -have is skipped when it changes no shared variable, and matches any step to the same shared state -when it does. +are compared. One mapping draws both models, so it may read only what both have. The command +stops when the mapping reads a variable or field of the current model on a state of the second +model that lacks it. Test "name" in v first to label such a state another way. A step of an +action that the second model does not have is skipped when it changes no shared variable, and +matches any step to the same shared state when it does. In the customer view, states whose labels read "context: progress" with the same context sit in one box named context, and each shows only its progress. A context with one state stays a plain @@ -148,8 +164,9 @@ Writes only the files that --out, --story, and --summary name. Exit codes 0 It wrote the chart. - 1 It cannot use an input: a mapping without state(), TLC output that it refuses, or a - --highlight with no such bug. The error says why. + 1 It cannot use an input: a mapping without state(), a mapping that reads what the second + model lacks, TLC output that it refuses, or a --highlight with no such bug. The error says + why. 2 A bad argument.`; const more = "Run node tlc-to-chart.mjs --help for the flags."; @@ -157,6 +174,8 @@ const args = { traces: [], fixedTraces: [], againstTraces: [], + fixedRules: [], + againstRules: [], specs: [], view: "customer", highlight: 1, @@ -172,8 +191,11 @@ for (let i = 2; i < process.argv.length; i++) { else if (a === "--traces") args.traces.push(next()); else if (a === "--fixed-dot") args.fixedDot = next(); else if (a === "--fixed-traces") args.fixedTraces.push(next()); + else if (a === "--fixed-rules") args.fixedRules.push(...next().split(",")); else if (a === "--against-dot") args.againstDot = next(); else if (a === "--against-traces") args.againstTraces.push(next()); + else if (a === "--against-rules") args.againstRules.push(...next().split(",")); + else if (a === "--listed") args.listed = next(); else if (a === "--label") args.label = next(); else if (a === "--spec") args.specs.push(next()); else if (a === "--view") args.view = next(); @@ -204,6 +226,29 @@ if (!["customer", "developer", "layered"].includes(args.view)) if (args.fixedDot && args.againstDot) fail("use --fixed-dot or --against-dot, not both."); if (args.fixedTraces.length && !args.fixedDot) fail("--fixed-traces needs --fixed-dot."); if (args.againstTraces.length && !args.againstDot) fail("--against-traces needs --against-dot."); +if (!args.fixedTraces.length !== !args.fixedRules.length) + fail("--fixed-traces and --fixed-rules go together. The rules are what those TLC runs check."); +if (!args.againstTraces.length !== !args.againstRules.length) + fail( + "--against-traces and --against-rules go together. The rules are what those TLC runs check.", + ); +if (args.listed !== undefined) { + if (!args.againstDot) + fail("--listed says what the spec's configs expect; it needs --against-dot."); + const shape = `--listed must be JSON such as {"spec":"Spec.tla","breaks":{"A.cfg":"Rule"}}`; + try { + args.listed = JSON.parse(args.listed); + } catch (e) { + fail(`${shape}: ${e.message}.`); + } + const { spec, breaks } = isRecord(args.listed) ? args.listed : {}; + if ( + typeof spec !== "string" || + !isRecord(breaks) || + Object.values(breaks).some((r) => typeof r !== "string") + ) + fail(`${shape}.`); +} if (args.label !== undefined && !args.fixedDot && !args.againstDot) fail("--label names the second model; it needs --fixed-dot or --against-dot."); if (args.proof && !args.regions) fail("--proof writes the regions proof; it needs --regions."); @@ -292,23 +337,31 @@ function omit(vars, paths) { } return out; } -function fill(vars, paths, from) { - if (!paths.length) return vars; - const out = structuredClone(vars); - for (const p of paths) { - const [o, f] = [holder(out, p), holder(from, p)]; - if (o && f && p.at(-1) in f) o[p.at(-1)] = structuredClone(f[p.at(-1)]); - } - return out; +function guard(vars, paths, at = "v") { + if (!paths.length || !isRecord(vars)) return vars; + const missing = new Set(); + const deeper = new Map(); + for (const [k, ...rest] of paths) + if (!rest.length) missing.add(k); + else deeper.set(k, [...(deeper.get(k) ?? []), rest]); + return new Proxy(vars, { + get(target, k) { + if (missing.has(k) && !(k in target)) { + const name = `${at}.${k}`.slice(2); + throw new Error( + `${L} has no ${name}, and the mapping reads ${at}.${k} on its states. Label states and steps only from what both models have, or test "${k}" in ${at} first.`, + ); + } + return deeper.has(k) ? guard(target[k], deeper.get(k), `${at}.${k}`) : target[k]; + }, + }); } -function modelOf(graph, lookup = (vars) => vars) { +function modelOf(graph) { const byId = new Map([...graph.nodes.keys()].map((id) => [id, new Set()])); for (const e of [...graph.edges, ...graph.loops]) byId.get(e.from).add(e.action); - const index = new Map( - [...graph.nodes.values()].map((n) => [stateKey(n.raw ?? n.vars), byId.get(n.id)]), - ); - const facts = (vars) => factsFrom(index.get(stateKey(lookup(vars))) ?? new Set()); + const index = new Map([...graph.nodes.values()].map((n) => [stateKey(n.vars), byId.get(n.id)])); + const facts = (vars) => factsFrom(index.get(stateKey(vars)) ?? new Set()); return { graph, facts, @@ -356,16 +409,17 @@ const secondGraph = secondDot ? parseDot(fs.readFileSync(secondDot, "utf8")) : n const secondInit = secondGraph && [...secondGraph.nodes.values()].find((n) => n.init).vars; const lacks = secondGraph ? lacking(mainInit, secondInit) : []; const extra = secondGraph ? lacking(secondInit, mainInit) : []; -const secondFilled = secondGraph && { - ...secondGraph, - nodes: new Map( - [...secondGraph.nodes].map(([id, n]) => [ - id, - { ...n, raw: n.vars, vars: fill(n.vars, lacks, mainInit) }, - ]), - ), -}; -const second = secondFilled && modelOf(secondFilled, (vars) => omit(vars, lacks)); +const second = + secondGraph && + modelOf({ + ...secondGraph, + nodes: new Map( + [...secondGraph.nodes].map(([id, n]) => [ + id, + { ...n, raw: n.vars, vars: guard(n.vars, lacks) }, + ]), + ), + }); const secondQ = second && quotient(second); function readerPath(trace, key, labelOf = stepLabel) { @@ -461,18 +515,19 @@ function replaySecond(trace) { .filter((t) => t.invariant === trace.invariant) .map((t) => stateKey(t.steps[t.steps.length - 1].vars)), ); - const ruleHolds = - secondTraceFiles.length > 0 && ![...passed].some((id) => bad.has(stateKey(nodeOf(id).vars))); - return { sameEnd: true, ruleHolds }; + const checked = secondRules.has(trace.invariant); + const ruleHolds = checked && ![...passed].some((id) => bad.has(stateKey(nodeOf(id).vars))); + return { sameEnd: true, checked, ruleHolds }; } function readTraces(files, paths = []) { return files.flatMap((f) => { const text = fs.readFileSync(f, "utf8"); - checkTlcOutput(text, f); + const warning = checkTlcOutput(text, f); + if (warning) console.error(`${f}: ${warning}`); return parseTraces(text).map((t) => ({ ...t, - steps: t.steps.map((s) => ({ ...s, vars: fill(s.vars, paths, mainInit) })), + steps: t.steps.map((s) => ({ ...s, vars: guard(s.vars, paths) })), })); }); } @@ -497,6 +552,7 @@ function firstBad(raw) { } const rawTraces = readTraces(args.traces); const secondTraceFiles = role === "fix" ? args.fixedTraces : args.againstTraces; +const secondRules = new Set(role === "fix" ? args.fixedRules : args.againstRules); const rawSecondTraces = readTraces(secondTraceFiles, lacks); const traces = firstBad(rawTraces); const secondTraces = firstBad(rawSecondTraces); @@ -592,12 +648,13 @@ function badKeys(m, keys, raw) { return out; } const badNow = badKeys(main, now.keys, rawTraces); -const badSecond = - second && secondTraceFiles.length > 0 - ? badKeys(second, secondQ.keys, rawSecondTraces) - : role === "fix" - ? badNow - : new Set(); +const uncheckedTraces = rawTraces.filter((t) => !secondRules.has(t.invariant)); +const badSecond = second + ? new Set([ + ...badKeys(second, secondQ.keys, rawSecondTraces), + ...(role === "fix" ? badKeys(main, now.keys, uncheckedTraces) : []), + ]) + : new Set(); const allNodes = new Set([...now.nodes, ...(secondQ?.nodes ?? [])]); const initial = new Set([...now.initial, ...(secondQ?.initial ?? [])]); const onlySecond = (k) => second && !now.nodes.has(k); @@ -1229,9 +1286,11 @@ function secondLine(c) { const s = c.second; if (!s) return null; if (s.sameEnd) - return s.ruleHolds - ? `${W} ${L} you see the same screens and steps, yet the rule holds, so the state labels do not show what ${L} changes.` - : `${W} ${L} you see the same screens and steps, so ${L} does not change this path.`; + return !s.checked + ? `${W} ${L} you see the same screens and steps, but ${L} does not check this rule.` + : s.ruleHolds + ? `${W} ${L} you see the same screens and steps, yet the rule holds, so the state labels do not show what ${L} changes.` + : `${W} ${L} you see the same screens and steps, so ${L} does not change this path.`; if (s.reason) return `${cap(L)} cannot take these steps: it ${s.reason}.`; const outcome = s.disabled ? "cannot happen, so you stay at" @@ -1244,6 +1303,16 @@ function secondLine(c) { } return `${W} ${L}, step ${s.step} (${s.said}) ${outcome}: ${show(s.key)}.`; } +const listedIn = (c) => + Object.keys(args.listed.breaks).filter((cfg) => args.listed.breaks[cfg] === c.invariant); +function listedLine(c) { + const { spec, breaks } = args.listed; + const cfgs = listedIn(c); + if (cfgs.length) + return `Listed: ${joinAnd(cfgs)}, ${cfgs.length === 1 ? "a config" : "configs"} of ${spec}, expect${cfgs.length === 1 ? "s" : ""} TLC to break this rule.`; + const others = [...new Set(Object.values(breaks))].sort().map((r) => `\`${r}\``); + return `Not listed: no config of ${spec} expects TLC to break this rule. ${others.length ? `Its configs expect TLC to break ${joinAnd(others)}.` : "None of its configs expects TLC to break a rule."}`; +} if (args.story) { const lines = []; const header = role === "fix" ? `New with ${L}: ` : `Only in ${L}: `; @@ -1251,6 +1320,7 @@ if (args.story) { lines.push(`## ${i + 1}. ${c.introduced ? header : ""}${show(c.end)}`, ""); lines.push(`Rule broken: ${ruleOf(c)}`); if (c.cause) lines.push(`Why: ${c.cause.replace(/\.$/, "")}.`); + if (args.listed) lines.push(listedLine(c)); lines.push( c.count === 1 ? "This is the only way to get here in the model." @@ -1282,14 +1352,25 @@ const secondOf = (c) => : `only in ${L}` : c.second ? c.second.sameEnd - ? c.second.ruleHolds - ? "same screens, but the rule holds" - : "unchanged" + ? !c.second.checked + ? "same screens, rule not checked" + : c.second.ruleHolds + ? "same screens, but the rule holds" + : "unchanged" : (c.second.reason ?? show(c.second.key)) : null; const summary = { view: args.view, - ...(role ? { second: { role, label: L, lacks: lacks.map((p) => p.join(".")) } } : {}), + ...(role + ? { + second: { + role, + label: L, + lacks: lacks.map((p) => p.join(".")), + ...(args.listed ? { listed: args.listed } : {}), + }, + } + : {}), modelStates: graph.nodes.size, modelTransitions: graph.edges.length, chartStates: regions?.mermaid ? regions.states[0] + regions.states[1] : flatStates.size, @@ -1331,6 +1412,7 @@ const summary = { modelSteps: c.trace.steps.length, counterexamples: c.count, [role ?? "fix"]: secondOf(c), + ...(args.listed ? { listed: listedIn(c) } : {}), })), codeLike, }; diff --git a/tools/upstream.json b/tools/upstream.json index 34975295..560ce623 100644 --- a/tools/upstream.json +++ b/tools/upstream.json @@ -4,7 +4,7 @@ "pstack": { "upstreamPath": "pstack", "localPath": "plugins/pstack", - "sha": "eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10", + "sha": "7698375f92a729f8bb89d113c633dce9ff9dc6db", "exclude": [ ".cursor-plugin/", ".gitignore", @@ -20,7 +20,7 @@ "cursor-team-kit": { "upstreamPath": "cursor-team-kit/skills", "localPath": "plugins/pstack/skills", - "sha": "eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10", + "sha": "7698375f92a729f8bb89d113c633dce9ff9dc6db", "exclude": [ "check-compiler-errors/", "control-cli/", @@ -39,7 +39,7 @@ "thermos": { "upstreamPath": "thermos", "localPath": "plugins/pstack", - "sha": "eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10", + "sha": "7698375f92a729f8bb89d113c633dce9ff9dc6db", "exclude": [ ".cursor-plugin/", "CHANGELOG.md", From 2d8b487c9cc9190a6abdfc9b51ba047fe8011922 Mon Sep 17 00:00:00 2001 From: Christian Bager Bach Houmann Date: Thu, 22 Oct 2026 20:14:16 +0200 Subject: [PATCH 2/4] Release 2.0.0-rc.18: docs, notices, and manifests VERSION, the manifests, and package.json move to 2.0.0-rc.18. CHANGES.md gets the entry with its behavior-delta table. NOTICE.md, NOTICE-skills.md, poteto-mode's copy of the notice, and the README point at upstream 7698375, and the README's pinned installer command names the new tag. The skill count stays at 65. --- .claude-plugin/marketplace.json | 2 +- CHANGES.md | 13 +++++++++++++ NOTICE-skills.md | 6 +++--- NOTICE.md | 6 +++--- README.md | 4 ++-- VERSION | 2 +- package.json | 2 +- plugins/pstack/.claude-plugin/plugin.json | 2 +- plugins/pstack/.codex-plugin/plugin.json | 2 +- .../poteto-mode/references/licenses/NOTICE.md | 6 +++--- 10 files changed, 29 insertions(+), 16 deletions(-) diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json index de888ed9..e6ecbc7f 100644 --- a/.claude-plugin/marketplace.json +++ b/.claude-plugin/marketplace.json @@ -10,7 +10,7 @@ "name": "t3-pstack", "source": "./plugins/pstack", "description": "pstack for T3 Code: rigorous agent workflows whose panels and fan-outs run across model families through T3. Original pstack by Lauren Tan (poteto).", - "version": "2.0.0-rc.17" + "version": "2.0.0-rc.18" } ] } diff --git a/CHANGES.md b/CHANGES.md index ef2bd4b5..df2cc7d6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,19 @@ This file is the release changelog, with one `## - ` entry per release, newest first. The Cursor-to-T3 rewrite rules live in [`tools/substitutions.json`](tools/substitutions.json), and the [sync boundary](CONTRIBUTING.md#the-sync-boundary) in `CONTRIBUTING.md` defines how a change to upstream's skill content is declared. +## 2.0.0-rc.18 - Lauren's `7698375`: statechart stops on inputs it used to chart wrong without saying so + +t3-pstack moves to Lauren Tan's pstack at cursor/plugins `7698375` for all three components. Only pstack changed upstream, only in the `statechart` skill, and its version stays at 0.15.30 ([pstack #776](https://github.com/cursor/plugins/pull/776)). Before this, a run could draw a wrong chart or exit with the wrong code and not say so. The label map now stops on a variable or field that the `--fixed` or `--against` model lacks, where it used to give it the current model's start value. New `--config`, `--fixed-config`, and `--against-config` flags name each model's config. The agreed spec is never checked with the code model's config, and a missing config stops the run and lists the configs beside the spec. A rule the agreed config does not check reads "not checked" in the stories, where they used to say the agreed spec keeps it. When TLC finds a broken rule and then throws a Java exception, the run keeps the paths TLC printed, marks the rule broken, and warns that the charts can miss states. On a file system that cannot rename into the output folder (`ENOSYS`, `EXDEV`, or `EISDIR`, as on FUSE mounts), it copies the files into place. TLC checks each rule with one worker per CPU and checks a broken rule again with one worker, which gives the shortest paths. Each `PROPERTY` gets its own TLC run, `--expect-broken` accepts it, and a rule listed as both `INVARIANT` and `PROPERTY` is checked once. With `--against`, each story says whether a config beside the agreed spec expects the bug. With `--fixed` or `--against`, the run lists each condition of an action that no `\* file:line` comment ties to code. `SKILL.md` asks for those citations, says what a valid replay is, and asks the hand-off to say whether the spec already lists each bug. The test of each TLC run's temp folder accepts `Naturals.tla` anywhere under it, where TLC 1.8.0 puts it. `bun tools/sync.mjs` updated `SKILL.md`, `lib.mjs`, `statechart.mjs`, `tlc-to-chart.mjs`, and the test file cleanly, and each is byte-identical to upstream. No substitution, fork, or hook changed, and the 15 declared forks are untouched. With TLC 1.7.4 on Linux and Node 20, 66 of the 67 skill tests pass and the PID-namespace test skips. With the TLC 1.8.0 prerelease, the `PROPERTY` test fails because 1.8.0 words a broken temporal property as "Temporal property X was violated.", which the scripts do not read yet, as #776 says. Without TLC, 29 pass and 38 skip. The README's skill count stays at 65. #776's copies under `harness/pstack/claude-code/` sit outside every synced component. At `7698375` each component's dry run reports no undeclared fork, no denylist hit, and no substitution that matches nothing. Neither hooks file changes. + +| Change | 2.0.0-rc.17 | 2.0.0-rc.18 | Source | +| --- | --- | --- | --- | +| A label map that reads a variable the `--fixed` or `--against` model lacks | Uses the current model's start value. | Stops and names it. | pstack #776 | +| The config `--against` checks the agreed spec with | `AGREED.cfg`, or the code model's `SPEC.cfg` when there is none. | `AGREED.cfg` or `--against-config`, never the code model's. `--config` and `--fixed-config` name the others. | pstack #776 | +| A rule the agreed config does not check | The stories say the agreed spec keeps it. | The stories say "not checked". | pstack #776 | +| TLC throws after it finds a broken rule | The run stops on TLC's error. | The run keeps the printed paths, marks the rule broken, and warns. | pstack #776 | +| An output folder that cannot take a rename, as on FUSE | Publishing fails. | The files are copied into place. | pstack #776 | +| `PROPERTY` rules | Stay in every TLC run, and `--expect-broken` refuses them. | One TLC run each, and a broken one names TLC's counterexample file. | pstack #776 | + ## 2.0.0-rc.17 - Lauren's `eb4db2b`: a skill that draws a TLA+ model as a statechart a PM can read t3-pstack moves to Lauren Tan's pstack at cursor/plugins `eb4db2b` for all three components. Only pstack changed upstream, and its version moves to 0.15.30. The new `statechart` skill draws what an app's user sees as a Mermaid statechart generated from a TLA+ model, so a PM or a designer can judge the design without reading TLA+ ([pstack #741](https://github.com/cursor/plugins/pull/741)). TLC checks each rule the PM agrees to as an invariant. Each state is gray when it works, red when it is still wrong, and green when an open fix fixes it, and each class of counterexample is drawn as a numbered path. `from-spec` draws the chart from a model, `--fixed` shows what an open fix changes, and `--against` audits the code against an existing spec. `from-chart` turns a chart the PM agreed to into a TLA+ skeleton and compares the drawn chart with it. The skill is a `SKILL.md` and about 6,000 lines of Node scripts with a bundled `OutputFolder` model and a `node:test` suite. The agent runs them with `node`, which the installer already requires. The scripts find TLC only through `TLA2TOOLS`, the path to `tla2tools.jar`, and `JAVA`, and without `TLA2TOOLS` they say where to download it and exit 2. `--png` renders each chart through `npx @mermaid-js/mermaid-cli`. It keeps Lauren's `disable-model-invocation`, so on Claude Code it runs when the user types `/t3-pstack:statechart`. On Codex it is `$t3-pstack:statechart`, and Codex ignores the flag. poteto-help gains its row. `bun tools/sync.mjs` added the skill and updated poteto-help cleanly through existing substitutions, and the 12 new files are byte-identical to upstream. The skill names no Cursor tool, path, model, command, or subagent, so no rule was added, and the 15 declared forks are untouched. A new CI job, Skill script tests, runs `node --test plugins/pstack/skills/*/scripts/test/*.test.mjs` on Node 20, the step #741 added to upstream's `validate-plugins.yml`. The runner has no TLC, so 31 of the 58 tests skip there. With TLC 1.7.4 on Linux and Node 20, 57 pass and the PID-namespace test skips. On macOS two TLC tests fail on their own assumptions, not the scripts': one compares a `/var` temp path with Java's `/private/var` form, and one needs `LD_PRELOAD`, which macOS ignores. The README's skill count moves to 65. #741's version bump, upstream's README row, its guide page under `docs/guide/`, and its copies under `harness/pstack/claude-code/` sit outside every synced component. At `eb4db2b` each component's dry run reports no undeclared fork, no denylist hit, and no substitution that matches nothing. Neither hooks file changes. diff --git a/NOTICE-skills.md b/NOTICE-skills.md index 0bdc380d..7ce56ca5 100644 --- a/NOTICE-skills.md +++ b/NOTICE-skills.md @@ -4,9 +4,9 @@ This plugin contains MIT-licensed work from six sources. The copyright notices a | Included work | Upstream | Copyright | License | | --- | --- | --- | --- | -| The pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10/pstack) | (c) 2026 Lauren Tan | [MIT](LICENSE) | -| `deslop`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, and `what-did-i-get-done` | [cursor/plugins/cursor-team-kit](https://github.com/cursor/plugins/tree/eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10/cursor-team-kit) | (c) 2026 Cursor | [MIT](LICENSE-cursor-team-kit) | -| `thermos`, `thermo-nuclear-review`, `thermo-nuclear-code-quality-review`, and the `thermo-nuclear-review-subagent` and `thermo-nuclear-code-quality-review-subagent` definitions | [cursor/plugins/thermos](https://github.com/cursor/plugins/tree/eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10/thermos) | (c) 2026 Cursor | [MIT](LICENSE-thermos) | +| The pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/pstack) | (c) 2026 Lauren Tan | [MIT](LICENSE) | +| `deslop`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, and `what-did-i-get-done` | [cursor/plugins/cursor-team-kit](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/cursor-team-kit) | (c) 2026 Cursor | [MIT](LICENSE-cursor-team-kit) | +| `thermos`, `thermo-nuclear-review`, `thermo-nuclear-code-quality-review`, and the `thermo-nuclear-review-subagent` and `thermo-nuclear-code-quality-review-subagent` definitions | [cursor/plugins/thermos](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/thermos) | (c) 2026 Cursor | [MIT](LICENSE-thermos) | | The session-start hook scripts, `read-sheet.sh`, and `reflect/scripts/find-transcript.mjs`, which t3-pstack modified, and four `poteto-mode` rules, the worktree and head-guard rules in the Feature, Opening a PR, and Shipping playbooks, three `watch-pr` fixes, and the ignored-file and reflog-only-commit holds in `poteto-mode/scripts/worktree-audit.sh`, which t3-pstack reworded or adapted for T3, and the plugin icon | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude) | (c) 2026 Michael Denyer | [MIT](LICENSE) | | The plain-remove prune step in the worktree-cleanup playbook, which t3-pstack adapted | [sergchil/jutsu](https://github.com/sergchil/jutsu/commit/da9442422c72cc99442c1ce3500d2f2485234a31) | (c) 2026 Sergey Chilingaryan | [MIT](LICENSE) | | `poteto-mode/scripts/resolve-codex-transcript` and `resolve-codex-transcript.ts`, which t3-pstack modified | [ericlitman/open-pstack](https://github.com/ericlitman/open-pstack/tree/c5c8e237c324359a3d1929037da78fe66da3d1ed/plugins/pstack/skills/poteto-mode/scripts), [PR #151](https://github.com/ericlitman/open-pstack/pull/151) | (c) 2026 Eric A. Litman and Donncha O'Toole | [MIT](LICENSE) | diff --git a/NOTICE.md b/NOTICE.md index 7cbc2930..180f9cca 100644 --- a/NOTICE.md +++ b/NOTICE.md @@ -6,9 +6,9 @@ t3-pstack is a port of [pstack](https://github.com/cursor/plugins/tree/main/psta | Component | Upstream | Copyright | License | License file | | --- | --- | --- | --- | --- | -| Every skill under `plugins/pstack/skills/` except those named in the next two rows, `plugins/pstack/agents/poteto-agent.md`, `plugins/pstack/agents/comment-sicko.md`, and the vendored scripts under `plugins/pstack/skills/poteto-mode/scripts/` | [cursor/plugins/pstack @ eb4db2b](https://github.com/cursor/plugins/tree/eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | -| `plugins/pstack/skills/{deslop,fix-ci,fix-merge-conflicts,get-pr-comments,make-pr-easy-to-review,what-did-i-get-done}/` | [cursor/plugins/cursor-team-kit @ eb4db2b](https://github.com/cursor/plugins/tree/eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10/cursor-team-kit) | (c) 2026 Cursor | MIT | [LICENSE-cursor-team-kit](LICENSE-cursor-team-kit) | -| `plugins/pstack/skills/{thermos,thermo-nuclear-review,thermo-nuclear-code-quality-review}/`, `plugins/pstack/agents/thermo-nuclear-review-subagent.md`, `plugins/pstack/agents/thermo-nuclear-code-quality-review-subagent.md` | [cursor/plugins/thermos @ eb4db2b](https://github.com/cursor/plugins/tree/eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10/thermos) | (c) 2026 Cursor | MIT | [LICENSE-thermos](LICENSE-thermos) | +| Every skill under `plugins/pstack/skills/` except those named in the next two rows, `plugins/pstack/agents/poteto-agent.md`, `plugins/pstack/agents/comment-sicko.md`, and the vendored scripts under `plugins/pstack/skills/poteto-mode/scripts/` | [cursor/plugins/pstack @ 7698375](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | +| `plugins/pstack/skills/{deslop,fix-ci,fix-merge-conflicts,get-pr-comments,make-pr-easy-to-review,what-did-i-get-done}/` | [cursor/plugins/cursor-team-kit @ 7698375](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/cursor-team-kit) | (c) 2026 Cursor | MIT | [LICENSE-cursor-team-kit](LICENSE-cursor-team-kit) | +| `plugins/pstack/skills/{thermos,thermo-nuclear-review,thermo-nuclear-code-quality-review}/`, `plugins/pstack/agents/thermo-nuclear-review-subagent.md`, `plugins/pstack/agents/thermo-nuclear-code-quality-review-subagent.md` | [cursor/plugins/thermos @ 7698375](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/thermos) | (c) 2026 Cursor | MIT | [LICENSE-thermos](LICENSE-thermos) | | `tools/sync.mjs`, `tools/generate.mjs`, `tools/validate-skills.mjs`, `tools/plugin.mjs`, `plugins/pstack/skills/reflect/scripts/find-transcript.mjs`, `plugins/pstack/hooks/session-start.sh`, `plugins/pstack/hooks/session-start.ps1`, `plugins/pstack/skills/setup-pstack/scripts/read-sheet.sh`, and the tests that cover them, each modified by t3-pstack | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude), as merged into t3-pstack through 1.0.14 | (c) 2026 Michael Denyer | MIT | [LICENSE](LICENSE) | | Four rules in `plugins/pstack/skills/poteto-mode/SKILL.md` (load a platform's skill before deploying, stop an abandoned agent and confirm it stopped, keep a review gate closed with no independent reviewer, the `todo.md` fallback), the per-delegate worktree rule in `playbooks/feature.md`, the stop-live-agents rule in `playbooks/opening-a-pr.md`, the `--match-head-commit` guard in `playbooks/shipping.md`, and the review-gate, stale-check, and no-checks fixes in `plugins/pstack/skills/poteto-mode/scripts/watch-pr/` with their tests in `verdicts.test.ts`, each reworded or adapted for T3 by t3-pstack | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude), pull requests [#95](https://github.com/michael-denyer/pstack-claude/pull/95), [#97](https://github.com/michael-denyer/pstack-claude/pull/97), and [#153](https://github.com/michael-denyer/pstack-claude/pull/153) for watch-pr | (c) 2026 Michael Denyer | MIT | [LICENSE](LICENSE) | | The ignored-file and reflog-only-commit holds in `plugins/pstack/skills/poteto-mode/scripts/worktree-audit.sh`, ported from JavaScript to bash, and their wording in `playbooks/worktree-cleanup.md`, with the test cases in `tests/worktree-audit.test.mjs`; the plugin icon with its C2PA manifest removed (`plugins/pstack/.claude-plugin/icon.png`, `plugins/pstack/assets/pstack-icon.png`) and `tests/image-metadata.test.mjs` | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude), pull requests [#277](https://github.com/michael-denyer/pstack-claude/pull/277) and [#271](https://github.com/michael-denyer/pstack-claude/pull/271) | (c) 2026 Michael Denyer | MIT | [LICENSE](LICENSE) | diff --git a/README.md b/README.md index e88be6bf..bd6f8d5b 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ npx -y github:chhoumann/t3-pstack update npx -y github:chhoumann/t3-pstack doctor ``` -`npx -y github:chhoumann/t3-pstack` runs the installer from the latest commit on `main`. That is the rolling channel, the same one each home's marketplace auto-updates from. To run one release's installer, name its tag, as in `npx -y github:chhoumann/t3-pstack#v2.0.0-rc.17 doctor`. +`npx -y github:chhoumann/t3-pstack` runs the installer from the latest commit on `main`. That is the rolling channel, the same one each home's marketplace auto-updates from. To run one release's installer, name its tag, as in `npx -y github:chhoumann/t3-pstack#v2.0.0-rc.18 doctor`. `install` and `update` are the same command, and a second run changes nothing. With Node 20 or later, it installs or updates the `t3-pstack@t3-pstack` plugin in every Claude Code and Codex config home T3 can run: `~/.claude` and `~/.codex`, `$CLAUDE_CONFIG_DIR` and `$CODEX_HOME`, and the home of each `claudeAgent` and `codex` instance in T3's settings, disabled ones included. Name any other home with `--claude-home <dir>` or `--codex-home <dir>`. Each home's `t3-pstack` marketplace must come from `chhoumann/t3-pstack`, or from `--source <owner/repo|git URL|dir>` on the same run, and a home whose marketplace has another source is left as it is. A local directory needs a path such as `./t3-pstack`, since `owner/repo` always means GitHub. On Codex it also trusts t3-pstack's session-start hook, once its hooks file is the one this release pins. Codex runs a plugin's hook only once it is trusted, and T3's Codex sessions never ask, so without this step the hook never runs. Run `update` after each release. @@ -34,7 +34,7 @@ The plugin carries 65 skill directories, 24 of them `principle-*` leaves, and 4 ## Staying current -This repository syncs from Lauren's tree directly, synced against upstream `eb4db2b`. `tools/upstream.json` pins each component, `tools/substitutions.json` holds the rewrite rules and a denylist of Cursor terms, and `tools/forks.json` declares every file the port keeps in its own form and why. `bun tools/sync.mjs <component> <sha>` derives each upstream file through the rules, merges it three ways with the port's copy, and fails on an undeclared fork, a denylist hit, or a rule that no longer matches upstream. [CONTRIBUTING.md](CONTRIBUTING.md#the-sync-boundary) has the details. +This repository syncs from Lauren's tree directly, synced against upstream `7698375`. `tools/upstream.json` pins each component, `tools/substitutions.json` holds the rewrite rules and a denylist of Cursor terms, and `tools/forks.json` declares every file the port keeps in its own form and why. `bun tools/sync.mjs <component> <sha>` derives each upstream file through the rules, merges it three ways with the port's copy, and fails on an undeclared fork, a denylist hit, or a rule that no longer matches upstream. [CONTRIBUTING.md](CONTRIBUTING.md#the-sync-boundary) has the details. ## Data handling diff --git a/VERSION b/VERSION index 574c49f2..ce416fd4 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -2.0.0-rc.17 +2.0.0-rc.18 diff --git a/package.json b/package.json index d16262a9..b7ad37b9 100644 --- a/package.json +++ b/package.json @@ -1,7 +1,7 @@ { "name": "t3-pstack", "private": true, - "version": "2.0.0-rc.17", + "version": "2.0.0-rc.18", "description": "The installer and development tooling for t3-pstack, Lauren Tan's pstack rewritten in place for T3 Code. The plugin itself lives in plugins/pstack.", "author": { "name": "Christian Bager Bach Houmann", diff --git a/plugins/pstack/.claude-plugin/plugin.json b/plugins/pstack/.claude-plugin/plugin.json index 7e0c3da3..42309ca9 100644 --- a/plugins/pstack/.claude-plugin/plugin.json +++ b/plugins/pstack/.claude-plugin/plugin.json @@ -1,7 +1,7 @@ { "name": "t3-pstack", "displayName": "t3-pstack (pstack for T3 Code)", - "version": "2.0.0-rc.17", + "version": "2.0.0-rc.18", "description": "pstack for T3 Code: Lauren Tan's pstack with its Cursor mechanics rewritten in place for T3, so subagents, panels, schedules, and PR watches dispatch through T3's orchestration and panels mix Claude, GPT, and Grok.", "author": { "name": "Christian Bager Bach Houmann", diff --git a/plugins/pstack/.codex-plugin/plugin.json b/plugins/pstack/.codex-plugin/plugin.json index 1071f10b..10a7b577 100644 --- a/plugins/pstack/.codex-plugin/plugin.json +++ b/plugins/pstack/.codex-plugin/plugin.json @@ -1,6 +1,6 @@ { "name": "t3-pstack", - "version": "2.0.0-rc.17", + "version": "2.0.0-rc.18", "description": "pstack for T3 Code on a Codex host: Lauren Tan's pstack with its Cursor mechanics rewritten in place for T3, so subagents, panels, schedules, and PR watches dispatch through T3's orchestration.", "author": { "name": "Christian Bager Bach Houmann", diff --git a/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.md b/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.md index 0bdc380d..7ce56ca5 100644 --- a/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.md +++ b/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.md @@ -4,9 +4,9 @@ This plugin contains MIT-licensed work from six sources. The copyright notices a | Included work | Upstream | Copyright | License | | --- | --- | --- | --- | -| The pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10/pstack) | (c) 2026 Lauren Tan | [MIT](LICENSE) | -| `deslop`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, and `what-did-i-get-done` | [cursor/plugins/cursor-team-kit](https://github.com/cursor/plugins/tree/eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10/cursor-team-kit) | (c) 2026 Cursor | [MIT](LICENSE-cursor-team-kit) | -| `thermos`, `thermo-nuclear-review`, `thermo-nuclear-code-quality-review`, and the `thermo-nuclear-review-subagent` and `thermo-nuclear-code-quality-review-subagent` definitions | [cursor/plugins/thermos](https://github.com/cursor/plugins/tree/eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10/thermos) | (c) 2026 Cursor | [MIT](LICENSE-thermos) | +| The pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/pstack) | (c) 2026 Lauren Tan | [MIT](LICENSE) | +| `deslop`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, and `what-did-i-get-done` | [cursor/plugins/cursor-team-kit](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/cursor-team-kit) | (c) 2026 Cursor | [MIT](LICENSE-cursor-team-kit) | +| `thermos`, `thermo-nuclear-review`, `thermo-nuclear-code-quality-review`, and the `thermo-nuclear-review-subagent` and `thermo-nuclear-code-quality-review-subagent` definitions | [cursor/plugins/thermos](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/thermos) | (c) 2026 Cursor | [MIT](LICENSE-thermos) | | The session-start hook scripts, `read-sheet.sh`, and `reflect/scripts/find-transcript.mjs`, which t3-pstack modified, and four `poteto-mode` rules, the worktree and head-guard rules in the Feature, Opening a PR, and Shipping playbooks, three `watch-pr` fixes, and the ignored-file and reflog-only-commit holds in `poteto-mode/scripts/worktree-audit.sh`, which t3-pstack reworded or adapted for T3, and the plugin icon | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude) | (c) 2026 Michael Denyer | [MIT](LICENSE) | | The plain-remove prune step in the worktree-cleanup playbook, which t3-pstack adapted | [sergchil/jutsu](https://github.com/sergchil/jutsu/commit/da9442422c72cc99442c1ce3500d2f2485234a31) | (c) 2026 Sergey Chilingaryan | [MIT](LICENSE) | | `poteto-mode/scripts/resolve-codex-transcript` and `resolve-codex-transcript.ts`, which t3-pstack modified | [ericlitman/open-pstack](https://github.com/ericlitman/open-pstack/tree/c5c8e237c324359a3d1929037da78fe66da3d1ed/plugins/pstack/skills/poteto-mode/scripts), [PR #151](https://github.com/ericlitman/open-pstack/pull/151) | (c) 2026 Eric A. Litman and Donncha O'Toole | [MIT](LICENSE) | From a4b216cf99725f8a784170a4f62ec638760747f2 Mon Sep 17 00:00:00 2001 From: Christian Bager Bach Houmann <christian@bagerbach.com> Date: Thu, 22 Oct 2026 20:51:53 +0200 Subject: [PATCH 3/4] Sync Lauren's pstack to 4ec7ffa (#779) All three components move from 7698375 to 4ec7ffa. Upstream changed only pstack, and only the statechart scripts (pstack #779). It deletes comments that repeat the code and renames helpers so the name carries the fact a comment held: splitComments is splitCommentsKeepingOffsets, checkTlcOutput is tlcOutputWarning, quote is escapeMermaidQuotes, luminance is wcagRelativeLuminance, and parseMermaid's declared is declaredInRegion. cited takes { above } in place of a positional flag, and one PRIMES_OR_UNCHANGED regex replaces two copies. Behavior does not change. bun tools/sync.mjs updated lib.mjs, statechart.mjs, tlc-to-chart.mjs, and the test file cleanly, and the statechart directory is byte-identical to upstream at 4ec7ffa, file modes included. No substitution, fork, or hook changed. The 15 declared forks were left alone, and cursor-team-kit and thermos synced with no file changes. Upstream's copies under harness/pstack/claude-code/ sit outside every synced component. --- .../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 ++++++----- tools/upstream.json | 6 +-- 5 files changed, 47 insertions(+), 67 deletions(-) diff --git a/plugins/pstack/skills/statechart/scripts/lib.mjs b/plugins/pstack/skills/statechart/scripts/lib.mjs index 7fad394d..49f1675b 100644 --- a/plugins/pstack/skills/statechart/scripts/lib.mjs +++ b/plugins/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(/(?<![\\.\w])([A-Za-z_]\w*)'/g)] .map((m) => 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/plugins/pstack/skills/statechart/scripts/statechart.mjs b/plugins/pstack/skills/statechart/scripts/statechart.mjs index 685b6011..0ff4255c 100644 --- a/plugins/pstack/skills/statechart/scripts/statechart.mjs +++ b/plugins/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/plugins/pstack/skills/statechart/scripts/test/statechart.test.mjs b/plugins/pstack/skills/statechart/scripts/test/statechart.test.mjs index 28d1c3d9..72782e67 100644 --- a/plugins/pstack/skills/statechart/scripts/test/statechart.test.mjs +++ b/plugins/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: <Initial predicate>\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: <Initial predicate>\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/plugins/pstack/skills/statechart/scripts/tlc-to-chart.mjs b/plugins/pstack/skills/statechart/scripts/tlc-to-chart.mjs index 005c9ef7..37ae46e3 100644 --- a/plugins/pstack/skills/statechart/scripts/tlc-to-chart.mjs +++ b/plugins/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)}`); diff --git a/tools/upstream.json b/tools/upstream.json index 560ce623..7aa22fad 100644 --- a/tools/upstream.json +++ b/tools/upstream.json @@ -4,7 +4,7 @@ "pstack": { "upstreamPath": "pstack", "localPath": "plugins/pstack", - "sha": "7698375f92a729f8bb89d113c633dce9ff9dc6db", + "sha": "4ec7ffa173eaa70d3d9467a627baf0954645a353", "exclude": [ ".cursor-plugin/", ".gitignore", @@ -20,7 +20,7 @@ "cursor-team-kit": { "upstreamPath": "cursor-team-kit/skills", "localPath": "plugins/pstack/skills", - "sha": "7698375f92a729f8bb89d113c633dce9ff9dc6db", + "sha": "4ec7ffa173eaa70d3d9467a627baf0954645a353", "exclude": [ "check-compiler-errors/", "control-cli/", @@ -39,7 +39,7 @@ "thermos": { "upstreamPath": "thermos", "localPath": "plugins/pstack", - "sha": "7698375f92a729f8bb89d113c633dce9ff9dc6db", + "sha": "4ec7ffa173eaa70d3d9467a627baf0954645a353", "exclude": [ ".cursor-plugin/", "CHANGELOG.md", From 58f7119e3e475a78b32fcdf80ed122d39850a368 Mon Sep 17 00:00:00 2001 From: Christian Bager Bach Houmann <christian@bagerbach.com> Date: Thu, 22 Oct 2026 20:54:32 +0200 Subject: [PATCH 4/4] Point rc.18's release files at 4ec7ffa (#779) The CHANGES.md entry for 2.0.0-rc.18 now names upstream 4ec7ffa in its title and links pstack #779 beside #776. It says #779 changes no behavior, names the helpers it renames, and records the test runs at 4ec7ffa: without TLC 29 pass and 38 skip, and from-spec on the bundled OutputFolder model with TLC 1.7.4 exits 0 with all five rules holding. The TLC suite numbers stay labelled as runs at 7698375. NOTICE.md, NOTICE-skills.md, poteto-mode's copy of the notice, and the README's pin point at 4ec7ffa. The version stays 2.0.0-rc.18. --- CHANGES.md | 4 ++-- NOTICE-skills.md | 6 +++--- NOTICE.md | 6 +++--- README.md | 2 +- .../pstack/skills/poteto-mode/references/licenses/NOTICE.md | 6 +++--- 5 files changed, 12 insertions(+), 12 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index df2cc7d6..43f41068 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -2,9 +2,9 @@ This file is the release changelog, with one `## <version> - <title>` entry per release, newest first. The Cursor-to-T3 rewrite rules live in [`tools/substitutions.json`](tools/substitutions.json), and the [sync boundary](CONTRIBUTING.md#the-sync-boundary) in `CONTRIBUTING.md` defines how a change to upstream's skill content is declared. -## 2.0.0-rc.18 - Lauren's `7698375`: statechart stops on inputs it used to chart wrong without saying so +## 2.0.0-rc.18 - Lauren's `4ec7ffa`: statechart stops on inputs it used to chart wrong without saying so -t3-pstack moves to Lauren Tan's pstack at cursor/plugins `7698375` for all three components. Only pstack changed upstream, only in the `statechart` skill, and its version stays at 0.15.30 ([pstack #776](https://github.com/cursor/plugins/pull/776)). Before this, a run could draw a wrong chart or exit with the wrong code and not say so. The label map now stops on a variable or field that the `--fixed` or `--against` model lacks, where it used to give it the current model's start value. New `--config`, `--fixed-config`, and `--against-config` flags name each model's config. The agreed spec is never checked with the code model's config, and a missing config stops the run and lists the configs beside the spec. A rule the agreed config does not check reads "not checked" in the stories, where they used to say the agreed spec keeps it. When TLC finds a broken rule and then throws a Java exception, the run keeps the paths TLC printed, marks the rule broken, and warns that the charts can miss states. On a file system that cannot rename into the output folder (`ENOSYS`, `EXDEV`, or `EISDIR`, as on FUSE mounts), it copies the files into place. TLC checks each rule with one worker per CPU and checks a broken rule again with one worker, which gives the shortest paths. Each `PROPERTY` gets its own TLC run, `--expect-broken` accepts it, and a rule listed as both `INVARIANT` and `PROPERTY` is checked once. With `--against`, each story says whether a config beside the agreed spec expects the bug. With `--fixed` or `--against`, the run lists each condition of an action that no `\* file:line` comment ties to code. `SKILL.md` asks for those citations, says what a valid replay is, and asks the hand-off to say whether the spec already lists each bug. The test of each TLC run's temp folder accepts `Naturals.tla` anywhere under it, where TLC 1.8.0 puts it. `bun tools/sync.mjs` updated `SKILL.md`, `lib.mjs`, `statechart.mjs`, `tlc-to-chart.mjs`, and the test file cleanly, and each is byte-identical to upstream. No substitution, fork, or hook changed, and the 15 declared forks are untouched. With TLC 1.7.4 on Linux and Node 20, 66 of the 67 skill tests pass and the PID-namespace test skips. With the TLC 1.8.0 prerelease, the `PROPERTY` test fails because 1.8.0 words a broken temporal property as "Temporal property X was violated.", which the scripts do not read yet, as #776 says. Without TLC, 29 pass and 38 skip. The README's skill count stays at 65. #776's copies under `harness/pstack/claude-code/` sit outside every synced component. At `7698375` each component's dry run reports no undeclared fork, no denylist hit, and no substitution that matches nothing. Neither hooks file changes. +t3-pstack moves to Lauren Tan's pstack at cursor/plugins `4ec7ffa` for all three components. Only pstack changed upstream, only in the `statechart` skill, and its version stays at 0.15.30 ([pstack #776](https://github.com/cursor/plugins/pull/776) and [pstack #779](https://github.com/cursor/plugins/pull/779)). Before this, a run could draw a wrong chart or exit with the wrong code and not say so. The label map now stops on a variable or field that the `--fixed` or `--against` model lacks, where it used to give it the current model's start value. New `--config`, `--fixed-config`, and `--against-config` flags name each model's config. The agreed spec is never checked with the code model's config, and a missing config stops the run and lists the configs beside the spec. A rule the agreed config does not check reads "not checked" in the stories, where they used to say the agreed spec keeps it. When TLC finds a broken rule and then throws a Java exception, the run keeps the paths TLC printed, marks the rule broken, and warns that the charts can miss states. On a file system that cannot rename into the output folder (`ENOSYS`, `EXDEV`, or `EISDIR`, as on FUSE mounts), it copies the files into place. TLC checks each rule with one worker per CPU and checks a broken rule again with one worker, which gives the shortest paths. Each `PROPERTY` gets its own TLC run, `--expect-broken` accepts it, and a rule listed as both `INVARIANT` and `PROPERTY` is checked once. With `--against`, each story says whether a config beside the agreed spec expects the bug. With `--fixed` or `--against`, the run lists each condition of an action that no `\* file:line` comment ties to code. `SKILL.md` asks for those citations, says what a valid replay is, and asks the hand-off to say whether the spec already lists each bug. The test of each TLC run's temp folder accepts `Naturals.tla` anywhere under it, where TLC 1.8.0 puts it. #779 changes no behavior. It deletes script comments that repeat the code, and renames helpers so the name says what the comment did. `splitComments` becomes `splitCommentsKeepingOffsets`, `checkTlcOutput` becomes `tlcOutputWarning`, `quote` becomes `escapeMermaidQuotes`, and `luminance` becomes `wcagRelativeLuminance`, and one `PRIMES_OR_UNCHANGED` regex replaces two copies. `bun tools/sync.mjs` updated `SKILL.md`, `lib.mjs`, `statechart.mjs`, `tlc-to-chart.mjs`, and the test file cleanly, and each is byte-identical to upstream. No substitution, fork, or hook changed, and the 15 declared forks are untouched. At `7698375`, with TLC 1.7.4 on Linux and Node 20, 66 of the 67 skill tests pass and the PID-namespace test skips. With the TLC 1.8.0 prerelease, the `PROPERTY` test fails because 1.8.0 words a broken temporal property as "Temporal property X was violated.", which the scripts do not read yet, as #776 says. At `4ec7ffa` without TLC, 29 pass and 38 skip, and `from-spec` on the bundled `OutputFolder` model with TLC 1.7.4 exits 0 with all five rules holding. The README's skill count stays at 65. The copies #776 and #779 change under `harness/pstack/claude-code/` sit outside every synced component. At `4ec7ffa` each component's dry run reports no undeclared fork, no denylist hit, and no substitution that matches nothing. Neither hooks file changes. | Change | 2.0.0-rc.17 | 2.0.0-rc.18 | Source | | --- | --- | --- | --- | diff --git a/NOTICE-skills.md b/NOTICE-skills.md index 7ce56ca5..f83db199 100644 --- a/NOTICE-skills.md +++ b/NOTICE-skills.md @@ -4,9 +4,9 @@ This plugin contains MIT-licensed work from six sources. The copyright notices a | Included work | Upstream | Copyright | License | | --- | --- | --- | --- | -| The pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/pstack) | (c) 2026 Lauren Tan | [MIT](LICENSE) | -| `deslop`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, and `what-did-i-get-done` | [cursor/plugins/cursor-team-kit](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/cursor-team-kit) | (c) 2026 Cursor | [MIT](LICENSE-cursor-team-kit) | -| `thermos`, `thermo-nuclear-review`, `thermo-nuclear-code-quality-review`, and the `thermo-nuclear-review-subagent` and `thermo-nuclear-code-quality-review-subagent` definitions | [cursor/plugins/thermos](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/thermos) | (c) 2026 Cursor | [MIT](LICENSE-thermos) | +| The pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/4ec7ffa173eaa70d3d9467a627baf0954645a353/pstack) | (c) 2026 Lauren Tan | [MIT](LICENSE) | +| `deslop`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, and `what-did-i-get-done` | [cursor/plugins/cursor-team-kit](https://github.com/cursor/plugins/tree/4ec7ffa173eaa70d3d9467a627baf0954645a353/cursor-team-kit) | (c) 2026 Cursor | [MIT](LICENSE-cursor-team-kit) | +| `thermos`, `thermo-nuclear-review`, `thermo-nuclear-code-quality-review`, and the `thermo-nuclear-review-subagent` and `thermo-nuclear-code-quality-review-subagent` definitions | [cursor/plugins/thermos](https://github.com/cursor/plugins/tree/4ec7ffa173eaa70d3d9467a627baf0954645a353/thermos) | (c) 2026 Cursor | [MIT](LICENSE-thermos) | | The session-start hook scripts, `read-sheet.sh`, and `reflect/scripts/find-transcript.mjs`, which t3-pstack modified, and four `poteto-mode` rules, the worktree and head-guard rules in the Feature, Opening a PR, and Shipping playbooks, three `watch-pr` fixes, and the ignored-file and reflog-only-commit holds in `poteto-mode/scripts/worktree-audit.sh`, which t3-pstack reworded or adapted for T3, and the plugin icon | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude) | (c) 2026 Michael Denyer | [MIT](LICENSE) | | The plain-remove prune step in the worktree-cleanup playbook, which t3-pstack adapted | [sergchil/jutsu](https://github.com/sergchil/jutsu/commit/da9442422c72cc99442c1ce3500d2f2485234a31) | (c) 2026 Sergey Chilingaryan | [MIT](LICENSE) | | `poteto-mode/scripts/resolve-codex-transcript` and `resolve-codex-transcript.ts`, which t3-pstack modified | [ericlitman/open-pstack](https://github.com/ericlitman/open-pstack/tree/c5c8e237c324359a3d1929037da78fe66da3d1ed/plugins/pstack/skills/poteto-mode/scripts), [PR #151](https://github.com/ericlitman/open-pstack/pull/151) | (c) 2026 Eric A. Litman and Donncha O'Toole | [MIT](LICENSE) | diff --git a/NOTICE.md b/NOTICE.md index 180f9cca..01ac1184 100644 --- a/NOTICE.md +++ b/NOTICE.md @@ -6,9 +6,9 @@ t3-pstack is a port of [pstack](https://github.com/cursor/plugins/tree/main/psta | Component | Upstream | Copyright | License | License file | | --- | --- | --- | --- | --- | -| Every skill under `plugins/pstack/skills/` except those named in the next two rows, `plugins/pstack/agents/poteto-agent.md`, `plugins/pstack/agents/comment-sicko.md`, and the vendored scripts under `plugins/pstack/skills/poteto-mode/scripts/` | [cursor/plugins/pstack @ 7698375](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | -| `plugins/pstack/skills/{deslop,fix-ci,fix-merge-conflicts,get-pr-comments,make-pr-easy-to-review,what-did-i-get-done}/` | [cursor/plugins/cursor-team-kit @ 7698375](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/cursor-team-kit) | (c) 2026 Cursor | MIT | [LICENSE-cursor-team-kit](LICENSE-cursor-team-kit) | -| `plugins/pstack/skills/{thermos,thermo-nuclear-review,thermo-nuclear-code-quality-review}/`, `plugins/pstack/agents/thermo-nuclear-review-subagent.md`, `plugins/pstack/agents/thermo-nuclear-code-quality-review-subagent.md` | [cursor/plugins/thermos @ 7698375](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/thermos) | (c) 2026 Cursor | MIT | [LICENSE-thermos](LICENSE-thermos) | +| Every skill under `plugins/pstack/skills/` except those named in the next two rows, `plugins/pstack/agents/poteto-agent.md`, `plugins/pstack/agents/comment-sicko.md`, and the vendored scripts under `plugins/pstack/skills/poteto-mode/scripts/` | [cursor/plugins/pstack @ 4ec7ffa](https://github.com/cursor/plugins/tree/4ec7ffa173eaa70d3d9467a627baf0954645a353/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | +| `plugins/pstack/skills/{deslop,fix-ci,fix-merge-conflicts,get-pr-comments,make-pr-easy-to-review,what-did-i-get-done}/` | [cursor/plugins/cursor-team-kit @ 4ec7ffa](https://github.com/cursor/plugins/tree/4ec7ffa173eaa70d3d9467a627baf0954645a353/cursor-team-kit) | (c) 2026 Cursor | MIT | [LICENSE-cursor-team-kit](LICENSE-cursor-team-kit) | +| `plugins/pstack/skills/{thermos,thermo-nuclear-review,thermo-nuclear-code-quality-review}/`, `plugins/pstack/agents/thermo-nuclear-review-subagent.md`, `plugins/pstack/agents/thermo-nuclear-code-quality-review-subagent.md` | [cursor/plugins/thermos @ 4ec7ffa](https://github.com/cursor/plugins/tree/4ec7ffa173eaa70d3d9467a627baf0954645a353/thermos) | (c) 2026 Cursor | MIT | [LICENSE-thermos](LICENSE-thermos) | | `tools/sync.mjs`, `tools/generate.mjs`, `tools/validate-skills.mjs`, `tools/plugin.mjs`, `plugins/pstack/skills/reflect/scripts/find-transcript.mjs`, `plugins/pstack/hooks/session-start.sh`, `plugins/pstack/hooks/session-start.ps1`, `plugins/pstack/skills/setup-pstack/scripts/read-sheet.sh`, and the tests that cover them, each modified by t3-pstack | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude), as merged into t3-pstack through 1.0.14 | (c) 2026 Michael Denyer | MIT | [LICENSE](LICENSE) | | Four rules in `plugins/pstack/skills/poteto-mode/SKILL.md` (load a platform's skill before deploying, stop an abandoned agent and confirm it stopped, keep a review gate closed with no independent reviewer, the `todo.md` fallback), the per-delegate worktree rule in `playbooks/feature.md`, the stop-live-agents rule in `playbooks/opening-a-pr.md`, the `--match-head-commit` guard in `playbooks/shipping.md`, and the review-gate, stale-check, and no-checks fixes in `plugins/pstack/skills/poteto-mode/scripts/watch-pr/` with their tests in `verdicts.test.ts`, each reworded or adapted for T3 by t3-pstack | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude), pull requests [#95](https://github.com/michael-denyer/pstack-claude/pull/95), [#97](https://github.com/michael-denyer/pstack-claude/pull/97), and [#153](https://github.com/michael-denyer/pstack-claude/pull/153) for watch-pr | (c) 2026 Michael Denyer | MIT | [LICENSE](LICENSE) | | The ignored-file and reflog-only-commit holds in `plugins/pstack/skills/poteto-mode/scripts/worktree-audit.sh`, ported from JavaScript to bash, and their wording in `playbooks/worktree-cleanup.md`, with the test cases in `tests/worktree-audit.test.mjs`; the plugin icon with its C2PA manifest removed (`plugins/pstack/.claude-plugin/icon.png`, `plugins/pstack/assets/pstack-icon.png`) and `tests/image-metadata.test.mjs` | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude), pull requests [#277](https://github.com/michael-denyer/pstack-claude/pull/277) and [#271](https://github.com/michael-denyer/pstack-claude/pull/271) | (c) 2026 Michael Denyer | MIT | [LICENSE](LICENSE) | diff --git a/README.md b/README.md index bd6f8d5b..177837af 100644 --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ The plugin carries 65 skill directories, 24 of them `principle-*` leaves, and 4 ## Staying current -This repository syncs from Lauren's tree directly, synced against upstream `7698375`. `tools/upstream.json` pins each component, `tools/substitutions.json` holds the rewrite rules and a denylist of Cursor terms, and `tools/forks.json` declares every file the port keeps in its own form and why. `bun tools/sync.mjs <component> <sha>` derives each upstream file through the rules, merges it three ways with the port's copy, and fails on an undeclared fork, a denylist hit, or a rule that no longer matches upstream. [CONTRIBUTING.md](CONTRIBUTING.md#the-sync-boundary) has the details. +This repository syncs from Lauren's tree directly, synced against upstream `4ec7ffa`. `tools/upstream.json` pins each component, `tools/substitutions.json` holds the rewrite rules and a denylist of Cursor terms, and `tools/forks.json` declares every file the port keeps in its own form and why. `bun tools/sync.mjs <component> <sha>` derives each upstream file through the rules, merges it three ways with the port's copy, and fails on an undeclared fork, a denylist hit, or a rule that no longer matches upstream. [CONTRIBUTING.md](CONTRIBUTING.md#the-sync-boundary) has the details. ## Data handling diff --git a/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.md b/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.md index 7ce56ca5..f83db199 100644 --- a/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.md +++ b/plugins/pstack/skills/poteto-mode/references/licenses/NOTICE.md @@ -4,9 +4,9 @@ This plugin contains MIT-licensed work from six sources. The copyright notices a | Included work | Upstream | Copyright | License | | --- | --- | --- | --- | -| The pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/pstack) | (c) 2026 Lauren Tan | [MIT](LICENSE) | -| `deslop`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, and `what-did-i-get-done` | [cursor/plugins/cursor-team-kit](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/cursor-team-kit) | (c) 2026 Cursor | [MIT](LICENSE-cursor-team-kit) | -| `thermos`, `thermo-nuclear-review`, `thermo-nuclear-code-quality-review`, and the `thermo-nuclear-review-subagent` and `thermo-nuclear-code-quality-review-subagent` definitions | [cursor/plugins/thermos](https://github.com/cursor/plugins/tree/7698375f92a729f8bb89d113c633dce9ff9dc6db/thermos) | (c) 2026 Cursor | [MIT](LICENSE-thermos) | +| The pstack skills, principles, scripts, and the `poteto-agent` and `comment-sicko` definitions | [cursor/plugins/pstack](https://github.com/cursor/plugins/tree/4ec7ffa173eaa70d3d9467a627baf0954645a353/pstack) | (c) 2026 Lauren Tan | [MIT](LICENSE) | +| `deslop`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, and `what-did-i-get-done` | [cursor/plugins/cursor-team-kit](https://github.com/cursor/plugins/tree/4ec7ffa173eaa70d3d9467a627baf0954645a353/cursor-team-kit) | (c) 2026 Cursor | [MIT](LICENSE-cursor-team-kit) | +| `thermos`, `thermo-nuclear-review`, `thermo-nuclear-code-quality-review`, and the `thermo-nuclear-review-subagent` and `thermo-nuclear-code-quality-review-subagent` definitions | [cursor/plugins/thermos](https://github.com/cursor/plugins/tree/4ec7ffa173eaa70d3d9467a627baf0954645a353/thermos) | (c) 2026 Cursor | [MIT](LICENSE-thermos) | | The session-start hook scripts, `read-sheet.sh`, and `reflect/scripts/find-transcript.mjs`, which t3-pstack modified, and four `poteto-mode` rules, the worktree and head-guard rules in the Feature, Opening a PR, and Shipping playbooks, three `watch-pr` fixes, and the ignored-file and reflog-only-commit holds in `poteto-mode/scripts/worktree-audit.sh`, which t3-pstack reworded or adapted for T3, and the plugin icon | [michael-denyer/pstack-claude](https://github.com/michael-denyer/pstack-claude) | (c) 2026 Michael Denyer | [MIT](LICENSE) | | The plain-remove prune step in the worktree-cleanup playbook, which t3-pstack adapted | [sergchil/jutsu](https://github.com/sergchil/jutsu/commit/da9442422c72cc99442c1ce3500d2f2485234a31) | (c) 2026 Sergey Chilingaryan | [MIT](LICENSE) | | `poteto-mode/scripts/resolve-codex-transcript` and `resolve-codex-transcript.ts`, which t3-pstack modified | [ericlitman/open-pstack](https://github.com/ericlitman/open-pstack/tree/c5c8e237c324359a3d1929037da78fe66da3d1ed/plugins/pstack/skills/poteto-mode/scripts), [PR #151](https://github.com/ericlitman/open-pstack/pull/151) | (c) 2026 Eric A. Litman and Donncha O'Toole | [MIT](LICENSE) |