import fs from "node:fs";import process from "node:process"; export function findTlc() {  const { TLA2TOOLS, JAVA } = process.env;  if (!TLA2TOOLS)    throw new Error(      "Cannot find TLC. Download tla2tools.jar from a TLA+ release:\n  https://github.com/tlaplus/tlaplus/releases\nThen set TLA2TOOLS to the path of tla2tools.jar, and JAVA to a java binary (Java 11 or later).",    );  if (!fs.existsSync(TLA2TOOLS)) throw new Error(`TLA2TOOLS is ${TLA2TOOLS}, which does not exist.`);  return { jar: TLA2TOOLS, java: JAVA || "java" };} export function parseValue(text) {  const src = text.trim();  let i = 0;  const ws = () => {    while (i < src.length && /\s/.test(src[i])) i++;  };  const peek = (s) => src.startsWith(s, i);  const eat = (s) => {    ws();    if (!peek(s)) throw new Error(`expected ${s} at ${i} in ${src}`);    i += s.length;  };  const list = (close, item) => {    const out = [];    ws();    if (peek(close)) {      i += close.length;      return out;    }    for (;;) {      out.push(item());      ws();      if (peek(",")) {        i++;        continue;      }      eat(close);      return out;    }  };  const value = () => {    ws();    if (peek("<<")) {      i += 2;      return list(">>", value);    }    if (peek("{")) {      i++;      return list("}", value);    }    if (peek("[")) {      i++;      const pairs = list("]", () => {        ws();        const m = /^[A-Za-z_][A-Za-z0-9_]*/.exec(src.slice(i));        if (!m) throw new Error(`bad record field at ${i}`);        i += m[0].length;        eat("|->");        return [m[0], value()];      });      return Object.fromEntries(pairs);    }    if (peek("(")) {      i++;      const fn = {};      for (;;) {        const k = value();        eat(":>");        fn[typeof k === "string" ? k : JSON.stringify(k)] = value();        ws();        if (peek("@@")) {          i += 2;          continue;        }        eat(")");        return fn;      }    }    if (peek('"')) {      i++;      let s = "";      while (i < src.length && src[i] !== '"') {        if (src[i] === "\\") i++;        s += src[i++];      }      i++;      return s;    }    const m = /^-?\d+|^[A-Za-z_][A-Za-z0-9_]*/.exec(src.slice(i));    if (!m) throw new Error(`bad value at ${i} in ${src}`);    i += m[0].length;    if (m[0] === "TRUE") return true;    if (m[0] === "FALSE") return false;    return /^-?\d+$/.test(m[0]) ? Number(m[0]) : m[0];  };  try {    const v = value();    ws();    return i === src.length ? v : src;  } catch {    return src;  }} // One state as TLC prints it: "/\ x = 1" lines, or "x = 1" for one variable.function parseState(text) {  const lines = text.split("\n").filter((l) => l.trim() !== "");  const conjuncts = [];  for (const line of lines) {    if (/^\s*\/\\ /.test(line) || conjuncts.length === 0)      conjuncts.push(line.replace(/^\s*\/\\ /, ""));    else conjuncts[conjuncts.length - 1] += ` ${line.trim()}`;  }  const vars = {};  for (const c of conjuncts) {    const eq = c.indexOf(" = ");    if (eq < 0) continue;    vars[c.slice(0, eq).trim()] = parseValue(c.slice(eq + 3));  }  return vars;} export const isRecord = (v) => v !== null && typeof v === "object" && !Array.isArray(v);const canon = (v) =>  Array.isArray(v)    ? v.map(canon)    : isRecord(v)      ? Object.fromEntries(          Object.keys(v)            .sort()            .map((k) => [k, canon(v[k])]),        )      : v;export const stateKey = (vars) => JSON.stringify(canon(vars)); export function ruleSentences(tla) {  const out = new Map();  const lines = tla.split("\n");  lines.forEach((line, i) => {    const name = /^([A-Za-z_]\w*)\s*==/.exec(line)?.[1];    if (!name) return;    const said = [];    for (let j = i - 1; j >= 0 && /^\s*\\\*/.test(lines[j]); j--)      said.unshift(lines[j].replace(/^\s*\\\*\s?/, "").trim());    const sentence = said.filter(Boolean).join(" ");    if (sentence) out.set(name, sentence);  });  return out;} export const tlaVariables = (code) =>  [...code.matchAll(/\bVARIABLES?\s+(\w+(?:\s*,\s*\w+)*)/g)].flatMap((m) => m[1].split(/\s*,\s*/)); function splitCommentsKeepingOffsets(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 = /(?<![\\.\w])[A-Za-z_]\w*(?!\w)(?!\s*\|->)/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/;export const PRIMES_OR_UNCHANGED = /[\w)\]>}]'|\bUNCHANGED\b/; 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]);} export function uncitedConditions(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)];  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(/(?<![\\.\w])([A-Za-z_]\w*)'/g)]        .map((m) => m[1])        .filter((id) => variables.has(id)),      acts: PRIMES_OR_UNCHANGED.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, { above: 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++) {    if (s[i] === "\\" && i + 1 < s.length) {      const n = s[++i];      out += n === "n" ? "\n" : n;    } else out += s[i];  }  return out;} export function parseDot(text) {  const nodes = new Map();  const edges = [];  const loops = [];  const seen = new Set();  const LABEL = '"((?:[^"\\\\]|\\\\.)*)"';  const nodeRe = new RegExp(`^(-?\\d+) \\[label=${LABEL}(.*)\\];?\\s*$`);  const edgeRe = new RegExp(`^(-?\\d+) -> (-?\\d+)(?: \\[label=${LABEL})?`);  for (const line of text.split("\n")) {    let m = edgeRe.exec(line);    if (m) {      const e = { from: m[1], to: m[2], action: m[3] ? unescapeDot(m[3]) : "" };      const id = `${e.from} ${e.to} ${e.action}`;      if (seen.has(id)) continue;      seen.add(id);      (e.from === e.to ? loops : edges).push(e);      continue;    }    m = nodeRe.exec(line);    if (m)      nodes.set(m[1], {        id: m[1],        vars: parseState(unescapeDot(m[2])),        init: /style\s*=\s*filled/.test(m[3]),      });  }  if (nodes.size === 0)    throw new Error("no states found; dump the graph with TLC -dump dot,actionlabels <file>");  const missing = [...edges, ...loops].find((e) => !nodes.has(e.from) || !nodes.has(e.to));  if (missing)    throw new Error(      `transition ${missing.from} -> ${missing.to} names a state the file does not define`,    );  if (edges.length > 0 && [...edges, ...loops].every((e) => !e.action))    throw new Error(      "the graph has no action names; dump it with TLC -dump dot,actionlabels <file>",    );  return { nodes, edges, loops };} export function parseTraces(text) {  const traces = [];  let invariant = null;  let current = null;  const lines = text.split("\n");  const stateAt = (i) => {    const body = [];    while (i + 1 < lines.length && lines[i + 1].trim() !== "") body.push(lines[++i]);    return [parseState(body.join("\n")), i];  };  for (let i = 0; i < lines.length; i++) {    const line = lines[i];    const inv = /^Error: Invariant (\S+) is violated( by the initial state:)?/.exec(line);    if (inv) {      invariant = inv[1];      if (inv[2]) {        const [vars, end] = stateAt(i);        traces.push({ invariant, steps: [{ action: null, vars }] });        i = end;      }      continue;    }    if (line.startsWith("Error: ") && !line.startsWith("Error: The behavior up to this point is"))      invariant = null;    const head = /^State (\d+): <([^\s>(]+)/.exec(line);    if (!head) continue;    const [vars, end] = stateAt(i);    i = end;    if (head[1] === "1") {      current = { invariant, steps: [] };      traces.push(current);    }    current?.steps.push({ action: head[2] === "Initial" ? null : head[2], vars });  }  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. 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.*.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/);  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 (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) {  const words = String(text).split(/\s+/);  const rows = [];  let row = "";  for (const w of words) {    if (row && (row + " " + w).length > width) {      rows.push(row);      row = w;    } else row = row ? `${row} ${w}` : w;  }  if (row) rows.push(row);  return rows.join("<br/>");} 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(" "),);export function joinLabels(labels) {  if (labels.length < 2) return labels.join(" or ");  const words = labels.map((l) => String(l).split(" "));  let n = 0;  while (words.every((w) => n < w.length - 1 && w[n] === words[0][n])) n++;  while (n > 0 && OPENS_A_PHRASE.has(words[0][n - 1])) n--;  if (n < 2) return labels.join(" or ");  const rest = words.map((w) => w.slice(n).join(" "));  const list =    rest.length === 2 ? rest.join(" or ") : `${rest.slice(0, -1).join(", ")}, or ${rest.at(-1)}`;  return `${words[0].slice(0, n).join(" ")} ${list}`;} const unwrap = (s) =>

Lines 1–500 of 928. Load more