import assert from "node:assert/strict";import { spawn, spawnSync } from "node:child_process";import { existsSync, mkdirSync, mkdtempSync, readdirSync, readFileSync, rmSync, writeFileSync,} from "node:fs";import { tmpdir } from "node:os";import { delimiter, dirname, join } from "node:path";import { test } from "node:test";import { setTimeout as sleep } from "node:timers/promises";import { fileURLToPath } from "node:url";import { findTlc, parseDot, parseMermaid, parseTraces, parseValue, ruleSentences, stateKey, tlcOutputWarning, 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 = {}) => { 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")); const main = regions.Main; assert.deepEqual([...main.states].sort(), [ "Nothing chosen", "Upload failed", "Uploaded", "Uploading.Checking the file", "Uploading.Sending the file", ]); assert.deepEqual([...main.initial], ["Nothing chosen"]); assert.deepEqual(edges(main), [ "Nothing chosen -> Uploading.Sending the file : you choose a file", "Upload failed -> Uploading.Sending the file : you retry", "Uploading.Checking the file -> Nothing chosen : you cancel", "Uploading.Checking the file -> Upload failed : the network drops", "Uploading.Checking the file -> Uploaded : the check passes", "Uploading.Sending the file -> Nothing chosen : you cancel", "Uploading.Sending the file -> Upload failed : the network drops", "Uploading.Sending the file -> Uploading.Checking the file : the last byte arrives", ]);}); test("the deepest source wins when a composite and a state inside it share a label", () => { const { regions } = parseMermaid(`stateDiagram-v2 state Form { [*] --> Typing Typing --> Confirm : you press Escape state Confirm } [*] --> Form Form --> Closed : you press Escape Confirm --> Closed : you press Escape`); assert.deepEqual(edges(regions.Main), [ "Form.Confirm -> Closed : you press Escape", "Form.Typing -> Form.Confirm : you press Escape", ]);}); test("a top-level composite split by -- makes one region per part", () => { const { regions, nevers } = parseMermaid(fixture("sync.mmd")); assert.deepEqual(Object.keys(regions), ["Connection", "Sync badge"]); assert.deepEqual(edges(regions["Sync badge"]), [ "Synced -> Waiting to sync : the network drops", "Synced -> Waiting to sync : you edit a note", "Waiting to sync -> Synced : the server confirms", ]); assert.deepEqual(nevers, [ { name: "NeverSyncedWhileOffline", states: ["Offline", "Synced"], sentence: 'You never see "Synced" while you are offline.', }, ]);}); test("a rule's sentence is the comment lines right above it, and a state key ignores field order", () => { const sentences = ruleSentences(`---- MODULE M ----\\* Not about a rule. \\* You never see "Saved"\\* while the note is a draft.NoFalseSaved == TRUEBare == TRUE====`); assert.deepEqual( [...sentences], [["NoFalseSaved", 'You never see "Saved" while the note is a draft.']], ); 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 MaxAgeVARIABLES screen, sent, paid, clockReady == sent > 0Tick == clock' = clock + 1 /\\ UNCHANGED <<screen, sent, paid>>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 <<sent, clock>>\\* fill.ts:10Fill == \\E o \\in 1..3 : /\\ paid = TRUE /\\ clock > 0 /\\ sent' = o + 1 /\\ sent = o /\\ paid => clock > 0 /\\ screen = "Cart" /\\ UNCHANGED <<screen, paid, clock>>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 { state "Works today" as legendWorks } [*] --> A A --> B : go`); assert.deepEqual([...regions.Main.states].sort(), ["A", "B"]);}); test("the parser refuses charts it cannot read", () => { assert.throws(() => parseMermaid("stateDiagram-v2\n state A {\n [*] --> B"), /unclosed/); assert.throws(() => parseMermaid("stateDiagram-v2\n A ==> B"), /cannot read chart line/); assert.throws( () => parseMermaid("stateDiagram-v2\n state A {\n B --> C : go\n }\n [*] --> A"), /no \[\*\] --> start/, ); assert.throws( () => parseMermaid( "stateDiagram-v2\n state A {\n state B {\n [*] --> C\n --\n [*] --> D\n }\n [*] --> B\n }\n [*] --> A", ), /below the top level/, ); assert.throws( () => parseMermaid("stateDiagram-v2\n [*] --> A\n A --> [*] : you close the app"), /final state/, ); assert.throws( () => parseMermaid( 'stateDiagram-v2\n state "Something went wrong" as UploadError\n state "Something went wrong" as SyncError\n [*] --> UploadError\n UploadError --> SyncError : go', ), /two states have the caption "Something went wrong"/, );}); test("the parser reads class shorthand, repeated descriptions, and states first named inside a composite", () => { const { regions } = parseMermaid(`stateDiagram-v2 classDef wrong fill:#fdd N : Nothing chosen N : press Upload to start [*] --> N N:::wrong --> Done : you finish Done --> Moving:::wrong state A { [*] --> X X --> Y : go } Moving --> A : start Y --> Z : next A --> N : cancel`); assert.deepEqual([...regions.Main.states].sort(), [ "A.X", "A.Y", "Done", "Moving", "Nothing chosen", "Z", ]); assert.deepEqual(edges(regions.Main), [ "A.X -> A.Y : go", "A.X -> Nothing chosen : cancel", "A.Y -> Nothing chosen : cancel", "A.Y -> Z : next", "Done -> Moving : ", "Moving -> A.X : start", "Nothing chosen -> Done : you finish", ]);}); test("TLC values, states, graphs, and traces parse", () => { assert.deepEqual(parseValue('[a |-> <<1, "x">>, b |-> {TRUE}]'), { a: [1, "x"], b: [true] }); assert.deepEqual(parseValue('("p" :> 1 @@ "q" :> 2)'), { p: 1, q: 2 }); const graph = parseDot(`strict digraph DiskGraph {1 [label="/\\\\ x = 0",style = filled]2 [label="/\\\\ x = 1"]1 -> 2 [label="Inc",color="black",fontcolor="black"];1 -> 2 [label="Inc",color="black",fontcolor="black"];2 -> 2 [label="Stay"];}`); assert.equal(graph.nodes.get("1").init, true); assert.deepEqual(graph.nodes.get("2").vars, { x: 1 }); assert.deepEqual(graph.edges, [{ from: "1", to: "2", action: "Inc" }]); assert.deepEqual(graph.loops, [{ from: "2", to: "2", action: "Stay" }]); assert.throws( () => parseDot( 'strict digraph DiskGraph {\n1 [label="/\\\\ x = 0",style = filled]\n2 [label="/\\\\ x = 1"]\n1 -> 2;\n}', ), /no action names/, ); const [trace] = parseTraces(`Error: Invariant Small is violated.Error: The behavior up to this point is:State 1: <Initial predicate>x = 0 State 2: <Inc line 9, col 8 to line 9, col 20 of module M>x = 1`); assert.equal(trace.invariant, "Small"); assert.deepEqual(trace.steps, [ { action: null, vars: { x: 0 } }, { action: "Inc", vars: { x: 1 } }, ]);}); const done = "Model checking completed. No error has been found.\n";const evaluationError = `Error: Invariant NoLost is violated.Error: The behavior up to this point is:State 1: <Initial predicate>s = "Idle" State 2: <Lose line 4, col 9 to line 4, col 33 of module F>s = "Lost" Error: TLC threw an unexpected exception.This was probably caused by an error in the spec or model. Error: The behavior up to this point is:State 1: <Initial predicate>s = "Idle" State 2: <Save line 5, col 9 to line 5, col 35 of module F>s = "Saving" 3 states generated, 3 distinct states found, 0 states left on queue.`; test("a rule broken by a start state is a counterexample of one state", () => { const text = `Error: Invariant NeverSyncedWhileOffline is violated by the initial state:/\\ badge = "Synced"/\\ conn = "Offline" ${done}`; assert.doesNotThrow(() => tlcOutputWarning(text, "tlc.out")); assert.deepEqual(parseTraces(text), [ { invariant: "NeverSyncedWhileOffline", steps: [{ action: null, vars: { badge: "Synced", conn: "Offline" } }], }, ]);}); test("TLC output from a run that failed or stopped early is refused", () => { assert.doesNotThrow(() => 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( () => 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( () => tlcOutputWarning("Error: Parsing or semantic analysis failed.\n", "parse.out"), /not a broken rule/, ); assert.throws( () => tlcOutputWarning(evaluationError, "eval.out"), /TLC threw an unexpected exception/, ); assert.throws( () => tlcOutputWarning( "Error: Invariant Small is violated.\nError: The behavior up to this point is:\nState 1: <Initial predicate>\nx = 0\n", "stopped.out", ), /did not finish/, ); assert.deepEqual( parseTraces(evaluationError).map((t) => t.invariant), ["NoLost", null], );}); const tlcThrew = (cls, message) => `Error: Evaluating invariant Small failed.Index 123 out of bounds for length 4Error: 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 nestedexpressions 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: <Initial predicate>\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( 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( tlcOutputWarning(workersInterleaved, "tlc.out"), /failed with java\.lang\.ArrayIndexOutOfBoundsException: Index 123/, ); assert.deepEqual( parseTraces(workersInterleaved).map((t) => t.invariant), ["Small"], ); assert.throws( () => tlcOutputWarning( `${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( () => tlcOutputWarning( `${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( join(dir, "save.dot"), `strict digraph DiskGraph {1 [label="/\\\\ s = \\"Idle\\"",style = filled]2 [label="/\\\\ s = \\"Saving\\""]1 -> 2 [label="Tap"];2 -> 2 [label="Retry"];}`, ); writeFileSync( join(dir, "save.map.mjs"), `export const readerActions = ["Tap"];export const state = (v, facts) => (v.s === "Idle" ? 'Badge says "Synced"' : facts.settled ? "Saved" : "Saving");export const step = (action) => ({ Tap: "you tap Save" })[action] ?? "";`, ); const r = node( "tlc-to-chart.mjs", ["--dot", "save.dot", "--map", "save.map.mjs", "--highlight", "0", "--out", "chart.mmd"], dir, ); assert.equal(r.status, 0, r.stderr); assert.deepEqual(edges(parseMermaid(readFileSync(join(dir, "chart.mmd"), "utf8")).regions.Main), [ 'Badge says "Synced" -> Saving : you tap Save', ]);}); test("chart-to-tla writes one action per label and one invariant per never line", () => { const dir = mkdtempSync(join(tmpdir(), "statechart-")); writeFileSync(join(dir, "sync.mmd"), fixture("sync.mmd")); const r = node("chart-to-tla.mjs", ["sync.mmd", "--module", "Sync"], dir); assert.equal(r.status, 0, r.stderr); const spec = readFileSync(join(dir, "Sync.tla"), "utf8"); assert.match(spec, /^VARIABLES connection, syncBadge$/m); assert.match( spec, /^TheNetworkDrops ==\n {4}\/\\ \(connection \\in \{"Online"\} \\\/ syncBadge \\in \{"Synced"\}\)$/m, ); assert.match( spec, /^NeverSyncedWhileOffline == ~\(connection = "Offline" \/\\ syncBadge = "Synced"\)$/m, ); assert.equal( readFileSync(join(dir, "Sync.cfg"), "utf8"), "SPECIFICATION Spec\nINVARIANT TypeOK\nINVARIANT NeverSyncedWhileOffline\n", ); assert.match(r.stderr, /rules TypeOK NeverSyncedWhileOffline/);}); test("chart-to-tla refuses a never line that names no state", () => { const dir = mkdtempSync(join(tmpdir(), "statechart-")); writeFileSync( join(dir, "c.mmd"), "stateDiagram-v2\n [*] --> A\n A --> B : go\n %% never Bad: C -- never C\n", ); const r = node("chart-to-tla.mjs", ["c.mmd", "--module", "C"], dir); assert.notEqual(r.status, 0); assert.match(r.stderr, /names "C", which is not a state/);}); test("a never line names a state exactly, or every state inside a composite", () => { const dir = mkdtempSync(join(tmpdir(), "statechart-")); writeFileSync( join(dir, "c.mmd"), `stateDiagram-v2 state "Saving" as S state "Saving..." as S2 state Busy { [*] --> Checking Checking --> Sending : the check passes } [*] --> S S --> S2 : you wait S2 --> Busy : you send Busy --> S : you cancel %% never NoSaving: Saving -- You never see Saving. %% never NoBusy: Busy -- You are never busy.`, ); const r = node("chart-to-tla.mjs", ["c.mmd", "--module", "C"], dir); assert.equal(r.status, 0, r.stderr); const spec = readFileSync(join(dir, "C.tla"), "utf8"); assert.match(spec, /^NoSaving == ~\(main = "Saving"\)$/m); assert.match(spec, /^NoBusy == ~\(main \\in \{"Busy\.Checking", "Busy\.Sending"\}\)$/m); assert.match( readFileSync(join(dir, "C.map.mjs"), "utf8"), /^export const readerActions = \[\];$/m, );}); const door = `stateDiagram-v2 state Door { [*] --> Locked Locked --> Unlocked : tap unlock Unlocked --> Locked : tap lock -- [*] --> Closed Closed --> Open : open the door Open --> Closed : close the door } [*] --> Door`;const flatDoor = (extra = []) => [ "stateDiagram-v2", ' state "Locked | Closed" as L_C', ' state "Locked | Open" as L_O', ' state "Unlocked | Closed" as U_C', ' state "Unlocked | Open" as U_O', " [*] --> L_C", " L_C --> U_C : tap unlock", " U_C --> L_C : tap lock", " L_O --> U_O : tap unlock", " L_C --> L_O : open the door", " L_O --> L_C : close the door", " U_C --> U_O : open the door", " U_O --> U_C : close the door", ...extra, ].join("\n");Lines 1–500 of 3291. Load more
import assert from "node:assert/strict"; import { spawn, spawnSync } from "node:child_process"; import { existsSync, mkdirSync, mkdtempSync, readdirSync, readFileSync, rmSync, writeFileSync, } from "node:fs"; import { tmpdir } from "node:os"; import { delimiter, dirname, join } from "node:path"; import { test } from "node:test"; import { setTimeout as sleep } from "node:timers/promises"; import { fileURLToPath } from "node:url"; import { findTlc, parseDot, parseMermaid, parseTraces, parseValue, ruleSentences, stateKey, tlcOutputWarning, 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 = {}) => { 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")); const main = regions.Main; assert.deepEqual([...main.states].sort(), [ "Nothing chosen", "Upload failed", "Uploaded", "Uploading.Checking the file", "Uploading.Sending the file", ]); assert.deepEqual([...main.initial], ["Nothing chosen"]); assert.deepEqual(edges(main), [ "Nothing chosen -> Uploading.Sending the file : you choose a file", "Upload failed -> Uploading.Sending the file : you retry", "Uploading.Checking the file -> Nothing chosen : you cancel", "Uploading.Checking the file -> Upload failed : the network drops", "Uploading.Checking the file -> Uploaded : the check passes", "Uploading.Sending the file -> Nothing chosen : you cancel", "Uploading.Sending the file -> Upload failed : the network drops", "Uploading.Sending the file -> Uploading.Checking the file : the last byte arrives", ]); }); test("the deepest source wins when a composite and a state inside it share a label", () => { const { regions } = parseMermaid(`stateDiagram-v2 state Form { [*] --> Typing Typing --> Confirm : you press Escape state Confirm } [*] --> Form Form --> Closed : you press Escape Confirm --> Closed : you press Escape`); assert.deepEqual(edges(regions.Main), [ "Form.Confirm -> Closed : you press Escape", "Form.Typing -> Form.Confirm : you press Escape", ]); }); test("a top-level composite split by -- makes one region per part", () => { const { regions, nevers } = parseMermaid(fixture("sync.mmd")); assert.deepEqual(Object.keys(regions), ["Connection", "Sync badge"]); assert.deepEqual(edges(regions["Sync badge"]), [ "Synced -> Waiting to sync : the network drops", "Synced -> Waiting to sync : you edit a note", "Waiting to sync -> Synced : the server confirms", ]); assert.deepEqual(nevers, [ { name: "NeverSyncedWhileOffline", states: ["Offline", "Synced"], sentence: 'You never see "Synced" while you are offline.', }, ]); }); test("a rule's sentence is the comment lines right above it, and a state key ignores field order", () => { const sentences = ruleSentences(`---- MODULE M ---- \\* Not about a rule. \\* You never see "Saved" \\* while the note is a draft. NoFalseSaved == TRUE Bare == TRUE ====`); assert.deepEqual( [...sentences], [["NoFalseSaved", 'You never see "Saved" while the note is a draft.']], ); 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 <<screen, sent, paid>> 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 <<sent, clock>> \\* fill.ts:10 Fill == \\E o \\in 1..3 : /\\ paid = TRUE /\\ clock > 0 /\\ sent' = o + 1 /\\ sent = o /\\ paid => clock > 0 /\\ screen = "Cart" /\\ UNCHANGED <<screen, paid, clock>> 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 { state "Works today" as legendWorks } [*] --> A A --> B : go`); assert.deepEqual([...regions.Main.states].sort(), ["A", "B"]); }); test("the parser refuses charts it cannot read", () => { assert.throws(() => parseMermaid("stateDiagram-v2\n state A {\n [*] --> B"), /unclosed/); assert.throws(() => parseMermaid("stateDiagram-v2\n A ==> B"), /cannot read chart line/); assert.throws( () => parseMermaid("stateDiagram-v2\n state A {\n B --> C : go\n }\n [*] --> A"), /no \[\*\] --> start/, ); assert.throws( () => parseMermaid( "stateDiagram-v2\n state A {\n state B {\n [*] --> C\n --\n [*] --> D\n }\n [*] --> B\n }\n [*] --> A", ), /below the top level/, ); assert.throws( () => parseMermaid("stateDiagram-v2\n [*] --> A\n A --> [*] : you close the app"), /final state/, ); assert.throws( () => parseMermaid( 'stateDiagram-v2\n state "Something went wrong" as UploadError\n state "Something went wrong" as SyncError\n [*] --> UploadError\n UploadError --> SyncError : go', ), /two states have the caption "Something went wrong"/, ); }); test("the parser reads class shorthand, repeated descriptions, and states first named inside a composite", () => { const { regions } = parseMermaid(`stateDiagram-v2 classDef wrong fill:#fdd N : Nothing chosen N : press Upload to start [*] --> N N:::wrong --> Done : you finish Done --> Moving:::wrong state A { [*] --> X X --> Y : go } Moving --> A : start Y --> Z : next A --> N : cancel`); assert.deepEqual([...regions.Main.states].sort(), [ "A.X", "A.Y", "Done", "Moving", "Nothing chosen", "Z", ]); assert.deepEqual(edges(regions.Main), [ "A.X -> A.Y : go", "A.X -> Nothing chosen : cancel", "A.Y -> Nothing chosen : cancel", "A.Y -> Z : next", "Done -> Moving : ", "Moving -> A.X : start", "Nothing chosen -> Done : you finish", ]); }); test("TLC values, states, graphs, and traces parse", () => { assert.deepEqual(parseValue('[a |-> <<1, "x">>, b |-> {TRUE}]'), { a: [1, "x"], b: [true] }); assert.deepEqual(parseValue('("p" :> 1 @@ "q" :> 2)'), { p: 1, q: 2 }); const graph = parseDot(`strict digraph DiskGraph { 1 [label="/\\\\ x = 0",style = filled] 2 [label="/\\\\ x = 1"] 1 -> 2 [label="Inc",color="black",fontcolor="black"]; 1 -> 2 [label="Inc",color="black",fontcolor="black"]; 2 -> 2 [label="Stay"]; }`); assert.equal(graph.nodes.get("1").init, true); assert.deepEqual(graph.nodes.get("2").vars, { x: 1 }); assert.deepEqual(graph.edges, [{ from: "1", to: "2", action: "Inc" }]); assert.deepEqual(graph.loops, [{ from: "2", to: "2", action: "Stay" }]); assert.throws( () => parseDot( 'strict digraph DiskGraph {\n1 [label="/\\\\ x = 0",style = filled]\n2 [label="/\\\\ x = 1"]\n1 -> 2;\n}', ), /no action names/, ); const [trace] = parseTraces(`Error: Invariant Small is violated. Error: The behavior up to this point is: State 1: <Initial predicate> x = 0 State 2: <Inc line 9, col 8 to line 9, col 20 of module M> x = 1 `); assert.equal(trace.invariant, "Small"); assert.deepEqual(trace.steps, [ { action: null, vars: { x: 0 } }, { action: "Inc", vars: { x: 1 } }, ]); }); const done = "Model checking completed. No error has been found.\n"; const evaluationError = `Error: Invariant NoLost is violated. Error: The behavior up to this point is: State 1: <Initial predicate> s = "Idle" State 2: <Lose line 4, col 9 to line 4, col 33 of module F> s = "Lost" Error: TLC threw an unexpected exception. This was probably caused by an error in the spec or model. Error: The behavior up to this point is: State 1: <Initial predicate> s = "Idle" State 2: <Save line 5, col 9 to line 5, col 35 of module F> s = "Saving" 3 states generated, 3 distinct states found, 0 states left on queue. `; test("a rule broken by a start state is a counterexample of one state", () => { const text = `Error: Invariant NeverSyncedWhileOffline is violated by the initial state: /\\ badge = "Synced" /\\ conn = "Offline" ${done}`; assert.doesNotThrow(() => tlcOutputWarning(text, "tlc.out")); assert.deepEqual(parseTraces(text), [ { invariant: "NeverSyncedWhileOffline", steps: [{ action: null, vars: { badge: "Synced", conn: "Offline" } }], }, ]); }); test("TLC output from a run that failed or stopped early is refused", () => { assert.doesNotThrow(() => 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( () => 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( () => tlcOutputWarning("Error: Parsing or semantic analysis failed.\n", "parse.out"), /not a broken rule/, ); assert.throws( () => tlcOutputWarning(evaluationError, "eval.out"), /TLC threw an unexpected exception/, ); assert.throws( () => tlcOutputWarning( "Error: Invariant Small is violated.\nError: The behavior up to this point is:\nState 1: <Initial predicate>\nx = 0\n", "stopped.out", ), /did not finish/, ); assert.deepEqual( parseTraces(evaluationError).map((t) => t.invariant), ["NoLost", null], ); }); 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: <Initial predicate>\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( 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( tlcOutputWarning(workersInterleaved, "tlc.out"), /failed with java\.lang\.ArrayIndexOutOfBoundsException: Index 123/, ); assert.deepEqual( parseTraces(workersInterleaved).map((t) => t.invariant), ["Small"], ); assert.throws( () => tlcOutputWarning( `${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( () => tlcOutputWarning( `${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( join(dir, "save.dot"), `strict digraph DiskGraph { 1 [label="/\\\\ s = \\"Idle\\"",style = filled] 2 [label="/\\\\ s = \\"Saving\\""] 1 -> 2 [label="Tap"]; 2 -> 2 [label="Retry"]; }`, ); writeFileSync( join(dir, "save.map.mjs"), `export const readerActions = ["Tap"]; export const state = (v, facts) => (v.s === "Idle" ? 'Badge says "Synced"' : facts.settled ? "Saved" : "Saving"); export const step = (action) => ({ Tap: "you tap Save" })[action] ?? ""; `, ); const r = node( "tlc-to-chart.mjs", ["--dot", "save.dot", "--map", "save.map.mjs", "--highlight", "0", "--out", "chart.mmd"], dir, ); assert.equal(r.status, 0, r.stderr); assert.deepEqual(edges(parseMermaid(readFileSync(join(dir, "chart.mmd"), "utf8")).regions.Main), [ 'Badge says "Synced" -> Saving : you tap Save', ]); }); test("chart-to-tla writes one action per label and one invariant per never line", () => { const dir = mkdtempSync(join(tmpdir(), "statechart-")); writeFileSync(join(dir, "sync.mmd"), fixture("sync.mmd")); const r = node("chart-to-tla.mjs", ["sync.mmd", "--module", "Sync"], dir); assert.equal(r.status, 0, r.stderr); const spec = readFileSync(join(dir, "Sync.tla"), "utf8"); assert.match(spec, /^VARIABLES connection, syncBadge$/m); assert.match( spec, /^TheNetworkDrops ==\n {4}\/\\ \(connection \\in \{"Online"\} \\\/ syncBadge \\in \{"Synced"\}\)$/m, ); assert.match( spec, /^NeverSyncedWhileOffline == ~\(connection = "Offline" \/\\ syncBadge = "Synced"\)$/m, ); assert.equal( readFileSync(join(dir, "Sync.cfg"), "utf8"), "SPECIFICATION Spec\nINVARIANT TypeOK\nINVARIANT NeverSyncedWhileOffline\n", ); assert.match(r.stderr, /rules TypeOK NeverSyncedWhileOffline/); }); test("chart-to-tla refuses a never line that names no state", () => { const dir = mkdtempSync(join(tmpdir(), "statechart-")); writeFileSync( join(dir, "c.mmd"), "stateDiagram-v2\n [*] --> A\n A --> B : go\n %% never Bad: C -- never C\n", ); const r = node("chart-to-tla.mjs", ["c.mmd", "--module", "C"], dir); assert.notEqual(r.status, 0); assert.match(r.stderr, /names "C", which is not a state/); }); test("a never line names a state exactly, or every state inside a composite", () => { const dir = mkdtempSync(join(tmpdir(), "statechart-")); writeFileSync( join(dir, "c.mmd"), `stateDiagram-v2 state "Saving" as S state "Saving..." as S2 state Busy { [*] --> Checking Checking --> Sending : the check passes } [*] --> S S --> S2 : you wait S2 --> Busy : you send Busy --> S : you cancel %% never NoSaving: Saving -- You never see Saving. %% never NoBusy: Busy -- You are never busy. `, ); const r = node("chart-to-tla.mjs", ["c.mmd", "--module", "C"], dir); assert.equal(r.status, 0, r.stderr); const spec = readFileSync(join(dir, "C.tla"), "utf8"); assert.match(spec, /^NoSaving == ~\(main = "Saving"\)$/m); assert.match(spec, /^NoBusy == ~\(main \\in \{"Busy\.Checking", "Busy\.Sending"\}\)$/m); assert.match( readFileSync(join(dir, "C.map.mjs"), "utf8"), /^export const readerActions = \[\];$/m, ); }); const door = `stateDiagram-v2 state Door { [*] --> Locked Locked --> Unlocked : tap unlock Unlocked --> Locked : tap lock -- [*] --> Closed Closed --> Open : open the door Open --> Closed : close the door } [*] --> Door`; const flatDoor = (extra = []) => [ "stateDiagram-v2", ' state "Locked | Closed" as L_C', ' state "Locked | Open" as L_O', ' state "Unlocked | Closed" as U_C', ' state "Unlocked | Open" as U_O', " [*] --> L_C", " L_C --> U_C : tap unlock", " U_C --> L_C : tap lock", " L_O --> U_O : tap unlock", " L_C --> L_O : open the door", " L_O --> L_C : close the door", " U_C --> U_O : open the door", " U_O --> U_C : close the door", ...extra, ].join("\n");