Differences

This shows you the differences between two versions of the page.

--- using:debugger [2024/09/28 15:58] – created - external edit 127.0.0.1
+++ using:debugger [2026/04/11 13:27] (current) – fponzi
@@ Line 3: / Line 3: @@
 TLA+ tools come with a debugger that allow you to debug your specifications. See it in action:
-<HTML>
+{{youtube>x6u8LYSso6s?}}
-<iframe width="1333" height="485" src="https://www.youtube.com/embed/x6u8LYSso6s" title="TLA+ Debugger:  Force violation of artificial invariant with &#39;violate&#39; debugger command" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" referrerpolicy="strict-origin-when-cross-origin" allowfullscreen>
+{{youtube>DsfbdsE4hJ0?}}
-</iframe>
-<iframe width="1917" height="806" src="https://www.youtube.com/embed/DsfbdsE4hJ0" title="The TLA+ Debugger" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" referrerpolicy="strict-origin-when-cross-origin" allowfullscreen>
+===== Graphical and time-traveling debugging =====
-</iframe>
-</HTML>
-===== graphical and time-traveling debugging =====
 You will need the SVG extension: https://marketplace.visualstudio.com/items?itemName=jock.svg.
+{{youtube>IO9ik850i0M?}}
+======= interactive state-space exploration - added 2026-01 =======
+The TLA+ Debugger has a new major capability: **interactive state-space exploration**. This feature changes how you can interact with your TLA+ specifications by letting you explore the state space of your models interactively, 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 [[https://github.com/tlaplus/vscode-tlaplus/blob/master/resources/knowledgebase/tla-animations.md|TLA+ animation guide]] 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:
+<code>
+LET J == INSTANCE _JsonTrace
+    WITH _JsonTraceFile <- "output.json"
+IN J!_JsonTrace
+</code>
+This exports the current trace to JSON without needing to preconfigure the debugger or manually trigger violations. Several [[https://github.com/tlaplus/tlaplus/tree/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules|other export formats]] are supported via 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 [[https://github.com/tlaplus/tlaplus/issues/860#issuecomment-2836117684|GitHub issue #860]]: 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 [[https://dl.acm.org/doi/10.1007/978-3-031-26236-4_15|publication]]) and is built on the [[https://microsoft.github.io/debug-adapter-protocol/|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 [[https://github.com/will62794/spectacle|Spectacle]], and his work has been an inspiration for this implementation. Will also pioneered TLA+ animations several years ago, as demonstrated in [[https://www.youtube.com/watch?v=mLF220fPrP4|his presentation at the TLA+ Community Event 2018]]. 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:
+. [[https://www.youtube.com/watch?v=ZrzoIYjFeHE|Interactive State-Space Exploration & Graphical Debugging with Animations]]
+. [[https://www.youtube.com/watch?v=aTW87nTmAmQ|Breakpoint Conditions with Deadlock Detection]]
+. [[https://www.youtube.com/watch?v=cIXqCmEr_V4|Dynamic Trace Export and Advanced Watch Expressions]]
+====== Technical Details ======
+For those interested in implementation details, the last 39 commit messages up to and including [[https://github.com/tlaplus/tlaplus/commit/3e083e3d8b0dc0202307e1496f7889f0f3cb21d7|this commit]] 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.
-<HTML>
-<iframe width="1917" height="806" src="https://www.youtube.com/embed/IO9ik850i0M" title="Graphical and time-traveling debugging for TLA+" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" referrerpolicy="strict-origin-when-cross-origin" allowfullscreen>
-</iframe>
-</HTML>