diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md index 3439d93..65d646d 100644 --- a/.github/copilot-instructions.md +++ b/.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/
/` 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. diff --git a/README.md b/README.md index 9be55ec..b13dbb5 100644 --- a/README.md +++ b/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. diff --git a/__tests__/MarkdownContent.test.tsx b/__tests__/MarkdownContent.test.tsx index c03a249..c30c81b 100644 --- a/__tests__/MarkdownContent.test.tsx +++ b/__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(); 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(); + const trace = Array.from(container.querySelectorAll("pre code")).find( + (code) => code.textContent?.includes("State 8:") + ); + expect(trace?.textContent).toContain("State 1: \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(); + const code = Array.from(container.querySelectorAll("code")).map( + (element) => element.textContent + ); + expect(code).toContain("2 * BufCapacity >= Cardinality(Producers \\cup Consumers)"); + }); }); diff --git a/__tests__/lessons.test.ts b/__tests__/lessons.test.ts index d21793c..afcf02a 100644 --- a/__tests__/lessons.test.ts +++ b/__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); + }); }); diff --git a/dev/lessons.md b/dev/lessons.md index 4c57277..f86075e 100644 --- a/dev/lessons.md +++ b/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,7 +54,7 @@ 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 @@ -60,13 +62,27 @@ Lesson files are sorted alphabetically by filename. Use numeric prefixes to cont 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. diff --git a/e2e/lessons.spec.ts b/e2e/lessons.spec.ts index 3bddd56..6e335fe 100644 --- a/e2e/lessons.spec.ts +++ b/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/); + }); }); diff --git a/src/app/intro/tla-intuition/TlaIntuitionClient.tsx b/src/app/intro/tla-intuition/TlaIntuitionClient.tsx index 94ce2e9..8bd8503 100644 --- a/src/app/intro/tla-intuition/TlaIntuitionClient.tsx +++ b/src/app/intro/tla-intuition/TlaIntuitionClient.tsx @@ -471,7 +471,7 @@ export default function TlaIntuitionClient({ description, spec, prev, next }: Pr The Counterexample Trace

- Because TLC uses BFS, the violation it finds is along a{" "} + With one-worker BFS for this invariant, the violation is along a{" "} shortest path. TLC reports this as a{" "} counterexample trace — the{" "} red path on @@ -504,16 +504,20 @@ export default function TlaIntuitionClient({ description, spec, prev, next }: Pr Why This Matters

- Traditional testing checks a few paths through your system. TLC - checks all of them systematically. It explored{" "} - {GRAPH.expansionSteps.length} states before finding the violation - — and because of BFS, the counterexample is guaranteed to be the{" "} - shortest possible path to the bug. + Traditional testing samples executions. TLC systematically + explores the reachable state graph of the + configured model. This animation expanded{" "} + {GRAPH.expansionSteps.length} states before finding the violation. + One-worker BFS gives a shortest counterexample + for this invariant check; it does not enumerate every path + through a graph with cycles.

- 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.

diff --git a/src/content/blocking-queue/01-introduction.md b/src/content/blocking-queue/01-introduction.md index d308d84..9819bea 100644 --- a/src/content/blocking-queue/01-introduction.md +++ b/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]; diff --git a/src/content/blocking-queue/02-state-graph.md b/src/content/blocking-queue/02-state-graph.md index d6a8c1f..7a96067 100644 --- a/src/content/blocking-queue/02-state-graph.md +++ b/src/content/blocking-queue/02-state-graph.md @@ -3,8 +3,8 @@ slug: state-graph expect: success title: "State Graph (Minimum Config)" section: blocking-queue -commitSha: "d21cd0fa" -commitUrl: "https://github.com/lemmy/BlockingQueue/commit/d21cd0fa" +commitSha: "9dfadd9d" +commitUrl: "https://github.com/lemmy/BlockingQueue/commit/9dfadd9d" --- This is the first version of the BlockingQueue specification. It models a bounded buffer shared between producers and consumers. @@ -19,7 +19,7 @@ The spec uses a **wait set** pattern: threads that cannot proceed (producer when ## What to Look For -Run TLC and observe the state graph. With this minimal configuration, you can trace through every possible state by hand. +Run TLC and inspect the output. With this minimal configuration, you can trace through every reachable state by hand using the graph below. The browser does not generate a graph; the image comes from the upstream tutorial. ## State Graph @@ -27,6 +27,10 @@ The model uses the minimal parameters (1 producer, 1 consumer, and a buffer of s ![State graph p1c1b1](/bq-images/p1c1b1.svg) +## Expected Result + +TLC completes without a deadlock and reports 4 distinct states. Try adding a second consumer to see why success for this minimal model does not imply success for every configuration. + ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE BlockingQueue --------------------------- (***************************************************************************) diff --git a/src/content/blocking-queue/03-larger-config.md b/src/content/blocking-queue/03-larger-config.md index 7c2f2e2..fb678b3 100644 --- a/src/content/blocking-queue/03-larger-config.md +++ b/src/content/blocking-queue/03-larger-config.md @@ -3,8 +3,8 @@ slug: larger-config expect: violation title: "Larger Configuration" section: blocking-queue -commitSha: "7d05fdfa" -commitUrl: "https://github.com/lemmy/BlockingQueue/commit/7d05fdfa" +commitSha: "607a169d" +commitUrl: "https://github.com/lemmy/BlockingQueue/commit/607a169d" --- We now use a slightly different configuration (1 producer, 2 consumers, buffer capacity 1) which lets us visually spot the deadlock. @@ -14,7 +14,7 @@ Only the configuration changed - the spec is the same. This demonstrates the pow ## Try It -Run TLC and notice how the state space grows compared to v02. +Run TLC and notice how the state space grows compared to the previous lesson (upstream v02). ## State Graph @@ -22,10 +22,14 @@ Slightly larger configuration with which we can visually spot the deadlock: ![State graph p1c2b1](/bq-images/p1c2b1.svg) -BlockingQueueDebug.tla/.cfg shows how to interactively explore a state graph with TLC in combination with GraphViz: +Upstream also supplies `BlockingQueueDebug.tla/.cfg` for a different configuration, **p2c1b1**. The following recording uses desktop TLC with GraphViz; that interactive graph explorer is not part of the browser playground: ![Explore state graph](/bq-images/v03-StateGraph.gif) +## Expected Result + +TLC reports **Deadlock reached** for the supplied p1c2b1 model. Its built-in deadlock check is enabled by default, even though this version has no explicit invariant. Try swapping the numbers of producers and consumers; the next lesson explores that configuration. + ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE BlockingQueue --------------------------- (***************************************************************************) diff --git a/src/content/blocking-queue/04-debug-config.md b/src/content/blocking-queue/04-debug-config.md index ebaa0da..4d2cf08 100644 --- a/src/content/blocking-queue/04-debug-config.md +++ b/src/content/blocking-queue/04-debug-config.md @@ -3,19 +3,25 @@ slug: debug-config expect: violation title: "Debug State Graph" section: blocking-queue -commitSha: "534f3928" -commitUrl: "https://github.com/lemmy/BlockingQueue/commit/534f3928" +commitSha: "0f777ce3" +commitUrl: "https://github.com/lemmy/BlockingQueue/commit/0f777ce3" --- A debug configuration with 2 producers, 1 consumer, and buffer capacity 1. ## What Changed -Again just a configuration change. Different configurations expose different behaviors. The deadlock might be easier or harder to find depending on the number of producers and consumers. +Upstream v04 adds an interactive debugger using `TLCExt!PickSuccessor` in `BlockingQueueDebug.tla`. Its debug configuration is p2c1b1. The playground uses those same constants with the base `BlockingQueue` spec, without the desktop-only interactive action constraint. -With the help of TLCExt!PickSuccessor we build us a debugger with which we study the state graph interactively. We learn that with configuration p2c1b1 there are two deadlock states: +The upstream debugger lets us explore both deadlock states for p2c1b1: ![PickSuccessor](/bq-images/v04-PickSuccessor.gif) +To reproduce the debugger rather than the browser run, use the linked upstream revision's `BlockingQueueDebug.tla/.cfg` and the [CommunityModules](https://github.com/tlaplus/CommunityModules) library containing `TLCExt`. + +## Expected Result + +The browser reports **Deadlock reached** and stops at the first deadlock. Unlike the recording, it does not prompt you to choose a successor. Try returning to p1c1b1 to see the deadlock disappear. + ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE BlockingQueue --------------------------- (***************************************************************************) @@ -84,8 +90,8 @@ Next == \E t \in RunningThreads: \/ /\ t \in Producers \* SPECIFICATION CONSTANTS BufCapacity = 1 - Producers = {p1} - Consumers = {c1,c2} + Producers = {p1,p2} + Consumers = {c1} INIT Init NEXT Next diff --git a/src/content/blocking-queue/05-safety.md b/src/content/blocking-queue/05-safety.md index ba9cb09..7ac435c 100644 --- a/src/content/blocking-queue/05-safety.md +++ b/src/content/blocking-queue/05-safety.md @@ -3,14 +3,14 @@ slug: safety expect: violation title: "Safety - Detecting Deadlocks" section: blocking-queue -commitSha: "ce99d16a" -commitUrl: "https://github.com/lemmy/BlockingQueue/commit/ce99d16a" +commitSha: "2fa48399" +commitUrl: "https://github.com/lemmy/BlockingQueue/commit/2fa48399" --- -Now we add an **invariant** to automatically detect deadlocks instead of manually inspecting the state graph. +Now we add an **invariant** that explicitly expresses deadlock freedom for this model. TLC already detects deadlocks automatically; the invariant gives us a state predicate to study and, in later upstream steps, prove. ## What Changed -An Invariant definition was added to the spec, and INVARIANT was added to the configuration. +The definitions `Invariant` and `TypeInv` were added to the spec and enabled with `INVARIANT` entries in the configuration. ## The Deadlock Invariant @@ -22,9 +22,18 @@ A **safety property** says "something bad never happens." Invariants are the pri ## TLC Output -TLC now finds the deadlock for configuration p1c2b1: +The supplied configuration is **p4c3b3**, matching the Java application's defaults. It produces a longer counterexample. The upstream tutorial also shows the shorter **p1c2b1** trace below. To reproduce that example, change only the constants to: -\`\`\` +```cfg +CONSTANTS + BufCapacity = 1 + Producers = {p1} + Consumers = {c1,c2} +``` + +Keep `INIT`, `NEXT`, and both `INVARIANT` entries in the configuration. + +```text Error: Invariant Invariant is violated. State 1: /\ buffer = <<>> @@ -57,10 +66,14 @@ State 7: State 8: /\ buffer = <<>> /\ waitSet = {p1, c1, c2} -\`\`\` +``` Note that the Java app with p2c1b1 usually deadlocks only after thousands of log statements, which is considerably longer than the error trace above. This makes it more difficult to understand the root cause. +## Expected Result + +TLC reports that `Invariant` is violated: all producers and consumers are waiting. `TypeInv` still holds, illustrating that well-typed states need not be deadlock-free. Try the smaller configuration above to follow each step of the counterexample. + ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE BlockingQueue --------------------------- EXTENDS Naturals, Sequences, FiniteSets diff --git a/src/content/blocking-queue/06-variables.md b/src/content/blocking-queue/06-variables.md index 82bbb91..72decf4 100644 --- a/src/content/blocking-queue/06-variables.md +++ b/src/content/blocking-queue/06-variables.md @@ -3,20 +3,32 @@ slug: variables expect: violation title: "Constants to Variables" section: blocking-queue -commitSha: "d48bd86a" -commitUrl: "https://github.com/lemmy/BlockingQueue/commit/d48bd86a" +commitSha: "2c9d8870" +commitUrl: "https://github.com/lemmy/BlockingQueue/commit/2c9d8870" --- In this step, we convert some constants into variables to explore a wider range of configurations automatically. ## What Changed -Instead of fixing the buffer capacity as a constant, the spec now allows TLC to explore different values. This lets us check the invariant across many configurations in a single run. +The constants now bound the choices for three new variables: `producers`, `consumers`, and `bufCapacity`. `Init` chooses nonempty subsets of the process sets and a capacity in `1..BufCapacity`. `Next` leaves these variables unchanged, so each behavior uses one fixed configuration rather than changing its configuration while running. ## Key Insight Converting constants to variables is a powerful technique: it lets TLC explore configurations you might not have thought to check manually. -As Michel Charpentier points out, BlockingQueue is deadlock-free under some configurations, but model checking is not helpful with finding the underlying mathematical function. However, we can at least ask TLC to find as many data points as possible. This rewrite increases the complete state space to 57254 distinct states, but TLC continues to find the deadlock behavior. +As Michel Charpentier points out, BlockingQueue is deadlock-free under some configurations. TLC can supply data points from finite models to help us infer a general relationship, but those data points are not a proof for unbounded parameters. + +## Expected Result + +The browser still reports an `Invariant` violation and stops at the first counterexample. There are 315 initial states for the supplied bounds. Try reducing the sets or capacity bound to see how many initial configurations remain. + +The complete state space has **57254 distinct states**, as reported upstream. To explore it past invariant violations, save this lesson's editors as `BlockingQueue.tla` and `BlockingQueue.cfg` alongside a local `tla2tools.jar`, then run: + +```bash +java -jar tla2tools.jar -workers 1 -deadlock -continue BlockingQueue +``` + +`-continue` continues after invariant violations; `-deadlock` disables the separate built-in deadlock check so it does not stop the run. The invariant still reports all-waiting states. These options are not exposed by the browser playground, whose partial state count will be smaller. ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE BlockingQueue --------------------------- diff --git a/src/content/blocking-queue/07-symmetry.md b/src/content/blocking-queue/07-symmetry.md index 72ae3ad..91fd8a1 100644 --- a/src/content/blocking-queue/07-symmetry.md +++ b/src/content/blocking-queue/07-symmetry.md @@ -3,23 +3,35 @@ slug: symmetry expect: violation title: "Symmetry Sets" section: blocking-queue -commitSha: "553287fd" -commitUrl: "https://github.com/lemmy/BlockingQueue/commit/553287fd" +commitSha: "2a624e22" +commitUrl: "https://github.com/lemmy/BlockingQueue/commit/2a624e22" --- We declare Producers and Consumers as **symmetry sets** to dramatically reduce the state space. ## What Changed -The configuration now uses SYMMETRY to tell TLC that individual producer/consumer identities do not matter - only the count matters. +The configuration now uses `SYMMETRY` to tell TLC that consistently renaming producers among themselves, or consumers among themselves, preserves the model and its properties. This does not discard relationships such as whether the same producer appears twice in the buffer. ## Why Symmetry Matters Without symmetry, TLC treats "p1 waiting, p2 running" and "p2 waiting, p1 running" as different states. With symmetry, they are equivalent. This can reduce the state space by orders of magnitude. -TLC can take advantage of symmetry sets to reduce the number of distinct states it has to examine from 57254 to 1647! +TLC reduces the **complete** state space from 57254 to 1647 distinct states. These are the upstream totals for exploration with `-deadlock -continue`, not the partial counts shown by the browser before it stops at the first violation. An expression is symmetric for a set S if and only if interchanging any two values of S does not change the value of the expression. You should declare a set S of model values to be a symmetry set only if the specification and all properties you are checking are symmetric for S. Note that symmetry sets should not be used when checking liveness properties. +TLC does not verify that your symmetry declaration is sound. An incorrect declaration can hide errors. + +## Expected Result + +The browser still reports an `Invariant` violation, but explores fewer distinct states than the previous lesson. Try removing `SYMMETRY Sym` to compare the runs. + +To reproduce the full 1647-state total, save this lesson's spec and configuration locally as `BlockingQueue.tla/.cfg`, place `tla2tools.jar` alongside them, and run: + +```bash +java -jar tla2tools.jar -workers 1 -deadlock -continue BlockingQueue +``` + ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE BlockingQueue --------------------------- EXTENDS Naturals, Sequences, FiniteSets, TLC diff --git a/src/content/blocking-queue/08-inequation.md b/src/content/blocking-queue/08-inequation.md index 3201bf4..18b1e3e 100644 --- a/src/content/blocking-queue/08-inequation.md +++ b/src/content/blocking-queue/08-inequation.md @@ -3,8 +3,8 @@ slug: inequation expect: violation title: "Deadlock-Free Inequation" section: blocking-queue -commitSha: "8e536cba" -commitUrl: "https://github.com/lemmy/BlockingQueue/commit/8e536cba" +commitSha: "80b23f9e" +commitUrl: "https://github.com/lemmy/BlockingQueue/commit/80b23f9e" --- Now we infer the **inequation** under which the system is deadlock-free. @@ -14,9 +14,25 @@ The spec and config are extended to systematically check when the deadlock invar ## Key Insight -TLC finds that the system is deadlock-free when BufCapacity >= (Producers + Consumers - 1). This is a precise characterization discovered through model checking. +The relationship stated in the upstream tutorial is that the original single-wait-set algorithm is deadlock-free if and only if: -We run TLC with the \`-continue\` option to not stop state space exploration after a violation has been found, asking TLC to find all violations. A bit of analysis reveals that BlockingQueue is deadlock-free iff \`2*BufCapacity >= Cardinality(Producers \\union Consumers)\`. +```tla +2 * BufCapacity >= Cardinality(Producers \cup Consumers) +``` + +For example, two producers and two consumers need capacity at least two. In this lesson's multi-configuration model, apply the relationship to the chosen variables `bufCapacity`, `producers`, and `consumers`, not just to their upper-bound constants. + +We infer this relationship from finite data points. Model checking these bounds is not, by itself, a mathematical proof for all process counts and capacities. + +## Collecting the Data Locally + +Save this lesson's spec and configuration as `BlockingQueue.tla/.cfg` alongside `tla2tools.jar`, then use the upstream workflow: + +```bash +java -jar tla2tools.jar -workers 1 -deadlock -continue BlockingQueue | grep InvVio | sort | uniq +``` + +`-continue` keeps exploring after invariant violations. `-deadlock` disables the separate built-in deadlock check; our invariant still identifies the all-waiting states. Each `InvVio` record contains the chosen capacity and total thread count. ![ContinueInequation](/bq-images/ContinueInequation.svg) @@ -24,6 +40,10 @@ Collecting even more data, we can correlate the length of the error trace with t ![TraceLengthCorrelation](/bq-images/TraceLengthCorrelation.svg) +## Expected Result + +The browser reports the first `Invariant` violation and prints an `InvVio` record. It does not expose `-continue`, so it will not collect all the data shown in the upstream plots. Try the local command to collect all violating configurations within the supplied bounds. + ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE BlockingQueue --------------------------- EXTENDS Naturals, Sequences, FiniteSets, TLC diff --git a/src/content/blocking-queue/09-view.md b/src/content/blocking-queue/09-view.md index 84639c2..53390a5 100644 --- a/src/content/blocking-queue/09-view.md +++ b/src/content/blocking-queue/09-view.md @@ -3,8 +3,8 @@ slug: view expect: violation title: "View Abstraction" section: blocking-queue -commitSha: "02119f46" -commitUrl: "https://github.com/lemmy/BlockingQueue/commit/02119f46" +commitSha: "e4911b6d" +commitUrl: "https://github.com/lemmy/BlockingQueue/commit/e4911b6d" --- Define a **view** that abstracts the buffer into a counter, reducing the state space. @@ -16,7 +16,21 @@ A VIEW directive is added to the configuration. The view maps each state to an a The buffer content does not matter for deadlock checking - only its length does. By abstracting the buffer to its length, we dramatically reduce the state space while preserving the properties we care about. -We exploit the insight that the order of elements in the (fifo) buffer is irrelevant for the correctness of the algorithm. In other words, we can abstract the buffer into a simple counter of elements. With this abstraction, the state-space for the current config shrinks from 2940 to 1797 distinct states. +The order and identity of elements in the FIFO buffer are irrelevant to this **deadlock-freedom** question. They would matter for a property about which item is returned, such as FIFO ordering. A view is not automatically safe for every property. + +With this abstraction, the **complete** state space for the current configuration shrinks from 2940 to 1797 distinct states, as reported upstream. + +## Expected Result + +The browser still reports an `Invariant` violation and stops at the first counterexample. Try removing `VIEW View` to compare the partial exploration counts. + +To reproduce the complete totals, save this lesson's spec and configuration as `BlockingQueue.tla/.cfg` alongside `tla2tools.jar`, then run: + +```bash +java -jar tla2tools.jar -workers 1 -deadlock -continue BlockingQueue +``` + +This continues after invariant violations and disables the separate built-in deadlock stopping condition. Compare runs with and without `VIEW View`; leave `SYMMETRY Sym` enabled in both. ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE BlockingQueue --------------------------- diff --git a/src/content/blocking-queue/10-notify-nondeterministic.md b/src/content/blocking-queue/10-notify-nondeterministic.md index 641daea..5da4025 100644 --- a/src/content/blocking-queue/10-notify-nondeterministic.md +++ b/src/content/blocking-queue/10-notify-nondeterministic.md @@ -1,25 +1,28 @@ --- slug: notify-nondeterministic +expect: violation title: "Non-deterministic Notification" section: blocking-queue -commitSha: "ea2a2303" -commitUrl: "https://github.com/lemmy/BlockingQueue/commit/ea2a2303" +commitSha: "be91c6d6" +commitUrl: "https://github.com/lemmy/BlockingQueue/commit/be91c6d6" --- -A critical bugfix: the notification mechanism now non-deterministically selects which waiting thread to wake up. +Upstream v11 tries an additional, non-deterministically scheduled notification as a workaround for the blocking-queue bug. It is an attempted fix, not the final solution. ## What Changed -Previously, the spec assumed a specific thread would be notified. Now it models the real behavior of notify() in Java: any one of the waiting threads can be selected. +`Notify` already used `\E x \in waitSet` to choose any waiting thread. The new choice is in `Next`: notification can now happen as a separate step, without a producer adding an item or a consumer removing one. -## The Bug +## Why This Is Not the Final Fix -If we always notify a specific thread, we miss executions where a different thread gets notified - which could lead to deadlock. +As the upstream tutorial explains, we can keep waking the wrong kind of thread, which cannot perform useful work and goes back to waiting. Adding a possible wakeup does not guarantee progress. -## Key Concept +There is an important distinction in this version: `Invariant` still forbids all threads being in `waitSet`, but that state is no longer a TLC deadlock. The independent `Notify` step remains enabled and can wake someone. Even when `waitSet` is empty, that step permits an unchanged state. -When modeling a system, you must capture **all** possible behaviors, not just the ones you expect. Non-determinism is how TLA+ models situations where the system can make any of several choices. +The supplied invariant checks a state condition, not eventual progress. A liveness claim would require a temporal property and appropriate fairness assumptions; upstream explores these in later lessons. -Non-deterministically notify waiting threads in an attempt to fix the deadlock situation. This attempt fails because we might end up waking the wrong thread up over and over again. +## Expected Result + +TLC reports an `Invariant` violation because all threads can still be waiting. Try removing only `INVARIANT Invariant` from the configuration: TLC completes without a built-in deadlock error, but that does not establish that useful work must continue. ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE BlockingQueue --------------------------- @@ -75,7 +78,7 @@ Init == /\ buffer = <<>> (* Then, pick a thread out of all running threads and have it do its thing. *) Next == - \/ Notify /\ UNCHANGED buffer \* At each step notify all waiting threads. + \/ Notify /\ UNCHANGED buffer \/ \E t \in RunningThreads: \/ /\ t \in Producers /\ Put(t, t) \* Add some data to buffer \/ /\ t \in Consumers @@ -88,7 +91,7 @@ TypeInv == /\ buffer \in Seq(Producers) /\ Len(buffer) \in 0..BufCapacity /\ waitSet \subseteq (Producers \cup Consumers) -(* No Deadlock *) +(* The original all-waiting invariant, not a deadlock test with this Next. *) Invariant == waitSet # (Producers \cup Consumers) ============================================================================= diff --git a/src/content/blocking-queue/11-notify-all.md b/src/content/blocking-queue/11-notify-all.md index 8fbccce..49e31be 100644 --- a/src/content/blocking-queue/11-notify-all.md +++ b/src/content/blocking-queue/11-notify-all.md @@ -1,27 +1,32 @@ --- slug: notify-all +expect: success title: "Notify All" section: blocking-queue -commitSha: "a81e4914" -commitUrl: "https://github.com/lemmy/BlockingQueue/commit/a81e4914" +commitSha: "8ab5eb37" +commitUrl: "https://github.com/lemmy/BlockingQueue/commit/8ab5eb37" --- -Another bugfix: switch from notify() to notifyAll() - always wake up all waiting threads. +Upstream v12 replaces `notify()` with `notifyAll()` on successful queue operations. ## What Changed -Instead of non-deterministically notifying one thread, we now notify **all** waiting threads. This is the standard fix for the lost-wakeup problem. +Instead of notifying one thread, successful `Put` and `Get` operations notify **all** waiting threads. The independent notification step from the previous attempted fix is removed. -## The Lost Wakeup Problem +## Waking the Wrong Kind of Thread With notify(), the JVM might wake up a thread that cannot make progress (e.g., waking a producer when the buffer is already full). That thread goes back to waiting, and the actual thread that could make progress is never woken - leading to deadlock. ## The Fix -notifyAll() ensures every waiting thread gets a chance to check whether it can proceed. +`notifyAll()` makes all waiters eligible to reacquire the shared lock and recheck their conditions. This fixes the modeled deadlock, but waking threads that cannot proceed can add contention. It does not by itself guarantee fair scheduling or freedom from starvation. As a bonus exercise, check if it is necessary to notify all waiting threads in both Put and Get. -Note that this is the proposed solution to the bug in Challenge 14 of the c2 extreme programming wiki. To the best of my knowledge, not a single comment mentions that just one notifyAll suffices. Neither does anybody mention a more elegant fix that has no performance implications (see next step). +The upstream tutorial notes that using `notifyAll()` in just one of the two operations suffices for this deadlock fix. Try keeping `NotifyAll` in one operation and restoring the earlier single-thread `Notify` in the other. The next lesson avoids waking the wrong kind of thread in the first place. + +## Expected Result + +TLC completes without a deadlock or invariant violation for the supplied p4c3b3 model. This is a finite-model result, not a proof for every configuration or a liveness guarantee. ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE BlockingQueue --------------------------- diff --git a/src/content/blocking-queue/12-two-mutexes.md b/src/content/blocking-queue/12-two-mutexes.md index f39035a..ad798f9 100644 --- a/src/content/blocking-queue/12-two-mutexes.md +++ b/src/content/blocking-queue/12-two-mutexes.md @@ -1,31 +1,36 @@ --- slug: two-mutexes -title: "Two Mutexes" +expect: success +title: "(Logically) Two Mutexes" section: blocking-queue -commitSha: "a400b585" -commitUrl: "https://github.com/lemmy/BlockingQueue/commit/a400b585" +commitSha: "fe230e23" +commitUrl: "https://github.com/lemmy/BlockingQueue/commit/fe230e23" --- -The final bugfix: using (logically) two separate mutexes for producers and consumers. +Upstream v13 calls this fix **"(Logically) two mutexes"**: separate the waiting producers from the waiting consumers so each operation notifies the other kind of thread. ## What Changed -Instead of a single wait set for all threads, we separate waiting producers from waiting consumers. +The abstract spec keeps one `waitSet`. `NotifyOther(Consumers)` selects a waiting consumer after a put, and `NotifyOther(Producers)` selects a waiting producer after a get. There is no need to represent two separate wait sets at this level. ## Why This Matters -With a single mutex/condition variable, notifyAll() wakes up ALL threads - including those that definitely cannot proceed. With separate conditions for "buffer not full" and "buffer not empty," we can be more precise. +With a single condition, `notifyAll()` wakes up all waiters, including those that cannot proceed. Separate conditions for "buffer not full" and "buffer not empty" let us signal only the relevant group. + +The upstream title describes the logical separation of waiters, not a recommendation to protect shared buffer updates with unrelated locks. Its later Java implementation uses **one `ReentrantLock` and two `Condition` objects**; its C implementation likewise uses one mutex and two condition variables. Both producers and consumers must still synchronize access to the shared buffer. ## Summary of the Bugfix Journey -1. **v11**: Model the real non-deterministic behavior of notify() -2. **v12**: Fix with notifyAll() - correct but inefficient -3. **v13**: Optimize with separate condition variables - correct AND efficient +1. **v11**: Try independently scheduled notifications; the all-waiting invariant still fails. +2. **v12**: Fix the modeled deadlock with `notifyAll()`, at the cost of unnecessary wakeups. +3. **v13**: Notify only the opposite kind of waiter, avoiding those unnecessary wakeups. This is exactly the kind of bug that TLA+ excels at finding: subtle concurrency issues that only manifest in specific interleavings. -Remove notifyAll and instead introduce two mutexes (one for Producers and one for Consumers). A Consumer will notify the subset of Producers waiting on the Producer mutex (vice versa for a Producer). +## Expected Result + +TLC completes without a deadlock or invariant violation for the supplied model. Try different positive capacities and nonempty producer/consumer sets. -The spec does not have to introduce two mutexes. Instead, we can just pick the right thread type from the set of waiting threads. This fix completely solves the bug, but are we fully satisfied yet? +Are we fully satisfied? As upstream v14 points out, finite runs alone cannot prove the fix for arbitrary parameters. The upstream tutorial continues with TLAPS proofs and, later, starvation and fairness. Those topics are beyond this shortened walkthrough. ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE BlockingQueue --------------------------- diff --git a/src/content/intro/basic-operators.md b/src/content/intro/basic-operators.md index 3579b1e..09f9eb9 100644 --- a/src/content/intro/basic-operators.md +++ b/src/content/intro/basic-operators.md @@ -22,7 +22,7 @@ TLA+ supports both the ASCII version as well as its Unicode equivalent. Almost every TLA+ spec follows this pattern: -1. **Init** - defines the initial state (conjunction of assignments) +1. **Init** - a predicate defining the allowed initial states 2. **Next** - defines all possible transitions (disjunction of actions) ``` @@ -36,6 +36,8 @@ Next == \/ ActionA In Init, `/\` means "and" - all conditions must hold. In Next, `\/` means "or" - any one action can happen. +These are mathematical predicates, not sequences of assignments. `=` means equality, and all conjuncts hold simultaneously. `==` defines an operator. An initial predicate can allow several states, for example `Init == x \in {0, 1}`. + ## Actions and Primed Variables An **action** describes one kind of state transition. It uses primed variables (`x'`) to refer to the value in the next state: @@ -56,6 +58,18 @@ Increment == /\ x' = x + 1 For multiple variables: `UNCHANGED <>` +## Quantifiers and Non-deterministic Choice + +`\E x \in S : P(x)` means that **there exists** an `x` in `S` for which `P(x)` holds. In a next-state relation, it can describe several possible successors: + +```tla +Next == \E n \in 1..3 : x' = n +``` + +TLC explores all three choices; this is not a random assignment. + +`\A x \in S : P(x)` means that **for every** `x` in `S`, `P(x)` holds. For example, `\A n \in {1, 2, 3} : n > 0` is true. `\in` means set membership; the Sets lesson covers it in more detail. + ## IF / THEN / ELSE ``` @@ -66,6 +80,16 @@ Max(a, b) == IF a > b THEN a ELSE b The spec demonstrates a simple traffic light with Init/Next pattern and boolean operators. +`TypeOK` is a **state predicate**: it mentions only the current state. `(light = "green") => (light' # "red")` is an **action predicate**: it relates two consecutive states. + +`[A]_light` allows action `A` or a step leaving `light` unchanged (stuttering). Prefixing this with `[]` means "always", giving the temporal safety property `NeverSkipYellow`. TLA+ requires this stuttering form when applying `[]` to an action. The configuration enables the property with `PROPERTY`, not `INVARIANT`. + +## Expected Result + +TLC completes without errors: the light cycles red, green, yellow, red. Both `TypeOK` and `NeverSkipYellow` are enabled. + +Try changing the guard of `ToRed` to `light \in {"yellow", "green"}`. The values remain well-typed, but TLC reports an action-property violation because a green-to-red transition skips yellow. + ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE TrafficLight ----------------------------- EXTENDS Naturals @@ -90,7 +114,7 @@ Next == \/ ToGreen \/ ToYellow \/ ToRed -NeverSkipYellow == (light = "green") => (light' # "red") +NeverSkipYellow == [][(light = "green") => (light' # "red")]_light ============================================================================= @@ -98,3 +122,4 @@ NeverSkipYellow == (light = "green") => (light' # "red") INIT Init NEXT Next INVARIANT TypeOK +PROPERTY NeverSkipYellow diff --git a/src/content/intro/functions.md b/src/content/intro/functions.md index 2a7d052..2a59a67 100644 --- a/src/content/intro/functions.md +++ b/src/content/intro/functions.md @@ -58,6 +58,12 @@ f' = [f EXCEPT ![2] = @ + 1] The spec models a simple key-value store using TLA+ functions. +## Expected Result + +TLC reports that `AllBounded` is violated when a key's value reaches 12. `Put` is bounded, but `Increment` is not; `TypeOK` still holds because 12 is a natural number. + +Try adding `store[k] < 11` as a guard in `Increment`. The resulting finite model should complete without violating either invariant. + ---TLA_BY_EXAMPLE_SPEC--- ---------------------------- MODULE KeyValue --------------------------------- EXTENDS Naturals diff --git a/src/content/intro/module-structure.md b/src/content/intro/module-structure.md index 85fcee9..9ca75dc 100644 --- a/src/content/intro/module-structure.md +++ b/src/content/intro/module-structure.md @@ -39,7 +39,7 @@ Everything after the footer is ignored by TLA+ tools. By convention, this space ``` ======================== Modification History -* Added Bound invariant to limit state space +* Added Bound invariant to detect reaching the limit * Initial version with basic counter ``` @@ -83,8 +83,14 @@ To use these operators, add `EXTENDS TLC` to your module. The spec on the right shows a module with text before the header and after the footer. It also uses `PrintT` to print the value of `x` on each step. Notice how the module name matches the tab filename. Try modifying it and running TLC to see what happens. +`Spec == Init /\ [][Next]_x` is the conventional temporal form: start in `Init`, then always (`[]`) take a `Next` step or leave `x` unchanged. Such an unchanged step is called **stuttering**. This lesson's configuration uses `INIT Init` and `NEXT Next` directly; `SPECIFICATION Spec` is an alternative. + +## Expected Result + +TLC reports that `Bound` is violated when `x = 5`. The invariant detects that state; it does not prevent the counter from reaching it. Try changing the limit in `Bound` and following the new trace. Removing `Bound` entirely leaves an unbounded exploration, not a finite successful run. + ---TLA_BY_EXAMPLE_SPEC--- -A simple counter that increments from 0 up to a bound. +A counter that increments until TLC reports an invariant violation. Demonstrates the basic structure of a TLA+ module. ----------------------------- MODULE MySpec ---------------------------------- (***************************************************************************) @@ -107,7 +113,7 @@ Bound == x < 5 ============================================================================= Modification History -* Initial version with a simple bounded counter +* Initial version with a counter and a bound invariant ---TLA_BY_EXAMPLE_CFG--- INIT Init diff --git a/src/content/intro/platform.md b/src/content/intro/platform.md index 056ab5c..04a7a4f 100644 --- a/src/content/intro/platform.md +++ b/src/content/intro/platform.md @@ -10,8 +10,10 @@ Welcome to TLA+ By Example! This platform lets you learn TLA+ by reading explana On the right side of this page, you'll see the **playground**. It has two tabs: -- **Spec.tla** - the TLA+ specification you're writing -- **Spec.cfg** - the TLC model checker configuration +- **DieHard.tla** - the TLA+ specification you're writing +- **DieHard.cfg** - the TLC model checker configuration + +Tab filenames follow the module name, so they differ between lessons. Click **▶ Run TLC** to model-check the specification. The output will appear in the panel at the bottom of the playground. @@ -27,11 +29,11 @@ A TLA+ specification describes: ## What is TLC? -TLC is the **model checker** for TLA+. When you click **▶ Run TLC**, it systematically explores **every reachable state** of your specification by starting from the initial state and following all possible transitions. +TLC is a **model checker** for TLA+. When you click **▶ Run TLC**, it starts from all states satisfying the initial predicate and systematically explores the reachable state graph of the configured model. -At each state, TLC checks your **invariants** - properties you've declared must always be true. If TLC finds a state that violates an invariant, it stops and shows you the exact sequence of steps that led to the violation. If no violations are found, TLC reports that all states satisfy the invariants. +At each state, TLC checks the **invariants enabled in the configuration**. If one is false, TLC stops and shows the sequence of steps that led to the violation. If exploration of the finite model completes without errors, all its reachable states satisfy those invariants. -This exhaustive approach means TLC doesn't test random scenarios - it checks **all of them**. That's what makes formal verification more powerful than traditional testing. +Unlike testing a selection of executions, this checks the entire reachable graph of that finite model. A graph with cycles can represent infinitely many behaviors; TLC does not enumerate every possible path separately. The result applies to the chosen constants, assumptions, and properties, not automatically to arbitrary system sizes or to an implementation. Unbounded models may never finish. ## Try It Now @@ -41,9 +43,13 @@ The playground on the right has a classic example: the **DieHard** water jugs pu Click **▶ Run TLC** to see TLC find a solution (it will report an invariant violation - which is actually the solution!). +## Expected Result + +TLC reports that `NotSolved` is violated and shows a trace ending with `big = 4`. Try removing only `INVARIANT NotSolved` from the configuration: TLC will instead complete its exploration while checking `TypeOK`. + ## Understanding the TLC Output -TLC runs entirely **in your browser** using WebAssembly - nothing is sent to a server. After clicking Run TLC, you'll see output like the following. Here's how to read it: +TLC runs **in your browser** via CheerpJ's Java runtime; your spec and configuration are not submitted to a model-checking server. The runtime itself is downloaded from a CDN. After clicking Run TLC, you'll see output like the following. Version details and source locations may differ: ### Header @@ -53,7 +59,7 @@ Running breadth-first search Model-Checking with fp 62 and seed ... with 1 worker on 1 cores with 2048MB heap ``` -This tells you the TLC version and that it's using **breadth-first search** - it explores all states at depth 1, then depth 2, and so on. This means when TLC finds a violation, the error trace is always the **shortest possible path** to the error. +This tells you the TLC version and that it's using **breadth-first search** - it explores states layer by layer. For this invariant check with one worker, the counterexample is a **shortest path** to a violation. This guarantee does not extend to every TLC mode or to arbitrary temporal-property counterexamples. ### Parsing and Semantic Processing @@ -113,7 +119,7 @@ Reading this trace, you can follow the solution step by step: fill the big jug, TLC finished with exit code: 2110 ``` -Exit code `2110` means TLC found an invariant violation. An exit code of `0` means all states were checked and no violations were found. +The browser wrapper labels TLC's internal result code as an "exit code": `2110` identifies an invariant violation. This is not the operating-system exit status of command-line TLC, which uses `12` for a safety violation. For this finite model, a result of `0` means exploration completed without an error. ## Follow Along Locally diff --git a/src/content/intro/records.md b/src/content/intro/records.md index c1e9893..ac50dd6 100644 --- a/src/content/intro/records.md +++ b/src/content/intro/records.md @@ -1,5 +1,6 @@ --- slug: records +expect: success title: Records section: intro --- @@ -54,23 +55,30 @@ is the same as: ## Try It -The spec models a simple user account system with records. +The spec models user accounts with a small maximum balance so the reachable state space is finite. `Deposit` checks the limit before changing a balance; a type invariant alone would only detect an out-of-range balance, not prevent it. + +When every account is inactive, `Finished` permits an unchanged terminal state. This deliberate stuttering step models a completed system rather than an unexpected deadlock. + +## Expected Result + +TLC completes without errors for two users and `MaxBalance = 3`. Try removing the upper-bound guard from `Deposit`; `TypeOK` then fails when a balance exceeds `MaxBalance`. ---TLA_BY_EXAMPLE_SPEC--- ----------------------------- MODULE Records --------------------------------- EXTENDS Naturals -CONSTANT Users +CONSTANTS Users, MaxBalance VARIABLE accounts -TypeOK == accounts \in [Users -> [balance: Nat, active: BOOLEAN]] +TypeOK == accounts \in [Users -> [balance: 0..MaxBalance, active: BOOLEAN]] -Init == accounts = [u \in Users |-> [balance |-> 100, active |-> TRUE]] +Init == accounts = [u \in Users |-> [balance |-> MaxBalance, active |-> TRUE]] Deposit(u, amt) == /\ accounts[u].active - /\ amt \in 1..50 + /\ amt \in 1..MaxBalance + /\ accounts[u].balance + amt <= MaxBalance /\ accounts' = [accounts EXCEPT ![u].balance = @ + amt] Withdraw(u, amt) == @@ -82,10 +90,14 @@ Deactivate(u) == /\ accounts[u].active /\ accounts' = [accounts EXCEPT ![u].active = FALSE] -Next == \E u \in Users : - \/ \E amt \in 1..50 : Deposit(u, amt) - \/ \E amt \in 1..50 : Withdraw(u, amt) - \/ Deactivate(u) +Finished == /\ \A u \in Users : ~accounts[u].active + /\ UNCHANGED accounts + +Next == \/ \E u \in Users : + \/ \E amt \in 1..MaxBalance : Deposit(u, amt) + \/ \E amt \in 1..MaxBalance : Withdraw(u, amt) + \/ Deactivate(u) + \/ Finished NoNegativeBalances == \A u \in Users : accounts[u].balance >= 0 @@ -93,6 +105,7 @@ NoNegativeBalances == \A u \in Users : accounts[u].balance >= 0 ---TLA_BY_EXAMPLE_CFG--- CONSTANT Users = {alice, bob} +CONSTANT MaxBalance = 3 INIT Init NEXT Next INVARIANT TypeOK diff --git a/src/content/intro/sequences.md b/src/content/intro/sequences.md index ea19a30..e96a3ad 100644 --- a/src/content/intro/sequences.md +++ b/src/content/intro/sequences.md @@ -57,6 +57,10 @@ Front(s) == Head(s) The spec on the right models a simple bounded stack. +## Expected Result + +TLC completes without errors. `Push` is enabled only below `MaxSize`, and `Pop` only for a nonempty stack. Try removing the size guard from `Push`; TLC will report a violated invariant when the stack exceeds `MaxSize`. + ---TLA_BY_EXAMPLE_SPEC--- ------------------------------ MODULE Stack ---------------------------------- EXTENDS Naturals, Sequences diff --git a/src/content/intro/sets.md b/src/content/intro/sets.md index 0cc59fb..4640014 100644 --- a/src/content/intro/sets.md +++ b/src/content/intro/sets.md @@ -65,6 +65,10 @@ Example: `{x * 2 : x \in 1..3}` gives `{2, 4, 6}` The spec on the right demonstrates various set operations. Run TLC to verify the invariants. +## Expected Result + +TLC completes without errors and finds 8 distinct states: all subsets of the three colors. Try adding a fourth color to `Colors`; the model then has 16 distinct states. + ---TLA_BY_EXAMPLE_SPEC--- ------------------------------- MODULE Sets ---------------------------------- EXTENDS Naturals, FiniteSets diff --git a/src/content/intro/tlc-config.md b/src/content/intro/tlc-config.md index a22047b..26eab5e 100644 --- a/src/content/intro/tlc-config.md +++ b/src/content/intro/tlc-config.md @@ -23,10 +23,9 @@ Properties that must hold in **every** reachable state: ``` INVARIANT TypeOK -INVARIANT NoDeadlock ``` -If TLC finds a state where an invariant is FALSE, it reports an error with a trace showing how it got there. +`TypeOK` must be defined in the spec. Defining it does not enable the check by itself. If TLC finds a state where an enabled invariant is FALSE, it reports an error with a trace showing how it got there. ## CONSTANT @@ -39,12 +38,20 @@ CONSTANT Procs = {p1, p2, p3} ## PROPERTY (Temporal Properties) -For liveness checks (things that must **eventually** happen): +`PROPERTY` enables a temporal formula defined in the spec. These can express safety as well as liveness. For example, define: +```tla +AlwaysNonnegative == [](counter >= 0) ``` -PROPERTY Liveness + +Then enable it in the configuration: + +```cfg +PROPERTY AlwaysNonnegative ``` +`[]` means "always", so this is a safety property. `<>` means "eventually" and is used for liveness properties. Eventual progress often requires explicit fairness assumptions; `INIT` and `NEXT` alone do not guarantee it. The Basic Operators lesson also uses `PROPERTY` for a condition on every transition. + ## SYMMETRY When constants represent interchangeable processes, symmetry reduces the state space: @@ -54,7 +61,9 @@ CONSTANT Procs = {p1, p2, p3} SYMMETRY Perms ``` -Where `Perms` is defined as `Permutations(Procs)` in your spec. +Here `Procs` must be declared as a constant, and `Perms == Permutations(Procs)` must be defined in the spec. `Permutations` comes from the `TLC` module, so add `TLC` to `EXTENDS`. + +Only use symmetry when the specification and checked properties are invariant under renaming those process identities. TLC does not verify that assumption, and symmetry should not be used for liveness checking. ## CHECK_DEADLOCK @@ -64,10 +73,16 @@ By default, TLC checks for deadlocks (states with no successor). You can disable CHECK_DEADLOCK FALSE ``` +This is a built-in check, not an invariant named `NoDeadlock`. Disable it only when terminal states are intentional; it does not make an infinite model finite. + ## Try It Try editing the configuration on the right. Change the constant `Size` to different values and see how the state space changes. +## Expected Result + +With `Size = 5`, TLC completes without errors and finds 6 distinct states (`counter` from 0 to 5). Try `Size = 0`: the initial state is well-typed, but neither `Inc` nor `Dec` is enabled, so TLC reports a deadlock. + ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE ConfigDemo -------------------------------- EXTENDS Naturals diff --git a/src/content/intro/variables-constants.md b/src/content/intro/variables-constants.md index 0bd552a..73ff3f4 100644 --- a/src/content/intro/variables-constants.md +++ b/src/content/intro/variables-constants.md @@ -43,11 +43,17 @@ TypeOK == /\ x \in Nat /\ y \in 1..N ``` -Since TLA+ has no types, `TypeOK` is just a formula like any other. TLC checks it as an invariant at every reachable state, making it a useful way to catch bugs early. +Since TLA+ has no types, `TypeOK` is just a formula like any other. When enabled with `INVARIANT TypeOK` in the configuration, TLC checks it at every reachable state. Merely defining an operator named `TypeOK` does not enable a check. ## Try It -The spec on the right uses both variables and constants. Check the `Spec.cfg` tab to see how the constant `N` is assigned a value. +The spec on the right uses both variables and constants. Check the `VarsAndConsts.cfg` tab to see how the constant `N` is assigned a value. + +## Expected Result + +With `N = 3`, TLC reports **Deadlock reached** at `count = 2, total = 5`. `Increment` requires `total < 5`, while `Reset` requires `count = N`, so neither is enabled. `TypeOK` still holds: type correctness does not imply that the system can keep making progress. + +Try changing `Reset` so it also sets `total' = 0`. The counters can then cycle without reaching this deadlock. ---TLA_BY_EXAMPLE_SPEC--- --------------------------- MODULE VarsAndConsts ----------------------------