Add pluggable in-browser TLC regression tests for lessons

.github/workflows/ci.yml

@@ -78,3 +78,46 @@ jobs:
                 body,
               });
             }
+
+  # In-browser TLC regression suite: runs every lesson (that declares an
+  # `expect` outcome) through the real CheerpJ worker and asserts the result.
+  # Needs a real browser + network (CheerpJ CDN). Runs on PRs (so changes can
+  # be validated before merge) and on merges to main.
+  e2e:
+    runs-on: ubuntu-latest
+    timeout-minutes: 25
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - name: Checkout Examples repo
+        uses: actions/checkout@v4
+        with:
+          repository: tlaplus/Examples
+          path: Examples
+
+      - name: Setup Node.js
+        uses: actions/setup-node@v4
+        with:
+          node-version: '20'
+          cache: 'npm'
+
+      - name: Download latest TLC JAR
+        run: curl -fSL -o public/tlaplus-web-cheerpj.jar https://github.com/FedericoPonzi/tlaplus-web/releases/latest/download/tlaplus-web-cheerpj.jar
+
+      - name: Install dependencies
+        run: npm ci
+
+      - name: Install Playwright browser
+        run: npx playwright install --with-deps chromium
+
+      - name: Run lesson regression suite
+        run: npm run test:e2e
+
+      - name: Upload Playwright report on failure
+        if: failure()
+        uses: actions/upload-artifact@v4
+        with:
+          name: playwright-report
+          path: playwright-report/
+          retention-days: 14

.gitignore

@@ -4,3 +4,5 @@ out/
 Examples/
 *.tsbuildinfo
 next-env.d.ts
+test-results/
+playwright-report/

e2e/lessons.spec.ts

@@ -0,0 +1,47 @@
+import { test, expect } from "@playwright/test";
+import { introLessons } from "@/content/intro";
+import { blockingQueueLessons } from "@/content/blocking-queue";
+import { runTlcInBrowser, classifyTlcOutput } from "./tlc-runner";
+
+/**
+ * Pluggable, per-lesson in-browser TLC regression suite.
+ *
+ * Every lesson that declares an `expect` field in its markdown frontmatter
+ * (see src/lib/lessons.ts) is model-checked in a real browser via the CheerpJ
+ * worker, and its outcome is asserted:
+ *
+ *   expect: success    -> TLC completes with no error
+ *   expect: violation  -> TLC reports a counterexample (invariant / deadlock)
+ *
+ * To add coverage for a lesson, add `expect: success` or `expect: violation`
+ * to its frontmatter — no test code changes required. Lessons without an
+ * `expect` (e.g. animation-only lessons, lessons with no spec/cfg, or very
+ * large models such as `intro/records` whose state space is impractical to
+ * explore in-browser) are skipped automatically.
+ *
+ * This guards against the class of CheerpJ regression where in-browser TLC
+ * silently stops after computing initial states and misses counterexamples.
+ */
+
+const lessons = [...introLessons, ...blockingQueueLessons].filter((l) => l.expect);
+
+test.describe("Lesson TLC regression", () => {
+  test("at least one lesson declares an expected outcome", () => {
+    expect(lessons.length).toBeGreaterThan(0);
+  });
+
+  for (const lesson of lessons) {
+    test(`${lesson.section}/${lesson.slug} -> ${lesson.expect}`, async ({ page }) => {
+      await page.goto("/");
+      const output = await runTlcInBrowser(page, lesson.spec, lesson.cfg);
+      const { violated, completed } = classifyTlcOutput(output);
+
+      if (lesson.expect === "violation") {
+        expect(violated, `expected a counterexample but none was reported:\n${output}`).toBe(true);
+      } else {
+        expect(violated, `unexpected counterexample:\n${output}`).toBe(false);
+        expect(completed, `expected model checking to complete:\n${output}`).toBe(true);
+      }
+    });
+  }
+});

e2e/tlc-runner.ts

@@ -0,0 +1,59 @@
+import type { Page } from "@playwright/test";
+
+/**
+ * Drives the real in-browser TLC worker (`public/tlc-worker.html`) — the same
+ * CheerpJ runtime + jar the app uses — from within the app origin.
+ *
+ * `page` must already be navigated to the app (e.g. `await page.goto("/")`) so
+ * that the worker iframe is same-origin. Returns the raw TLC output string.
+ *
+ * A fresh Playwright page should be used per call: CheerpJ does not reliably
+ * support many runtime initialisations within a single page.
+ */
+export async function runTlcInBrowser(page: Page, spec: string, cfg: string): Promise<string> {
+  return page.evaluate(
+    ({ spec, cfg }) =>
+      new Promise<string>((resolve) => {
+        const iframe = document.createElement("iframe");
+        iframe.style.display = "none";
+        let done = false;
+        function onMsg(ev: MessageEvent) {
+          if (ev.source !== iframe.contentWindow) return; // ignore the app's own worker
+          const d = ev.data;
+          if (!d || !d.type) return;
+          if (d.type === "ready") {
+            iframe.contentWindow!.postMessage(
+              { type: "run", spec, cfg, workers: 1, checkDeadlock: true, extraModules: [] },
+              "*",
+            );
+          } else if (d.type === "result") {
+            if (done) return;
+            done = true;
+            window.removeEventListener("message", onMsg);
+            iframe.remove();
+            resolve(d.output as string);
+          } else if (d.type === "error") {
+            if (done) return;
+            done = true;
+            window.removeEventListener("message", onMsg);
+            iframe.remove();
+            resolve("INIT ERROR: " + d.message);
+          }
+        }
+        window.addEventListener("message", onMsg);
+        iframe.src = "/tlc-worker.html";
+        document.body.appendChild(iframe);
+      }),
+    { spec, cfg },
+  );
+}
+
+/** Classify a raw TLC output string into the outcome dimensions the suite asserts on. */
+export function classifyTlcOutput(output: string): { violated: boolean; completed: boolean } {
+  return {
+    // A counterexample: an invariant/property violation or a deadlock.
+    violated: /is violated|Deadlock reached/.test(output),
+    // A clean, exhaustive exploration with no error.
+    completed: /Model checking completed/.test(output),
+  };
+}

jest.config.js

@@ -18,4 +18,5 @@ module.exports = {
   moduleNameMapper: {
     "^@/(.*)$": "<rootDir>/src/$1",
   },
+  testPathIgnorePatterns: ["/node_modules/", "/e2e/"],
 };

package.json

@@ -7,7 +7,8 @@
     "build": "next build",
     "start": "next start",
     "lint": "next lint",
-    "test": "jest"
+    "test": "jest",
+    "test:e2e": "playwright test"
   },
   "dependencies": {
     "@codemirror/lang-javascript": "^6.2.4",

playwright.config.ts

@@ -0,0 +1,31 @@
+import { defineConfig, devices } from "@playwright/test";
+
+/**
+ * E2E config for the in-browser TLC checker.
+ *
+ * These tests run TLC inside a real browser via CheerpJ, so they need a browser
+ * and network access (CheerpJ downloads its runtime from a CDN at load time).
+ * They are intentionally kept separate from the jsdom `npm test` unit suite.
+ */
+export default defineConfig({
+  testDir: "./e2e",
+  timeout: 5 * 60 * 1000,
+  expect: { timeout: 4 * 60 * 1000 },
+  fullyParallel: false,
+  workers: 1,
+  reporter: [["list"], ["html", { open: "never" }]],
+  use: {
+    baseURL: "http://localhost:3000",
+    headless: true,
+    trace: "retain-on-failure",
+  },
+  projects: [
+    { name: "chromium", use: { ...devices["Desktop Chrome"] } },
+  ],
+  webServer: {
+    command: "npm run dev",
+    url: "http://localhost:3000",
+    reuseExistingServer: !process.env.CI,
+    timeout: 120 * 1000,
+  },
+});

src/content/blocking-queue/01-introduction.md

@@ -1,5 +1,6 @@
 ---
 slug: introduction
+expect: success
 title: Introduction
 section: blocking-queue
 commitSha: "11410864"

src/content/blocking-queue/02-state-graph.md

@@ -1,5 +1,6 @@
 ---
 slug: state-graph
+expect: success
 title: "State Graph (Minimum Config)"
 section: blocking-queue
 commitSha: "d21cd0fa"

src/content/blocking-queue/03-larger-config.md

@@ -1,5 +1,6 @@
 ---
 slug: larger-config
+expect: violation
 title: "Larger Configuration"
 section: blocking-queue
 commitSha: "7d05fdfa"

src/content/blocking-queue/04-debug-config.md

@@ -1,5 +1,6 @@
 ---
 slug: debug-config
+expect: violation
 title: "Debug State Graph"
 section: blocking-queue
 commitSha: "534f3928"

src/content/blocking-queue/05-safety.md

@@ -1,5 +1,6 @@
 ---
 slug: safety
+expect: violation
 title: "Safety - Detecting Deadlocks"
 section: blocking-queue
 commitSha: "ce99d16a"

src/content/blocking-queue/06-variables.md

@@ -1,5 +1,6 @@
 ---
 slug: variables
+expect: violation
 title: "Constants to Variables"
 section: blocking-queue
 commitSha: "d48bd86a"

src/content/blocking-queue/07-symmetry.md

@@ -1,5 +1,6 @@
 ---
 slug: symmetry
+expect: violation
 title: "Symmetry Sets"
 section: blocking-queue
 commitSha: "553287fd"

src/content/blocking-queue/08-inequation.md

@@ -1,5 +1,6 @@
 ---
 slug: inequation
+expect: violation
 title: "Deadlock-Free Inequation"
 section: blocking-queue
 commitSha: "8e536cba"

src/content/blocking-queue/09-view.md

@@ -1,5 +1,6 @@
 ---
 slug: view
+expect: violation
 title: "View Abstraction"
 section: blocking-queue
 commitSha: "02119f46"

src/content/intro/basic-operators.md

@@ -1,5 +1,6 @@
 ---
 slug: basic-operators
+expect: success
 title: Basic Operators
 section: intro
 ---

src/content/intro/functions.md

@@ -1,5 +1,6 @@
 ---
 slug: functions
+expect: violation
 title: Functions
 section: intro
 ---

src/content/intro/module-structure.md

@@ -1,5 +1,6 @@
 ---
 slug: module-structure
+expect: violation
 title: Module Structure
 section: intro
 ---

src/content/intro/platform.md

@@ -1,5 +1,6 @@
 ---
 slug: platform
+expect: violation
 title: Welcome
 section: intro
 ---

src/content/intro/sequences.md

@@ -1,5 +1,6 @@
 ---
 slug: sequences
+expect: success
 title: Sequences
 section: intro
 ---

src/content/intro/sets.md

@@ -1,5 +1,6 @@
 ---
 slug: sets
+expect: success
 title: Sets
 section: intro
 ---

src/content/intro/tlc-config.md

@@ -1,5 +1,6 @@
 ---
 slug: tlc-config
+expect: success
 title: TLC Configuration
 section: intro
 ---

src/content/intro/variables-constants.md

@@ -1,5 +1,6 @@
 ---
 slug: variables-constants
+expect: violation
 title: "Variables & Constants"
 section: intro
 ---

src/lib/lessons.ts

@@ -15,8 +15,25 @@ export interface Lesson {
   extraTabs?: ExtraTab[];
   commitSha?: string;
   commitUrl?: string;
+  /**
+   * Expected TLC outcome when running this lesson's spec+cfg in the playground.
+   * Consumed by the browser regression suite (e2e/lessons.spec.ts).
+   * Omit for lessons that are not meant to be model-checked standalone
+   * (e.g. animation-only lessons or lessons without a spec/cfg).
+   */
+  expect?: TlcExpectation;
 }
 
+/**
+ * `success`   - TLC explores the whole state space and finds no error
+ *               ("Model checking completed").
+ * `violation` - TLC finds a counterexample: an invariant violation or a
+ *               deadlock ("is violated" / "Deadlock reached"). In this tutorial
+ *               a violation is often the intended teaching outcome
+ *               (e.g. DieHard, or the BlockingQueue deadlock bug stages).
+ */
+export type TlcExpectation = "success" | "violation";
+
 export interface LessonNavInfo {
   slug: string;
   title: string;

src/lib/parse-lesson.ts

@@ -69,6 +69,7 @@ export function parseLesson(markdown: string): Lesson {
 
   if (data.commitSha) lesson.commitSha = data.commitSha;
   if (data.commitUrl) lesson.commitUrl = data.commitUrl;
+  if (data.expect) lesson.expect = data.expect;
   if (extraTabs.length > 0) lesson.extraTabs = extraTabs;
 
   return lesson;