TLA+ Debugger: Interactive State-Space Exploration

[Markus Alexander Kuppe]

Hi everyone,

The TLA+ Debugger has a new major capability: **interactive state-space exploration**. Previously, the debugger let you inspect states along a single execution trace; now you can actively choose how the state space is explored, navigating freely through your specification's state machine one state at a time.

This represents a shift in how you can work with TLA+ specifications, enabling new workflows for understanding and validating your models.

## What is Interactive State-Space Exploration?

Interactive state-space exploration allows you to:

- **Interactively select the initial state** from the set of all initial states satisfying your `Init` predicate

- **Choose successor states** by selecting from the set of all valid next states computed by your `Next` action

- **Step backward** through the trace to any predecessor state, including all the way back to the set of initial states

- **Navigate freely** through your specification's state machine using step-in, step-over, and step-back operations

This approach emphasizes the **state-machine perspective of TLA+**, making it natural to think about your specification as a state transition system rather than just formulas and temporal properties.

## Combining with TLA+ Animations

When combined with TLA+ animations, interactive state-space exploration truly shines. The textual TLA+ specification is conceptually lifted into the application domain of the system being modeled. Instead of examining raw variable assignments, you can see animated visualizations of your protocol's behavior as you navigate through the state space.

Connecting animations to the debugger is **trivial with Watch expressions**—simply add a watch for your animation module's `AnimView` operator, and the debugger will display the SVG visualization for each state as you navigate through the state space.

The first screencast (linked below) demonstrates how to combine the TLA+ Debugger, interactive state-space exploration, Watch expressions, and animations into what becomes effectively a **Graphical Debugger** for your system or protocol. Notably, the animation module shown in the screencast was generated by AI, following the [TLA+ animation guide](https://github.com/tlaplus/vscode-tlaplus/blob/master/resources/knowledgebase/tla-animations.md) shipped as part of the new TLA+ MCP server—demonstrating how accessible this workflow can be.

## Enhanced Breakpoint Support

The new "Halt (break) after Init and Next" breakpoint that enables interactive state-space exploration supports **breakpoint conditions**, which opens up advanced debugging workflows:

- For specs that terminate or deadlock, the breakpoint condition `~ENABLED Next` will halt simulation at the terminal state

- Breakpoint conditions are evaluated both after `Init` (for the set of initial states) and after `Next` (for successor states)

- The debugger halts even when `Next` evaluates to `FALSE` (i.e., when no successor states exist), allowing you to catch deadlocks

## Loading External Modules

Breakpoint conditions, Watch expressions, and the Debug Console now support **loading any TLA+ module on the TLA-Library path**, even if those modules are not extended by the spec being debugged. This enables new capabilities, such as:

**Exporting trace prefixes** in various formats (JSON, TLA+, binary, etc.) dynamically during a debugging session. For example, you can evaluate this Watch expression:

```tla

LET J == INSTANCE _JsonTrace

WITH _JsonTraceFile <- "output.json"

IN J!_JsonTrace

```

This exports the current trace to JSON without needing to preconfigure the debugger or manually trigger violations. Several [other export formats](https://github.com/tlaplus/tlaplus/tree/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules) are supported via modules, but you can also create your own custom export modules:

- `_TLCTracePlain` - Exports the trace as a TLA+ module with a `Trace` constant (text format)

- `_TLCTrace` - Exports the trace in TLC's binary format (designed for very long traces)

- `_TLCTESpec` - Generates a trace expression specification that can replay the trace as a valid behavior

- `_TLCActionTrace` - Exports the sequence of actions with their parameters/arguments for minimization workflows

- `_TLAPlusCounterExample` - Exports the full `TLCExt!CounterExample` record as a TLA+ module

- `_DotTrace` - Exports the trace in DOT/GraphViz format for visualization

This functionality is showcased in the third screencast.

This export capability is a first step towards the goal outlined in [GitHub issue #860](https://github.com/tlaplus/tlaplus/issues/860#issuecomment-2836117684): create interesting traces interactively in the debugger, export them, and then have TLC verify repeatedly that these traces remain valid behaviors of the original specification as you update it. This bridges the gap between exploratory debugging and formal verification.

## Background

The TLA+ Debugger was first released in 2022 (see [publication](https://dl.acm.org/doi/10.1007/978-3-031-26236-4_15)) and is built on the [Debug Adapter Protocol](https://microsoft.github.io/debug-adapter-protocol/) (DAP), which provides a standardized interface between development tools and debuggers. The debugger is available for VSCode and Cursor, but will work in any IDE that supports DAP.

## Credit Where Credit is Due

Interactive state-space exploration was pioneered by Will Schultz in Spectacle (https://github.com/will62794/spectacle), and his work has been an inspiration for this implementation. Will also pioneered TLA+ animations several years ago, as demonstrated in his presentation at the TLA+ Community Event 2018 (https://www.youtube.com/watch?v=mLF220fPrP4). Spectacle remains unique as the only tool that runs entirely in the browser, providing an incredibly accessible way to explore and share TLA+ specifications with no installation required.

The TLA+ Debugger implementation builds on this concept while offering complementary capabilities:

- **Step through individual formulas** of your specification at the expression level

- **Support for the largest fragment of TLA+** by virtue of being implemented on top of TLC

- **Integration with the full debugging ecosystem** (breakpoints, watch expressions, call stacks, etc.)

Both tools have their strengths, and I encourage you to explore both approaches!

## Screencasts

Three screencasts demonstrate these new features in action:

1. **Interactive State-Space Exploration & Graphical Debugging with Animations**

https://www.youtube.com/watch?v=ZrzoIYjFeHE

2. **Breakpoint Conditions with Deadlock Detection**

https://www.youtube.com/watch?v=aTW87nTmAmQ

3. **Dynamic Trace Export and Advanced Watch Expressions**

https://www.youtube.com/watch?v=cIXqCmEr_V4

## Technical Details

For those interested in implementation details, the last 39 commit messages up to and including https://github.com/tlaplus/tlaplus/commit/3e083e3d8b0dc0202307e1496f7889f0f3cb21d7 contain extensive context about these features, including:

- Support for conditional breakpoints on initial and next states

- Deterministic sorting of successor states by action location and state values

- Unified infrastructure for Watch and Debug expressions

- Step-in functionality using minimal Hamming distance to select "close" successor states

- Step-over functionality using maximal Hamming distance to select "far" successor states

- Preservation of finite stuttering in debugger traces for faithful behavior representation

## Feedback Welcome

I'd love to hear your thoughts on these new capabilities! Please feel free to provide feedback here on the mailing list or on GitHub.

Happy debugging!

Markus