TLA+ By Example

Learn TLA+ specifications through interactive examples. Write specs and run the TLC model checker directly in your browser.

How to Write TLA+

A step-by-step introduction to TLA+ syntax, data structures, and model checking.

1

Welcome

2

Module Structure

3

Variables & Constants

4

Basic Operators

5

Sets

6

Functions

7

Sequences

8

Records

9

TLC Configuration

BlockingQueue Tutorial

A guided walkthrough of a real-world TLA+ specification: modeling a bounded blocking queue with producers and consumers.

Based on lemmy/BlockingQueue by Markus Kuppe.

1

Introduction

2

State Graph (Minimum Config)

3

Larger Configuration

4

Debug State Graph

5

Safety — Detecting Deadlocks

6

Constants to Variables

7

Symmetry Sets

8

Deadlock-Free Inequation

9

View Abstraction

10

Non-deterministic Notification

11

Notify All

12

Two Mutexes