fix(pstack): check statechart rules with every CPU again

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

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<Check
   const dir = fs.mkdtempSync(path.join(os.tmpdir(), "statechart-"));
   try {
     const tlc = await findTlc(dir);
+    const workers = workerCount();
     const config = (name: string, sections: ConfigSection[], extra: string[]) => {
       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<Check
         if (properties.length) extra.push(`PROPERTY ${properties.join(" ")}`);
         const bounded = first !== undefined && !states.complete;
         if (bounded) extra.push("CONSTRAINT ChartBound");
-        const r = await runJava(name, "tlc2.TLC", [
-          "-tool",
-          ...PINNED_FLAGS,
-          ...(names(group, "deadlock").length ? [] : ["-deadlock"]),
-          ...config(name, spec.written, extra),
-          bounded ? "ChartBound" : spec.module,
-        ]);
+        const entry = bounded ? "ChartBound" : spec.module;
+        const tlcRun = (runName: string, n: number) =>
+          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<Check
     if (judged.states.distinct <= CHART_STATES) {
       const tag = `chart-${randomBytes(16).toString("hex")}`;
       fs.writeFileSync(path.join(dir, "ChartRun.tla"), chartRun(spec, tag));
-      const drawn = await runJava("ChartRun", "tlc2.TLC", [
-        "-tool",
-        ...PINNED_FLAGS,
-        "-deadlock",
-        ...config("ChartRun", spec.written, ["INVARIANT ChartMark", "CONSTRAINT ChartBudget"]),
-        "-dump",
-        "dot,actionlabels",
-        path.join(dir, "graph"),
+      const drawn = await runJava(
         "ChartRun",
-      ]);
+        "tlc2.TLC",
+        [
+          "-tool",
+          ...PINNED_FLAGS,
+          "-deadlock",
+          ...config("ChartRun", spec.written, ["INVARIANT ChartMark", "CONSTRAINT ChartBudget"]),
+          "-dump",
+          "dot,actionlabels",
+          path.join(dir, "graph"),
+          "ChartRun",
+        ],
+        TLC_HEAP,
+      );
       const file = path.join(dir, "graph.dot");
       if (!fs.existsSync(file)) throw failed(drawn);
       if (readVerdict(messagesOf(drawn.output)).distinct <= CHART_STATES) {

pstack/skills/statechart/scripts/test/workers.test.ts

@@ -0,0 +1,111 @@
+import assert from "node:assert/strict";
+import { spawnSync } from "node:child_process";
+import fs from "node:fs";
+import os from "node:os";
+import path from "node:path";
+import { test } from "node:test";
+import { fileURLToPath } from "node:url";
+
+const here = path.dirname(fileURLToPath(import.meta.url));
+const skip = !process.env.TLA2TOOLS && "set TLA2TOOLS to the path of tla2tools.jar to run TLC";
+const read = (file: string) => 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 <<a, b>>`,
+      "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:/);
+  },
+);