Continuous (smoke) testing with TLC simulator upon editor save

[lemmy]

Hi-res screencast at https://www.youtube.com/watch?v=jcsQzzeVjuI

---

Install/Activate

Prerequisite: Install vscode-tlaplus nightly build!

Let Spec.tla be the spec one is working on. To activate "smoke testing", one has to create SmokeSpec.tla and SmokeSpec.cfg with the following content:

------------------------------- MODULE SmokeSpec -------------------------------
EXTENDS Spec, TLC

\* SmokeInit is configured to re-define the initial predicate. We use  SmokeInit
\* to randomly select a subset of the defined initial states in cases when the
\* set of all initial states is too expensive to generate during smoke testing.
SmokeInit ==
    /\ active = [n \in Node |-> RandomElement(BOOLEAN)]
    /\ pending = [i \in Node |-> 0]
    /\ color = [n \in Node |-> RandomElement(Color)]
    /\ counter = [i \in Node |-> 0]
    /\ pending = [i \in Node |-> 0]
    /\ token = [pos |-> 0, q |-> 0, color |-> "black"]

\* StopAfter  has to be configured as a state constraint. It stops TLC after ~1
\* second or after generating 100 traces, whatever comes first, unless TLC
\* encountered an error.  In this case,  StopAfter  has no relevance.
StopAfter ==
    (* The smoke test has a time budget of 1 second. *)
    \/ TLCSet("exit", TLCGet("duration") > 1)
    (* Generating 100 traces should provide reasonable coverage. *)
    \/ TLCSet("exit", TLCGet("diameter") > 100)

===============================================================================

CONSTANT
    \* An ordinary spec constant. 
    N = 3
    \* Force TLC to only generate a few initial states out of the set of all initial states.
    Init <- SmokeInit
SPECIFICATION Spec
INVARIANT TypeOK
\* 
CONSTRAINT StopAfter
\* Checking deadlocks is unlikely useful for smoke testing.
CHECK_DEADLOCK FALSE 

Additionally, activate source actions:

    "[tlaplus]": {
        "editor.codeActionsOnSave": {
            "source": true
        }
    }

---

Unsupported at this point:

• Runs smoke tests on all changes. Should run only if AST and/or semantic graph changes.
• Can only run simulation mode. Should support running BFS (for tiny models).

TODO

Code

• [x] Do not launch TLC/TLA+ debugger if the spec does not parse (otherwise, a annoying dialog pops up that VSCode cannot connect to the debugger
• [ ] "Check last run" on the result page runs SmokeMC... if 1) Ordinary model-checking runs 2) Smoke testing kicks in 3) User clicks "Check last run"
  • Depends on https://github.com/alygin/vscode-tlaplus/pull/222/commits/2e30a6c697ab3d4267b102e6ddb795ff9134cc84
• [x] Cannot pass nosuspend to TLA+ debugger
• [x] Terminate (kill) TLC upon save of the editor when editor (debugger) showed an error
• [x] Dedicated Code action provider, as replacement for Save and Run Ext extension, with which users can run TLC upon save
  • Disadvantage of standalone Save and Run Ext extension is not just overhead for users, but also overhead during development
  • Our extension already comes with a TlaCodeActionProvider Code Action Provider in actions.ts
  • Spawning/Terminating TLC from within a provider would be straight forward

TLC

• [x] Halt debugger on invariant violations (here TypeOK is especially interesting)
• [x] Halt debugger on "Error: Successor state is not completely specified by the next-state action", i.e., when variables are missing from UNCHANGED
• [x] ~Halt on EC 2143 "The variable token was changed while it is specified as UNCHANGED at ..."~
• [x] Debugger shortly jumps to a random stack frame upon connect (return empty array from tlc2.debug.TLCDebugger.stackTrace(StackTraceArguments) unless TLC waits at a breakpoint)
• [x] Non-atomically generate initial states when generating set of initial states is too expensive

[lemmy]

Hack that adds the command tlaplus.debugger.smoke mentioned above:

diff --git a/package.json b/package.json
index 23a6451..e3d1135 100644
--- a/package.json
+++ b/package.json
@@ -192,6 +192,13 @@
                 "icon": "$(debug-alt)",
                 "category": "TLA+"
             },
+            {
+                "command": "tlaplus.debugger.smoke",
+                "title": "Smoke Test Spec",
+                "enablement": "!inDebugMode",
+                "icon": "$(debug-alt)",
+                "category": "TLA+"
+            },
             {
                 "command": "tlaplus.debugger.attach",
                 "title": "Debug a running model",
diff --git a/src/debugger/debugging.ts b/src/debugger/debugging.ts
index c6e2d05..946acc6 100644
--- a/src/debugger/debugging.ts
+++ b/src/debugger/debugging.ts
@@ -3,6 +3,7 @@ import {
     doCheckModel, getSpecFiles
 } from '../commands/checkModel';
 
+export const TLAPLUS_DEBUG_LAUNCH_SMOKE = 'tlaplus.debugger.smoke';
 export const TLAPLUS_DEBUG_LAUNCH_CHECKNDEBUG = 'tlaplus.debugger.run';
 export const TLAPLUS_DEBUG_LAUNCH_DEBUG = 'tlaplus.debugger.attach';
 
@@ -73,3 +74,39 @@ export async function checkAndDebugSpec(
     // Don't await doCheckModel because it only returns after TLC terminates.
     doCheckModel(specFiles, false, context, diagnostic, true, ['-debugger', `port=${initPort}`], portOpenCallback);
 }
+
+export async function smokeTestSpec(
+    resource: vscode.Uri | undefined,
+    diagnostic: vscode.DiagnosticCollection,
+    context: vscode.ExtensionContext
+): Promise<void> {
+    let targetResource = resource;
+    if (!targetResource && vscode.window.activeTextEditor) {
+        // Since this command is registered as a button on the editor menu, I don't
+        // think this branch is ever taken.  It's here because the DAP example has it.
+        targetResource = vscode.window.activeTextEditor.document.uri;
+    }
+    if (!targetResource) {
+        return;
+    }
+    const specFiles = await getSpecFiles(targetResource);
+    if (!specFiles) {
+        return;
+    }
+    // Randomly select a port on which we request the debugger to listen
+    const initPort = Math.floor(Math.random() * (DEBUGGER_MAX_PORT - DEBUGGER_MIN_PORT)) + DEBUGGER_MIN_PORT;
+    // This will be called as soon as TLC starts listening on a port or fails to start
+    const portOpenCallback = (port?: number) => {
+        if (!port) {
+            return;
+        }
+        vscode.debug.startDebugging(undefined, {
+            type: 'tlaplus',
+            name: 'Debug Spec',
+            request: 'launch',
+            port: port
+        });
+    };
+    // Don't await doCheckModel because it only returns after TLC terminates.
+    doCheckModel(specFiles, false, context, diagnostic, false, ['-simulate', 'num=10', '-noTE', '-deadlock', '-debugger', `port=${initPort}`], portOpenCallback);
+}
diff --git a/src/main.ts b/src/main.ts
index 083600f..51da31a 100644
--- a/src/main.ts
+++ b/src/main.ts
@@ -6,8 +6,8 @@ import {
     showTlcOutput, checkModelCustom, CMD_CHECK_MODEL_RUN_AGAIN, runLastCheckAgain
 } from './commands/checkModel';
 import { CMD_RUN_REPL, launchRepl, REPLTerminalProfileProvider } from './commands/runRepl';
-import { TLAPLUS_DEBUG_LAUNCH_CHECKNDEBUG, TLAPLUS_DEBUG_LAUNCH_DEBUG,
-    TLADebugAdapterServerDescriptorFactory, checkAndDebugSpec, attachDebugger } from './debugger/debugging';
+import { TLAPLUS_DEBUG_LAUNCH_CHECKNDEBUG, TLAPLUS_DEBUG_LAUNCH_DEBUG,TLAPLUS_DEBUG_LAUNCH_SMOKE, 
+    TLADebugAdapterServerDescriptorFactory, checkAndDebugSpec, attachDebugger, smokeTestSpec } from './debugger/debugging';
 import { CMD_EVALUATE_SELECTION, evaluateSelection, CMD_EVALUATE_EXPRESSION,
     evaluateExpression } from './commands/evaluateExpression';
 import { parseModule, CMD_PARSE_MODULE } from './commands/parseModule';
@@ -119,6 +119,10 @@ export function activate(context: vscode.ExtensionContext): void {
             TLAPLUS_DEBUG_LAUNCH_CHECKNDEBUG,
             (uri) => checkAndDebugSpec(uri, diagnostic, context)
         ),
+        vscode.commands.registerCommand(
+            TLAPLUS_DEBUG_LAUNCH_SMOKE,
+            (uri) => smokeTestSpec(uri, diagnostic, context)
+        ),
         vscode.commands.registerCommand(
             TLAPLUS_DEBUG_LAUNCH_DEBUG,
             (uri) => attachDebugger()

[lemmy]

Prerequisite: Install vscode-tlaplus nightly build!

Let Spec.tla be the spec one is working on. To activate "smoke testing", one has to create SmokeSpec.tla and SmokeSpec.cfg with the following content:

------------------------------- MODULE SmokeSpec -------------------------------
EXTENDS Spec, TLC

\* SmokeInit is configured to re-define the initial predicate. We use  SmokeInit
\* to randomly select a subset of the defined initial states in cases when the
\* set of all initial states is too expensive to generate during smoke testing.
SmokeInit ==
    /\ active = [n \in Node |-> RandomElement(BOOLEAN)]
    /\ pending = [i \in Node |-> 0]
    /\ color = [n \in Node |-> RandomElement(Color)]
    /\ counter = [i \in Node |-> 0]
    /\ pending = [i \in Node |-> 0]
    /\ token = [pos |-> 0, q |-> 0, color |-> "black"]

\* StopAfter  has to be configured as a state constraint. It stops TLC after ~1
\* second or after generating 100 traces, whatever comes first, unless TLC
\* encountered an error.  In this case,  StopAfter  has no relevance.
StopAfter ==
    (* The smoke test has a time budget of 1 second. *)
    \/ TLCSet("exit", TLCGet("duration") > 1)
    (* Generating 100 traces should provide reasonable coverage. *)
    \/ TLCSet("exit", TLCGet("diameter") > 100)

===============================================================================

CONSTANT
    \* An ordinary spec constant. 
    N = 3
    \* Force TLC to only generate a few initial states out of the set of all initial states.
    Init <- SmokeInit
SPECIFICATION Spec
INVARIANT TypeOK
\* 
CONSTRAINT StopAfter
\* Checking deadlocks is unlikely useful for smoke testing.
CHECK_DEADLOCK FALSE 

Additionally, activate source actions:

    "[tlaplus]": {
        "editor.codeActionsOnSave": {
            "source": true
        }
    }

Unsupported at this point:

• Runs smoke tests on all changes. Should run only if AST and/or semantic graph changes.
• Can only run simulation mode. Should support running BFS (for tiny models).

[lemmy]

This nonsense is blocking this now. @alygin I suggest we turn SonarCloud off.

Taken care of in https://github.com/alygin/vscode-tlaplus/commit/e8de86c48870cc17bf82f7ef8af0d5dfd7041e8b