Content-review

.github/copilot-instructions.md

@@ -19,7 +19,7 @@ This is a **Next.js 14 static site** (`output: "export"`) that teaches TLA+ thro
 
 **Content → Pages → Components flow:**
 
-1. **Lesson definitions** (`src/content/intro/`, `src/content/blocking-queue/`) are TypeScript files exporting a `Lesson` object with `slug`, `title`, `section`, `description` (markdown), `spec` (TLA+ code), `cfg` (TLC config), and optional `extraTabs`/`commitSha` fields.
+1. **Lesson definitions** (`src/content/intro/`, `src/content/blocking-queue/`) are Markdown files with YAML frontmatter and spec/config/tab dividers. `src/lib/parse-lesson.ts` converts them into `Lesson` objects. See `dev/lessons.md` for the format.
 2. **Dynamic routes** (`src/app/intro/[slug]/page.tsx`, `src/app/blocking-queue/[step]/page.tsx`) use `generateStaticParams()` to pre-build all lesson pages.
 3. **LessonLayout** renders a resizable split view: markdown explanation on the left, **Playground** on the right.
 4. **Playground** manages tabbed CodeMirror editors (spec/cfg/extra tabs) and runs TLC via CheerpJ.
@@ -30,7 +30,9 @@ This is a **Next.js 14 static site** (`output: "export"`) that teaches TLA+ thro
 
 ## Conventions
 
-- **Lesson file pattern**: Each lesson is a single TS file in `src/content/<section>/` that default-exports a `Lesson` object. Sections re-export lessons as arrays from their `index.ts`. When adding a lesson, also update the array export and ensure the slug is unique within its section.
+- **Lesson registration**: Intro lessons use the explicit filename list in `src/content/intro/index.ts`; BlockingQueue lessons are automatically discovered and sorted by filename. Keep slugs unique within each section.
+- **Runnable examples**: Every lesson with a spec/config declares `expect: success` or `expect: violation` and explains the expected result. Keep default models practical for the browser. `npm run test:e2e` exercises them through CheerpJ.
+- **BlockingQueue provenance**: Match each lesson to its historical upstream tutorial step and document browser-specific omissions or adaptations. Do not substitute the latest fixed implementation into the introductory buggy example.
 - **`@/` path alias**: Configured in tsconfig and jest for imports from `src/`.
 - **No SSR for CodeEditor**: The `CodeEditor` component is loaded with `dynamic(() => import(...), { ssr: false })` because CodeMirror requires browser APIs.
 - **Tests validate content integrity**: `__tests__/lessons.test.ts` checks lesson counts, unique slugs, non-empty spec/cfg, and correct section assignments. Update expected counts when adding/removing lessons.

README.md

@@ -25,3 +25,5 @@ npm run build     # static export to out/
 ```
 
 Requires Node.js 20+.
+
+See [the lesson authoring guide](dev/lessons.md) for the Markdown format, lesson registration, expected outcomes, and BlockingQueue source alignment.

__tests__/MarkdownContent.test.tsx

@@ -5,6 +5,7 @@ import React from "react";
 import { render, screen } from "@testing-library/react";
 import "@testing-library/jest-dom";
 import MarkdownContent from "@/components/MarkdownContent";
+import { blockingQueueLessons } from "@/content/blocking-queue";
 
 describe("MarkdownContent", () => {
   it("renders headings", () => {
@@ -27,4 +28,23 @@ describe("MarkdownContent", () => {
     render(<MarkdownContent content="Use `inline code` here" />);
     expect(screen.getByText("inline code")).toBeInTheDocument();
   });
+
+  it("preserves the worked deadlock trace as a code block", () => {
+    const lesson = blockingQueueLessons.find((l) => l.slug === "safety");
+    const { container } = render(<MarkdownContent content={lesson!.description} />);
+    const trace = Array.from(container.querySelectorAll("pre code")).find(
+      (code) => code.textContent?.includes("State 8:")
+    );
+    expect(trace?.textContent).toContain("State 1: <Initial predicate>\n");
+    expect(trace?.textContent).toContain("/\\ waitSet = {p1, c1, c2}");
+  });
+
+  it("renders a copyable deadlock-free inequality", () => {
+    const lesson = blockingQueueLessons.find((l) => l.slug === "inequation");
+    const { container } = render(<MarkdownContent content={lesson!.description} />);
+    const code = Array.from(container.querySelectorAll("code")).map(
+      (element) => element.textContent
+    );
+    expect(code).toContain("2 * BufCapacity >= Cardinality(Producers \\cup Consumers)");
+  });
 });

__tests__/lessons.test.ts

@@ -41,4 +41,29 @@ describe("Lesson data", () => {
       expect(lesson.section).toBe("intro");
     }
   });
+
+  it("all runnable lessons declare an expected TLC outcome", () => {
+    for (const lesson of [...introLessons, ...blockingQueueLessons]) {
+      if (!lesson.spec || !lesson.cfg) continue;
+      expect({ slug: lesson.slug, outcome: lesson.expect }).toEqual({
+        slug: lesson.slug,
+        outcome: expect.stringMatching(/^(success|violation)$/),
+      });
+    }
+  });
+
+  it("uses the upstream p2c1b1 configuration for the debugger lesson", () => {
+    const lesson = blockingQueueLessons.find((l) => l.slug === "debug-config");
+    expect(lesson?.cfg).toMatch(/BufCapacity\s*=\s*1/);
+    expect(lesson?.cfg).toMatch(/Producers\s*=\s*\{p1,\s*p2\}/);
+    expect(lesson?.cfg).toMatch(/Consumers\s*=\s*\{c1\}/);
+  });
+
+  it("starts with the buggy single-condition C implementation", () => {
+    const lesson = blockingQueueLessons.find((l) => l.slug === "introduction");
+    const source = lesson?.extraTabs?.find((tab) => tab.label === "C")?.content;
+    expect(source).toContain("pthread_cond_t modify;");
+    expect(source?.match(/pthread_cond_wait\(&modify, &mutex\)/g)).toHaveLength(2);
+    expect(source?.match(/pthread_cond_signal\(&modify\)/g)).toHaveLength(2);
+  });
 });

dev/lessons.md

@@ -9,6 +9,7 @@ Lessons are written as Markdown files with YAML frontmatter and custom divider t
 slug: my-lesson
 title: "My Lesson Title"
 section: intro
+expect: success
 commitSha: "abc123"
 commitUrl: "https://github.com/..."
 ---
@@ -39,7 +40,8 @@ INVARIANT TypeOK
 | `slug` | Yes | URL-friendly identifier for the lesson |
 | `title` | Yes | Display title |
 | `section` | Yes | `"intro"` or `"blocking-queue"` |
-| `commitSha` | No | Git commit SHA (shown in blocking-queue lessons) |
+| `expect` | For runnable lessons | `"success"` for a completed run without errors, or `"violation"` for an intended invariant/property violation or deadlock |
+| `commitSha` | No | Upstream Git commit SHA associated with the lesson |
 | `commitUrl` | No | Link to the commit on GitHub |
 
 ## Divider Tags
@@ -52,21 +54,35 @@ Content is split into sections using divider tags on their own line:
 
 ## File Naming and Ordering
 
-Lesson files are sorted alphabetically by filename. Use numeric prefixes to control order:
+BlockingQueue lesson files are discovered automatically and sorted alphabetically by filename. Use numeric prefixes to control their order:
 
 ```
 01-introduction.md
 02-state-graph.md
 03-larger-config.md
 ```
 
+Intro lessons instead use the explicit `mdFiles` list in `src/content/intro/index.ts`. Add a new filename to that list at the appropriate position; alphabetical naming alone will not register it.
+
 ## Adding a New Lesson
 
 1. Create a new `.md` file in the appropriate `src/content/` subdirectory
-2. Add frontmatter with `slug`, `title`, and `section`
-3. Write the description in Markdown
+2. Add frontmatter with `slug`, `title`, `section`, and the expected outcome in `expect`
+3. Write the description in Markdown, including an **Expected Result** section that explains the default outcome and a small exercise
 4. Add `---TLA_BY_EXAMPLE_SPEC---` followed by the TLA+ spec
 5. Add `---TLA_BY_EXAMPLE_CFG---` followed by the TLC config
 6. Optionally add `---TLA_BY_EXAMPLE_TAB label="..."---` sections for extra tabs
+7. For intro lessons, register the filename in `src/content/intro/index.ts`; BlockingQueue lessons are automatically discovered
+8. Update the lesson counts in `__tests__/lessons.test.ts` when adding or removing a lesson
+
+Use ordinary Markdown backticks and single backslashes for TLA+ operators inside code spans/fences. Do not preserve TypeScript string escaping in Markdown files.
+
+Runnable lessons must have a finite, practical default exploration or a deliberately reachable counterexample. Explain whether a reported error is an invariant violation, a deadlock, or a temporal-property violation. The browser regression suite (`npm run test:e2e`) runs every lesson with a spec and configuration; animation-only lessons omit both and need no `expect`.
+
+## BlockingQueue Source Alignment
+
+Follow the historical steps in [lemmy/BlockingQueue](https://github.com/lemmy/BlockingQueue), not the latest implementation for every page. Keep `commitSha` and `commitUrl` aligned with the corresponding upstream step. Upstream periodically rewrites its history; map revisions by their tutorial step when refreshing references.
+
+Document browser adaptations explicitly: the introduction previews the v02 model beside abridged v01 implementations, the debugger lesson uses the upstream debug constants without its interactive constraint, and the final three configurations omit desktop animation directives. Keep algorithm semantics consistent with the relevant upstream version.
 
-The lesson will be automatically discovered and included - no need to update `index.ts`.
+Quoted state-space totals must specify whether they describe the browser's first-counterexample run or a complete local exploration with `-deadlock -continue`. Include matching constants for any worked trace.

e2e/lessons.spec.ts

@@ -4,29 +4,14 @@ 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);
+const lessons = [...introLessons, ...blockingQueueLessons].filter((l) => l.spec && l.cfg);
 
 test.describe("Lesson TLC regression", () => {
-  test("at least one lesson declares an expected outcome", () => {
+  test("at least one runnable lesson is registered", () => {
     expect(lessons.length).toBeGreaterThan(0);
   });
 
@@ -44,4 +29,16 @@ test.describe("Lesson TLC regression", () => {
       }
     });
   }
+
+  test("intro/basic-operators rejects a green-to-red transition", async ({ page }) => {
+    const lesson = introLessons.find((l) => l.slug === "basic-operators")!;
+    const spec = lesson.spec.replace(
+      'light = "yellow"',
+      'light \\in {"yellow", "green"}'
+    );
+    expect(spec).not.toBe(lesson.spec);
+    await page.goto("/");
+    const output = await runTlcInBrowser(page, spec, lesson.cfg);
+    expect(output).toMatch(/(?:Action property|Temporal properties).*violated/);
+  });
 });

src/app/intro/tla-intuition/TlaIntuitionClient.tsx

@@ -471,7 +471,7 @@ export default function TlaIntuitionClient({ description, spec, prev, next }: Pr
                   The Counterexample Trace
                 </h2>
                 <p className="text-gray-700 leading-relaxed mb-3">
-                  Because TLC uses BFS, the violation it finds is along a{" "}
+                  With one-worker BFS for this invariant, the violation is along a{" "}
                   <strong>shortest path</strong>. TLC reports this as a{" "}
                   <strong>counterexample trace</strong> — the{" "}
                   <span className="text-red-500 font-semibold">red path</span> on
@@ -504,16 +504,20 @@ export default function TlaIntuitionClient({ description, spec, prev, next }: Pr
                   Why This Matters
                 </h2>
                 <p className="text-gray-700 leading-relaxed mb-3">
-                  Traditional testing checks a few paths through your system. TLC
-                  checks <strong>all of them</strong> systematically. It explored{" "}
-                  {GRAPH.expansionSteps.length} states before finding the violation
-                  — and because of BFS, the counterexample is guaranteed to be the{" "}
-                  <strong>shortest</strong> possible path to the bug.
+                  Traditional testing samples executions. TLC systematically
+                  explores the <strong>reachable state graph</strong> of the
+                  configured model. This animation expanded{" "}
+                  {GRAPH.expansionSteps.length} states before finding the violation.
+                  One-worker BFS gives a <strong>shortest</strong> counterexample
+                  for this invariant check; it does not enumerate every path
+                  through a graph with cycles.
                 </p>
                 <p className="text-gray-700 leading-relaxed mb-3">
-                  For real concurrent systems, the state space can be millions of
-                  states — and TLC will explore them all, finding subtle bugs that
-                  testing would miss.
+                  A completed finite exploration establishes the enabled
+                  invariants for the chosen model and assumptions. It is not a
+                  proof for arbitrary system sizes or for the implementation.
+                  Large models can exhaust available resources, and an unbounded
+                  state space may never finish.
                 </p>
                 <div className="flex gap-2 mt-4 mb-2">
                   <BackBtn />

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

@@ -3,8 +3,8 @@ slug: introduction
 expect: success
 title: Introduction
 section: blocking-queue
-commitSha: "11410864"
-commitUrl: "https://github.com/lemmy/BlockingQueue/commit/11410864"
+commitSha: "cc8acf5c"
+commitUrl: "https://github.com/lemmy/BlockingQueue/commit/cc8acf5c"
 ---
 Tutorial-style talk **"Weeks of debugging can save you hours of TLA+"**.
 
@@ -14,28 +14,47 @@ This section is an adaptation of the tutorial by Markus Kuppe from the [Blocking
 
 The problem we model is a **bounded buffer** (blocking queue) shared between producer and consumer threads. Producers add items to the buffer. Consumers remove items from the buffer. When the buffer is full, producers wait. When the buffer is empty, consumers wait.
 
+## Following the Upstream Tutorial
+
+These lessons follow upstream v01-v08a and v11-v13. The optional trace-animation steps in between are omitted. Each lesson links to its corresponding upstream commit; the upstream history is periodically rewritten, so use the linked revision rather than assuming the latest branch represents that step.
+
+The Java and C tabs are abridged versions of the original v01 implementations. Both use a single wait set/condition and can deadlock; the C tab omits the upstream logging. The playground previews the minimal v02 model because v01 introduces the implementation before the TLA+ spec.
+
+The browser runs standalone specifications, not the desktop debugger or trace animator. The final three lessons omit upstream's animation-only configuration entries while retaining the algorithm and its safety invariants.
+
 ## Running the Java Implementation
 
-```
+Run these commands in a new clone with a JDK installed:
+
+```bash
 git clone https://github.com/lemmy/BlockingQueue.git
 cd BlockingQueue
-java -cp impl/src/ org.kuppe.App
+git switch --detach cc8acf5c8c47eccb6064941937567353b414ddc4
+mkdir -p build/classes
+javac -d build/classes impl/src/org/kuppe/*.java
+java -cp build/classes org.kuppe.App
 ```
 
-This launches the application with the default configuration **p4c3b3** (4 producers, 3 consumers, buffer capacity 3). The application may deadlock - that is the bug we will investigate with TLA+.
+This launches the original application with the default configuration **p4c3b3** (4 producers, 3 consumers, buffer capacity 3). It runs indefinitely and may deadlock; stop it with Ctrl+C. The current upstream branch already includes later fixes, which is why selecting the historical revision matters.
 
 ## Running the C Implementation
 
-```
+In the same historical checkout, after stopping Java, use GCC and Make:
+
+```bash
 cd impl
 make
 ./producer_consumer 3 4 3
 ```
 
-This is a C implementation of the same blocking buffer problem.
+This runs the original single-condition C implementation with the same parameters. Stop it with Ctrl+C.
 
 You can follow along using the [TLA+ VS Code extension](https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus) or via [Gitpod](https://gitpod.io/) / [GitHub Codespaces](https://github.com/features/codespaces).
 
+## Expected Result
+
+The playground's smaller **p1c1b1** model completes without a deadlock. This does not establish that the implementation is safe for the larger **p4c3b3** configuration. Try adding a second consumer to the configuration; the later lessons explain the resulting deadlock.
+
 ---TLA_BY_EXAMPLE_SPEC---
 --------------------------- MODULE BlockingQueue ---------------------------
 (***************************************************************************)
@@ -278,7 +297,7 @@ uint32_t buff_size, numProducers, numConsumers;
 uint32_t *buffer;
 uint32_t fillIndex, useIndex, count = 0;
 
-pthread_cond_t empty, full; 
+pthread_cond_t modify;
 pthread_mutex_t mutex;
 
 void append(uint32_t value) {
@@ -298,10 +317,10 @@ void *producer (void * arg) {
 while(1) {
 pthread_mutex_lock(&mutex);
 while (count == buff_size) {
-    pthread_cond_wait(&empty, &mutex);
+    pthread_cond_wait(&modify, &mutex);
 }
 append(rand() % (10));
-pthread_cond_signal(&full);
+pthread_cond_signal(&modify);
         pthread_mutex_unlock(&mutex);
 }
 }
@@ -311,10 +330,10 @@ uint32_t id = *((uint32_t *) arg);
 while(1) {
 pthread_mutex_lock(&mutex);
 while (count == 0) {
-pthread_cond_wait(&full, &mutex);
+pthread_cond_wait(&modify, &mutex);
 }
 head();
-pthread_cond_signal(&empty);
+pthread_cond_signal(&modify);
 pthread_mutex_unlock(&mutex);
 } 
 }
@@ -330,8 +349,7 @@ numProducers = atoi(argv[2]);
 numConsumers = atoi(argv[3]);
 
 pthread_mutex_init(&mutex, NULL);
-pthread_cond_init(&empty, NULL);
-pthread_cond_init(&full, NULL);
+pthread_cond_init(&modify, NULL);
 
 buffer = malloc(sizeof(int) * buff_size);
 pthread_t prods[numProducers], cons[numConsumers];