#!/usr/bin/env nodeimport { spawnSync } from "node:child_process";import fs from "node:fs";import os from "node:os";import path from "node:path";import process from "node:process";import { fileURLToPath, pathToFileURL } from "node:url";import { BROKEN_PROPERTY, findTlc, joinAnd, parseDot, PRIMES_OR_UNCHANGED, tlaVariables, tlcOutputWarning, uncitedConditions,} from "./lib.mjs"; const here = path.dirname(fileURLToPath(import.meta.url)); const USAGE = { "from-spec": "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]",};const usage = (lines) => `Usage: ${lines.join("\n ")}`; 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 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 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, 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 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 writes none of them. Then it checks the spec as from-spec does, and compares the chart that the spec draws with CHART.mmd. --module NAME The TLA+ module name. Default: the chart's file name in CamelCase, such as NotesApp for notes-app.mmd. The chart is a Mermaid stateDiagram-v2. Each transition label is one action. For parallel regions, split one top-level composite with --, and put each part in a named composite, such as state Connection { ... }. Each region is one variable. A step moves every region whose current state has a transition with the step's label, and the other regions stay where they are. Each rule is one comment line: %% never NAME: A & B -- the rule in one sentence Each name after the colon is a state caption or a composite, and each comes from a different region. A composite stands for every state in it. The command refuses final, choice, fork, and history states, and regions below the top level.`; const COMMON = `Both commands --expect-broken 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. 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. Output The command prints whether each rule holds, the chart's counts, and one story per bug. from-chart also prints the comparison. The command writes these files in the output folder: chart.mmd The overview. bug-N.mmd Only the steps of bug N, numbered. Bugs are numbered by fewest reader steps, then fewest model steps, then rule name, then cause. Bugs that only the --fixed or --against model has come last. bug-N-developer.mmd, bug-N-layered.mmd The path of bug N through the developer's states, when the mapping exports 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. 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. compare-charts.mjs tlc/regions-all.mmd tlc/regions-proof.mmd repeats the proof. *.png Each chart as a PNG, with --png. A run without --png deletes them. Reading a chart from-spec draws the overview as two parallel regions when every state reads "context: progress": the contexts on one side, the progress on the other, both at the same time. It does so only when that has fewer states, and when the regions combine back into exactly every state and step of TLC's graph. Otherwise it puts the states of one context in a box named context, and prints why. Regions draw only the arrows of the shortest way to each state, of each bug path, and of the nearest step with each label. The script checks that these arrows make no step that TLC's graph does not have. An arrow from a box's border leaves from every state in the box. In regions, a step leaves every region that has it. "[when A]" or "[unless A]" says which states of the other region the step needs. A loop says the region may also stay. Other words in [ ] come from the mapping's guard(), and "after N s" from its timer(). TLC does not check them, and has no clock, so a reviewer checks them against the code. Gray states work. Red states break a rule. With --fixed, red states stay wrong with the fix, and green states are fixed by it or exist only with it. With --against, red states break a rule in either model, and green states exist only in the spec. When the mapping exports group(), the fill is the state's group, which the legend names, and the status is a thick red or green border on top. tlc-to-chart.mjs --help tells more. A state is bad when it breaks a rule, or when every path from the start to it passes a state that breaks one. TLC stops each path at the first state that breaks the rule, so a rule that stays broken colors only the states where it first breaks and the states after them that no path without a bug reaches. A thick blue border and numbered labels mark the bug. Mermaid state diagrams cannot color an edge. A label "with the fix, STEP" or "in the spec, STEP" is a step that only the other model takes. On a bug's path it leaves the state before the first step that the other model shows the reader differently, and ends where that model goes instead. "with the fix, STEP cannot happen" or "in the spec, STEP cannot happen" loops on the state where that model stops the step. Outside regions, two states have at most one arrow between them. Its lines are the numbered steps, then SPEC.tla's steps, then the other model's steps, with a blank line between each group. An edge lists every step that takes it, most common first. Words that the steps share at the start are written once, as in "you tap Pay or Back". Regenerate With --expect-broken, one script rebuilds every chart and stops on any change: set -e node statechart.mjs from-spec Code.tla --against Agreed.tla --expect-broken NoLostUpload --png 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 back unchanged. 1 Another rule is broken, an expected rule holds, or the chart that the spec draws is not CHART.mmd. The output says which. 2 The command cannot finish: a bad argument, a missing file, a chart or TLC output that it cannot read, no TLC, a helper script that cannot start, an output folder with files that the command did not write, an input file that changed during the run, a new mapping to fill in, or a chart that --png cannot render. When a chart does not render, the command keeps the 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. 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"])} Draws a Mermaid statechart of what an app's user sees, from TLC's state graph of a TLA+ spec. Thehelp calls that user the reader. ${FROM_SPEC} ${FROM_CHART} ${COMMON}`, "from-spec": `${usage([USAGE["from-spec"]])}\n\n${FROM_SPEC}\n\n${COMMON}`, "from-chart": `${usage([USAGE["from-chart"]])}\n\n${FROM_CHART}\n\n${COMMON}`,}; const more = (cmd) => `Run node statechart.mjs ${cmd ? `${cmd} ` : ""}--help for the flags, the output, and the exit codes.`; class CannotFinish extends Error {}class TlcStopped extends CannotFinish {}class NotPublished extends CannotFinish {} const COMMANDS = { "from-spec": { 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 },}; function parseArgs([command, ...rest]) { if (command === "-h" || command === "--help") return { help: HELP[""] }; if (!Object.hasOwn(COMMANDS, command)) throw new CannotFinish(`${usage(Object.values(USAGE))}\n${more()}`); const flags = { "expect-broken": new Set() }; let input; for (let i = 0; i < rest.length; i++) { const a = rest[i]; if (a === "-h" || a === "--help") return { help: HELP[command] }; if (a === "--png") flags.png = true; else if (COMMANDS[command].flags.includes(a)) { if (i + 1 === rest.length) throw new CannotFinish(`${a} needs a value. ${more(command)}`); const name = a.slice(2); if (flags[name] instanceof Set) for (const v of rest[++i].split(",")) flags[name].add(v); else flags[name] = rest[++i]; } else if (!a.startsWith("-") && input === undefined) input = a; else throw new CannotFinish(`unknown argument ${a}. ${more(command)}`); } if (input === undefined) throw new CannotFinish(`${usage([USAGE[command]])}\n${more(command)}`); return { command, input, flags };} 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() { try { return findTlc(); } catch (e) { throw new CannotFinish(e.message); }} function script(name, scriptArgs, about, { okExits = [0] } = {}) { const r = spawnSync(process.execPath, [path.join(here, name), ...scriptArgs], { encoding: "utf8", }); if (r.error) throw new CannotFinish(`cannot run ${name}: ${r.error.message}`); if (okExits.includes(r.status)) return r; const thrown = r.stderr.match(/^Error: (.*)$/m)?.[1]; throw new CannotFinish(thrown ? `${rel(about)}: ${thrown}` : r.stderr.trim());} const KEYWORD = /^(SPECIFICATION|INIT|NEXT|CONSTANTS?|INVARIANTS?|PROPERTY|PROPERTIES|SYMMETRY|VIEW|CONSTRAINTS?|ACTION_CONSTRAINTS?|CHECK_DEADLOCK|POSTCONDITION|ALIAS)$/; function splitRules(cfg) { const words = cfg .replace(/\(\*[^]*?\*\)/g, " ") .replace(/\\\*.*/g, " ") .split(/\s+/) .filter(Boolean); const kept = []; const rules = []; const properties = []; let section = ""; for (const w of words) { if (KEYWORD.test(w)) section = 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); } // 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, 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, // so runs that share that folder can read a module while another run rewrites it. const javaTmp = path.join(metadir, "tmp"); fs.mkdirSync(javaTmp); // -deadlock: a UI at rest has nothing left to do, which TLC would report as a deadlock. const r = spawnSync( tools.java, [ "-XX:+UseParallelGC", `-Djava.io.tmpdir=${javaTmp}`, "-cp", tools.jar, "tlc2.TLC", "-workers", workers, "-metadir", metadir, "-deadlock", "-continue", ...(dump ? ["-dump", "dot,actionlabels", path.resolve(dump)] : []), "-config", path.resolve(`${base}.cfg`), path.basename(spec), ], { cwd: path.dirname(path.resolve(spec)), encoding: "utf8", maxBuffer: 1 << 30 }, ); fs.rmSync(metadir, { recursive: true, force: true }); if (r.error) throw new CannotFinish(`cannot run TLC: ${r.error.message}`); fs.writeFileSync(`${base}.out`, r.stdout); try { return { stdout: r.stdout, warning: tlcOutputWarning(r.stdout, `${base}.out`) }; } catch (e) { throw new TlcStopped(e.message); }} 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 = /^NEXT\s+(\w+)/m.exec(cfg)?.[1] ?? /\[\]\s*\[\s*(\w+)\s*\]_/.exec(specBody?.[1] ?? text)?.[1]; const graph = parseDot(fs.readFileSync(dot, "utf8")); const unnamed = [...graph.edges, ...graph.loops].filter((e) => e.action === next).length; if (unnamed > 0) console.error( `${rel(spec)}: ${unnamed} ${unnamed === 1 ? "step has" : "steps have"} the name ${next}, the whole next-state action, because TLC names a step after the innermost named action that takes it. If the reader must tell these steps apart, give each part of ${next} its own name, as in Pay == ... and ${next} == Pay \\/ Charge.`, );} function readModel(spec, cfgFile, flag) { if (!fs.existsSync(spec)) throw new CannotFinish(`${rel(spec)} does not exist`); 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. 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, 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 ${names.join(", ") || "none"}.`, ); return model;} 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`); // 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)} with ${rel(cfgFile)}:`); if (rules.length === 0) 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))); const traces = rules.map((rule) => { const file = path.join(tlcDir, `${name}-${rule}`); const cfg = `${cfgWithoutRules}INVARIANT ${rule}\nCONSTRAINT ${rule}\n`; 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( `${said(property, broken)}${broken ? ` The chart draws only INVARIANT rules, so read TLC's counterexample in ${shown(`${file}.out`)}.` : ""}`, ); return { file: `${file}.out`, rule: property, 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 ?? []), ...(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), ); const holds = [...expected].filter((r) => !brokenIn(now).includes(r)); if (unexpected.length) console.log(`\nBroken but not expected: ${unexpected.join(", ")}.`); if (holds.length) console.log(`\nExpected to break but holds: ${holds.join(", ")}.`); if (!unexpected.length && !holds.length) console.log(`\nBroken as expected: ${[...expected].join(", ")}.`); return !unexpected.length && !holds.length;} const SCAFFOLD = (name, spec) => { const text = withoutComments(spec); const vars = tlaVariables(text); // 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 && PRIMES_OR_UNCHANGED.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.// Variables: ${vars.join(", ")}. // The actions the reader takes. facts.settled is true when only these are enabled, and the overview// keeps the shortest path to each settled state, plus every bug path.export const readerActions = []; // The label for one model state. facts.enabled is the set of actions the state enables,// including steps that change no variable. Write it as "context: progress", such as// "Offline: upload queued": the chart puts the states of one context in one box.// Do not claim a result that a pending step can still change, such as "upload failed" while a// retry is still queued.export function state(v, facts) { return JSON.stringify(v);} // The names of the two parallel regions, when the overview draws them: contexts, then progress.Lines 1–500 of 961. Load more
#!/usr/bin/env node import { spawnSync } from "node:child_process"; import fs from "node:fs"; import os from "node:os"; import path from "node:path"; import process from "node:process"; import { fileURLToPath, pathToFileURL } from "node:url"; import { BROKEN_PROPERTY, findTlc, joinAnd, parseDot, PRIMES_OR_UNCHANGED, tlaVariables, tlcOutputWarning, uncitedConditions, } from "./lib.mjs"; const here = path.dirname(fileURLToPath(import.meta.url)); const USAGE = { "from-spec": "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]", }; const usage = (lines) => `Usage: ${lines.join("\n ")}`; 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 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 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, 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 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 writes none of them. Then it checks the spec as from-spec does, and compares the chart that the spec draws with CHART.mmd. --module NAME The TLA+ module name. Default: the chart's file name in CamelCase, such as NotesApp for notes-app.mmd. The chart is a Mermaid stateDiagram-v2. Each transition label is one action. For parallel regions, split one top-level composite with --, and put each part in a named composite, such as state Connection { ... }. Each region is one variable. A step moves every region whose current state has a transition with the step's label, and the other regions stay where they are. Each rule is one comment line: %% never NAME: A & B -- the rule in one sentence Each name after the colon is a state caption or a composite, and each comes from a different region. A composite stands for every state in it. The command refuses final, choice, fork, and history states, and regions below the top level.`; const COMMON = `Both commands --expect-broken 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. 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. Output The command prints whether each rule holds, the chart's counts, and one story per bug. from-chart also prints the comparison. The command writes these files in the output folder: chart.mmd The overview. bug-N.mmd Only the steps of bug N, numbered. Bugs are numbered by fewest reader steps, then fewest model steps, then rule name, then cause. Bugs that only the --fixed or --against model has come last. bug-N-developer.mmd, bug-N-layered.mmd The path of bug N through the developer's states, when the mapping exports 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. 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. compare-charts.mjs tlc/regions-all.mmd tlc/regions-proof.mmd repeats the proof. *.png Each chart as a PNG, with --png. A run without --png deletes them. Reading a chart from-spec draws the overview as two parallel regions when every state reads "context: progress": the contexts on one side, the progress on the other, both at the same time. It does so only when that has fewer states, and when the regions combine back into exactly every state and step of TLC's graph. Otherwise it puts the states of one context in a box named context, and prints why. Regions draw only the arrows of the shortest way to each state, of each bug path, and of the nearest step with each label. The script checks that these arrows make no step that TLC's graph does not have. An arrow from a box's border leaves from every state in the box. In regions, a step leaves every region that has it. "[when A]" or "[unless A]" says which states of the other region the step needs. A loop says the region may also stay. Other words in [ ] come from the mapping's guard(), and "after N s" from its timer(). TLC does not check them, and has no clock, so a reviewer checks them against the code. Gray states work. Red states break a rule. With --fixed, red states stay wrong with the fix, and green states are fixed by it or exist only with it. With --against, red states break a rule in either model, and green states exist only in the spec. When the mapping exports group(), the fill is the state's group, which the legend names, and the status is a thick red or green border on top. tlc-to-chart.mjs --help tells more. A state is bad when it breaks a rule, or when every path from the start to it passes a state that breaks one. TLC stops each path at the first state that breaks the rule, so a rule that stays broken colors only the states where it first breaks and the states after them that no path without a bug reaches. A thick blue border and numbered labels mark the bug. Mermaid state diagrams cannot color an edge. A label "with the fix, STEP" or "in the spec, STEP" is a step that only the other model takes. On a bug's path it leaves the state before the first step that the other model shows the reader differently, and ends where that model goes instead. "with the fix, STEP cannot happen" or "in the spec, STEP cannot happen" loops on the state where that model stops the step. Outside regions, two states have at most one arrow between them. Its lines are the numbered steps, then SPEC.tla's steps, then the other model's steps, with a blank line between each group. An edge lists every step that takes it, most common first. Words that the steps share at the start are written once, as in "you tap Pay or Back". Regenerate With --expect-broken, one script rebuilds every chart and stops on any change: set -e node statechart.mjs from-spec Code.tla --against Agreed.tla --expect-broken NoLostUpload --png 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 back unchanged. 1 Another rule is broken, an expected rule holds, or the chart that the spec draws is not CHART.mmd. The output says which. 2 The command cannot finish: a bad argument, a missing file, a chart or TLC output that it cannot read, no TLC, a helper script that cannot start, an output folder with files that the command did not write, an input file that changed during the run, a new mapping to fill in, or a chart that --png cannot render. When a chart does not render, the command keeps the 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. 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"])} Draws a Mermaid statechart of what an app's user sees, from TLC's state graph of a TLA+ spec. The help calls that user the reader. ${FROM_SPEC} ${FROM_CHART} ${COMMON}`, "from-spec": `${usage([USAGE["from-spec"]])}\n\n${FROM_SPEC}\n\n${COMMON}`, "from-chart": `${usage([USAGE["from-chart"]])}\n\n${FROM_CHART}\n\n${COMMON}`, }; const more = (cmd) => `Run node statechart.mjs ${cmd ? `${cmd} ` : ""}--help for the flags, the output, and the exit codes.`; class CannotFinish extends Error {} class TlcStopped extends CannotFinish {} class NotPublished extends CannotFinish {} const COMMANDS = { "from-spec": { 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 }, }; function parseArgs([command, ...rest]) { if (command === "-h" || command === "--help") return { help: HELP[""] }; if (!Object.hasOwn(COMMANDS, command)) throw new CannotFinish(`${usage(Object.values(USAGE))}\n${more()}`); const flags = { "expect-broken": new Set() }; let input; for (let i = 0; i < rest.length; i++) { const a = rest[i]; if (a === "-h" || a === "--help") return { help: HELP[command] }; if (a === "--png") flags.png = true; else if (COMMANDS[command].flags.includes(a)) { if (i + 1 === rest.length) throw new CannotFinish(`${a} needs a value. ${more(command)}`); const name = a.slice(2); if (flags[name] instanceof Set) for (const v of rest[++i].split(",")) flags[name].add(v); else flags[name] = rest[++i]; } else if (!a.startsWith("-") && input === undefined) input = a; else throw new CannotFinish(`unknown argument ${a}. ${more(command)}`); } if (input === undefined) throw new CannotFinish(`${usage([USAGE[command]])}\n${more(command)}`); return { command, input, flags }; } 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() { try { return findTlc(); } catch (e) { throw new CannotFinish(e.message); } } function script(name, scriptArgs, about, { okExits = [0] } = {}) { const r = spawnSync(process.execPath, [path.join(here, name), ...scriptArgs], { encoding: "utf8", }); if (r.error) throw new CannotFinish(`cannot run ${name}: ${r.error.message}`); if (okExits.includes(r.status)) return r; const thrown = r.stderr.match(/^Error: (.*)$/m)?.[1]; throw new CannotFinish(thrown ? `${rel(about)}: ${thrown}` : r.stderr.trim()); } const KEYWORD = /^(SPECIFICATION|INIT|NEXT|CONSTANTS?|INVARIANTS?|PROPERTY|PROPERTIES|SYMMETRY|VIEW|CONSTRAINTS?|ACTION_CONSTRAINTS?|CHECK_DEADLOCK|POSTCONDITION|ALIAS)$/; function splitRules(cfg) { const words = cfg .replace(/\(\*[^]*?\*\)/g, " ") .replace(/\\\*.*/g, " ") .split(/\s+/) .filter(Boolean); const kept = []; const rules = []; const properties = []; let section = ""; for (const w of words) { if (KEYWORD.test(w)) section = 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); } // 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, 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, // so runs that share that folder can read a module while another run rewrites it. const javaTmp = path.join(metadir, "tmp"); fs.mkdirSync(javaTmp); // -deadlock: a UI at rest has nothing left to do, which TLC would report as a deadlock. const r = spawnSync( tools.java, [ "-XX:+UseParallelGC", `-Djava.io.tmpdir=${javaTmp}`, "-cp", tools.jar, "tlc2.TLC", "-workers", workers, "-metadir", metadir, "-deadlock", "-continue", ...(dump ? ["-dump", "dot,actionlabels", path.resolve(dump)] : []), "-config", path.resolve(`${base}.cfg`), path.basename(spec), ], { cwd: path.dirname(path.resolve(spec)), encoding: "utf8", maxBuffer: 1 << 30 }, ); fs.rmSync(metadir, { recursive: true, force: true }); if (r.error) throw new CannotFinish(`cannot run TLC: ${r.error.message}`); fs.writeFileSync(`${base}.out`, r.stdout); try { return { stdout: r.stdout, warning: tlcOutputWarning(r.stdout, `${base}.out`) }; } catch (e) { throw new TlcStopped(e.message); } } 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 = /^NEXT\s+(\w+)/m.exec(cfg)?.[1] ?? /\[\]\s*\[\s*(\w+)\s*\]_/.exec(specBody?.[1] ?? text)?.[1]; const graph = parseDot(fs.readFileSync(dot, "utf8")); const unnamed = [...graph.edges, ...graph.loops].filter((e) => e.action === next).length; if (unnamed > 0) console.error( `${rel(spec)}: ${unnamed} ${unnamed === 1 ? "step has" : "steps have"} the name ${next}, the whole next-state action, because TLC names a step after the innermost named action that takes it. If the reader must tell these steps apart, give each part of ${next} its own name, as in Pay == ... and ${next} == Pay \\/ Charge.`, ); } function readModel(spec, cfgFile, flag) { if (!fs.existsSync(spec)) throw new CannotFinish(`${rel(spec)} does not exist`); 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. 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, 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 ${names.join(", ") || "none"}.`, ); return model; } 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`); // 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)} with ${rel(cfgFile)}:`); if (rules.length === 0) 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))); const traces = rules.map((rule) => { const file = path.join(tlcDir, `${name}-${rule}`); const cfg = `${cfgWithoutRules}INVARIANT ${rule}\nCONSTRAINT ${rule}\n`; 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( `${said(property, broken)}${broken ? ` The chart draws only INVARIANT rules, so read TLC's counterexample in ${shown(`${file}.out`)}.` : ""}`, ); return { file: `${file}.out`, rule: property, 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 ?? []), ...(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), ); const holds = [...expected].filter((r) => !brokenIn(now).includes(r)); if (unexpected.length) console.log(`\nBroken but not expected: ${unexpected.join(", ")}.`); if (holds.length) console.log(`\nExpected to break but holds: ${holds.join(", ")}.`); if (!unexpected.length && !holds.length) console.log(`\nBroken as expected: ${[...expected].join(", ")}.`); return !unexpected.length && !holds.length; } const SCAFFOLD = (name, spec) => { const text = withoutComments(spec); const vars = tlaVariables(text); // 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 && PRIMES_OR_UNCHANGED.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. // Variables: ${vars.join(", ")}. // The actions the reader takes. facts.settled is true when only these are enabled, and the overview // keeps the shortest path to each settled state, plus every bug path. export const readerActions = []; // The label for one model state. facts.enabled is the set of actions the state enables, // including steps that change no variable. Write it as "context: progress", such as // "Offline: upload queued": the chart puts the states of one context in one box. // Do not claim a result that a pending step can still change, such as "upload failed" while a // retry is still queued. export function state(v, facts) { return JSON.stringify(v); } // The names of the two parallel regions, when the overview draws them: contexts, then progress.