From decff1dd010c1c05ba381c927a15b518b19f3725 Mon Sep 17 00:00:00 2001 From: Prem Date: Thu, 5 Nov 2026 14:03:54 +0530 Subject: [PATCH] fix(pstack): check statechart rules with every CPU again #776 checked each rule with one worker per CPU and reran a broken rule with one worker for the shortest path. The compiler port (#977) pinned one worker and Java's default heap for every TLC run. Restore the all-CPU first run, keep one worker where the output depends on it, and let each TLC run's heap grow to half the memory Java sees. Co-Authored-By: Claude Opus 5.5 --- pstack/skills/statechart/SKILL.md | 2 +- pstack/skills/statechart/scripts/run.ts | 72 +++++++++--- .../statechart/scripts/test/workers.test.ts | 111 ++++++++++++++++++ 3 files changed, 167 insertions(+), 18 deletions(-) create mode 100644 pstack/skills/statechart/scripts/test/workers.test.ts diff --git a/pstack/skills/statechart/SKILL.md b/pstack/skills/statechart/SKILL.md index f5a64a8db..9fb2142ba 100644 --- a/pstack/skills/statechart/SKILL.md +++ b/pstack/skills/statechart/SKILL.md @@ -66,7 +66,7 @@ Aim for about 20 arrows or fewer, because a busier chart is hard to read. First - Because TLC goes past bugs, a model with no limit on its states can run without end. Keep the constants small, or add a CONSTRAINT. - With a VIEW or a SYMMETRY, TLC counts states that it treats as the same as one state, and the chart draws that one state. An arrow can lead to it rather than to the state that the step reaches, and the report says so. - TLC checks the rules in each state past a CONSTRAINT or an ACTION_CONSTRAINT, but it does not explore that state or check it for deadlock. When TLC's shortest path for a rule ends in such a state, the chart draws that state, and the report gives that path. The chart does not draw the other states past the bound. A deadlock in such a state does not show. TLC also checks the rules after each step that an ACTION_CONSTRAINT excludes, also when it reaches the next state another way. When TLC's shortest path for a rule ends with such a step, the chart draws that step. -- The command checks the rules with TLC on the config as written, with one worker. When a rule breaks, the command removes that rule and runs TLC again, until no rule breaks. After the first break, each run stops at 100,000 distinct states, so that a large model does not run without end. When a run reaches that bound or stops on an error, the report lists the rules that it did not check under "Rules not checked", and the chart does not mark them. A rule that is not checked can hold or break. To check it, remove the rules that break from the config, or make the model smaller. The bound adds a module that changes TLC's order of the variables, so for a property TLC can find a different counterexample than a run without the bound. +- The command checks the rules with TLC on the config as written. The first run uses one worker for each CPU, and `STATECHART_WORKERS` sets another count. Each TLC run's Java heap can grow to half the memory that Java sees. When that run reaches 100,000 states or fewer, or an INVARIANT or deadlock breaks, TLC runs it again with one worker, so that the bug path is the shortest and the same on every run. Above 100,000 states, a PROPERTY that breaks keeps the trace of the run with many workers, and that trace can differ between runs. When a rule breaks, the command removes that rule and runs TLC again, until no rule breaks. After the first break, each run stops at 100,000 distinct states, so that a large model does not run without end. When a run reaches that bound or stops on an error, the report lists the rules that it did not check under "Rules not checked", and the chart does not mark them. A rule that is not checked can hold or break. To check it, remove the rules that break from the config, or make the model smaller. The bound adds a module that changes TLC's order of the variables, so for a property TLC can find a different counterexample than a run without the bound. - `tlc.out` is what TLC printed on the config as written. When the chart does not show the bug path of a rule that breaks, `tlc-RULE.out` is what TLC printed for the run that found it. When TLC repeats its first warning, plain TLC prints it twice, but `tlc.out` shows it once, because TLC leaves the second copy out of the output that this command reads. That happens only when Java runs with `-XX:+UseParallelGC`, since otherwise TLC's first warning is its advice to pass that flag, which it prints once. ## Show the chart diff --git a/pstack/skills/statechart/scripts/run.ts b/pstack/skills/statechart/scripts/run.ts index 4efd368e5..741a54b14 100644 --- a/pstack/skills/statechart/scripts/run.ts +++ b/pstack/skills/statechart/scripts/run.ts @@ -10,7 +10,7 @@ import { plainText } from "./backends/plain-text.ts"; import { readConfig } from "./frontends/config.ts"; import { parseDot } from "./frontends/dot.ts"; import { readCounterexample, readMarks } from "./frontends/marks.ts"; -import { readMessages } from "./frontends/messages.ts"; +import { readMessages, textOf } from "./frontends/messages.ts"; import { initialOnlyProperties, readChecks, readSany, readSpec } from "./frontends/spec.ts"; import { readTrace } from "./frontends/trace.ts"; import { type Break, readVerdict } from "./frontends/verdict.ts"; @@ -68,6 +68,16 @@ const TLC_TOOL = "http:tla2tools[url=https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar,checksum=sha256:936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88]@1.7.4"; const JAVA_TOOL = "java@temurin-25"; export const PINNED_FLAGS = ["-workers", "1", "-fp", "0", "-lncheck", "final"]; +const TLC_HEAP = ["-XX:MaxRAMPercentage=50"]; + +const workerCount = () => { + const raw = process.env.STATECHART_WORKERS; + if (raw && /^[1-9]\d*$/.test(raw)) return Number(raw); + return os.availableParallelism(); +}; + +const tlcFlags = (n: number) => + n === 1 ? PINNED_FLAGS : ["-workers", String(n), "-fp", "0", "-lncheck", "final"]; type ChildResult = { status: number | null; @@ -215,6 +225,15 @@ async function findTlc(cwd: string) { const exitClass = (status: number | null) => status === 0 ? 0 : status === 11 || status === 12 || status === 13 ? 1 : 2; +const workersReported = (r: FileResult) => { + for (const m of messagesOf(r.output)) { + if (typeof m === "string") continue; + const found = /with (\d+) workers?/.exec(textOf(m)); + if (found) return Number(found[1]); + } + return undefined; +}; + const tail = (r: FileResult) => { if (r.error) return r.error.message; const kept: string[] = []; @@ -274,6 +293,7 @@ export async function check(specFile: string, configFile: string): Promise { fs.writeFileSync(path.join(dir, `${name}.cfg`), configText(sections, extra)); return [`-metadir`, path.join(dir, `meta-${name}`), "-config", path.join(dir, `${name}.cfg`)]; @@ -336,13 +356,26 @@ export async function check(specFile: string, configFile: string): Promise + runJava( + runName, + "tlc2.TLC", + [ + "-tool", + ...tlcFlags(n), + ...(names(group, "deadlock").length ? [] : ["-deadlock"]), + ...config(runName, spec.written, extra), + entry, + ], + TLC_HEAP, + ); + let r = await tlcRun(name, bounded ? 1 : workers); + if (!bounded && workers > 1 && exitClass(r.status) !== 2 && workersReported(r) !== 1) { + const seen = readVerdict(messagesOf(r.output)); + if (seen.distinct <= RERUN_STATES || (seen.broke && seen.broke.kind !== "temporal")) + r = await tlcRun(`${name}-w1`, 1); + } first ??= r; const { broke, distinct, initial } = readVerdict(messagesOf(r.output)); states.distinct = Math.max(states.distinct, distinct); @@ -412,16 +445,21 @@ export async function check(specFile: string, configFile: string): Promise fs.readFileSync(file, "utf8"); + +const distinct = (text: string) => { + let n = 0; + for (const m of text.matchAll(/(\d[\d,]*) distinct states found/g)) + n = Math.max(n, Number(m[1].replaceAll(",", ""))); + return n; +}; + +const holds = (report: string) => report.match(/^## Rules that hold\n(.*)$/m)?.[1]; +const reached = (report: string) => report.match(/^TLC reached ([\d,]+) states,/m)?.[1]; +const shortest = (report: string) => report.match(/^## \S+ breaks\n[\s\S]*?(?=\n## |$)/m)?.[0]; + +function writeModel(name: string, limit: number, rule: string, cfg: string) { + const dir = fs.mkdtempSync(path.join(os.tmpdir(), "statechart-workers-")); + fs.writeFileSync( + path.join(dir, `${name}.tla`), + [ + `---- MODULE ${name} ----`, + "EXTENDS Naturals", + "VARIABLES a, b", + "Init == a = 0 /\\ b = 0", + `IncA == a < ${limit} /\\ a' = a + 1 /\\ UNCHANGED b`, + `IncB == b < ${limit} /\\ b' = b + 1 /\\ UNCHANGED a`, + `Rest == a = ${limit} /\\ b = ${limit} /\\ UNCHANGED <>`, + "Next == IncA \\/ IncB \\/ Rest", + rule, + "====", + "", + ].join("\n"), + ); + fs.writeFileSync(path.join(dir, `${name}.cfg`), cfg); + return dir; +} + +function check(dir: string, name: string, workers: string) { + const out = path.join(dir, `out-${workers}`); + const r = spawnSync( + process.execPath, + [ + path.join(here, "../statechart.ts"), + path.join(dir, `${name}.tla`), + "--config", + path.join(dir, `${name}.cfg`), + "--out", + out, + ], + { + encoding: "utf8", + env: { ...process.env, STATECHART_WORKERS: workers }, + }, + ); + assert.equal(r.stderr, ""); + return { + status: r.status, + report: read(path.join(out, "report.md")), + tlc: read(path.join(out, "tlc.out")), + }; +} + +test( + "a model above 100,000 states that holds matches one worker and records two", + { skip, timeout: 1_200_000 }, + () => { + const dir = writeModel( + "WideHold", + 330, + "Room == a \\in 0..330 /\\ b \\in 0..330", + "INIT Init\nNEXT Next\nINVARIANT Room\n", + ); + const one = check(dir, "WideHold", "1"); + const two = check(dir, "WideHold", "2"); + assert.equal(one.status, 0); + assert.equal(two.status, 0); + assert.equal(holds(two.report), holds(one.report)); + assert.equal(reached(two.report), reached(one.report)); + assert.ok(distinct(one.tlc) > 100_000); + assert.equal(distinct(two.tlc), distinct(one.tlc)); + assert.match(two.tlc, /with 2 workers/); + }, +); + +test( + "a model above 100,000 states keeps the one-worker shortest path when an invariant breaks", + { skip, timeout: 1_200_000 }, + () => { + const dir = writeModel( + "WideBreak", + 460, + "Below == a < 460", + "INIT Init\nNEXT Next\nINVARIANT Below\nCHECK_DEADLOCK FALSE\n", + ); + const one = check(dir, "WideBreak", "1"); + const two = check(dir, "WideBreak", "2"); + assert.equal(one.status, 1); + assert.equal(two.status, 1); + assert.ok(distinct(one.tlc) > 100_000); + assert.equal(shortest(two.report), shortest(one.report)); + assert.match(shortest(one.report) ?? "", /The shortest path has 460 steps:/); + }, +);