https://docs.tlapl.us/ 2026-05-05T11:39:40+00:00 https://docs.tlapl.us/ https://docs.tlapl.us/_media/logo.png text/html 2026-04-11T13:27:23+00:00 fponzi (fponzi@undisclosed.example.com) https://docs.tlapl.us/using:debugger?rev=1775914043&do=diff Debugger TLA+ tools come with a debugger that allow you to debug your specifications. See it in action: Graphical and time-traveling debugging You will need the SVG extension: <https://marketplace.visualstudio.com/items?itemName=jock.svg>. interactive state-space exploration - added 2026-01 The TLA+ Debugger has a new major capability: text/html 2025-11-04T17:32:49+00:00 ahelwer (ahelwer@undisclosed.example.com) https://docs.tlapl.us/creating:jlists?rev=1762277569&do=diff Conjunction & Disjunction Lists Chapter 9 of Crafting Interpreters covers control flow - if, while, for, and all that. TLA⁺ doesn't really have that, because TLA⁺ specifications aren't imperative programs. However, TLA⁺ does have something similar. When specifying a system's actions, we commonly need to do two things: write preconditions or "guards" controlling whether an action can be taken, and specify the set of possible next-state transitions. For the former we use conjunction (aka logical … text/html 2025-11-04T09:29:47+00:00 fponzi (fponzi@undisclosed.example.com) https://docs.tlapl.us/using:start?rev=1762248587&do=diff Using TLA+ Browse Topics: * Apalache Symbolic Model Checker * Apalache Symbolic Model Checker * IntelliJ plugin for TLA+ * IntelliJ plugin for TLA+ * TLA+ Tools for Emacs users * TLA+ Tools for Emacs users * TLC Model Checker * Config files * Liveness checks * TLC Model Checker * Trace Validation * Visual Studio Code Extension * Automatic Module Parsing * Boxed Comments * Caveats * Commands * Fonts * Formatting Preferences * Getting Started * Installing… text/html 2025-11-04T09:29:20+00:00 fponzi (fponzi@undisclosed.example.com) https://docs.tlapl.us/using:vscode:settings?rev=1762248560&do=diff Settings This section provides the list of various settings that allow you to configure the extension to fit your preferences. Extension Settings These settings are available in the Extensions → TLA+ section of the Settings panel: * Java: Home allows to provide location of the JVM that the extension must use for running TLA text/html 2025-11-04T09:24:39+00:00 fponzi (fponzi@undisclosed.example.com) https://docs.tlapl.us/using:vscode:automatic_module_parsing?rev=1762248279&do=diff Automatic Module Parsing The extension provides the TLA+: Parse module command for both translating a PlusCal algorithm to TLA+ code and parsing the resulting TLA+ module. This command is so important in the specification writing process that you might want it to be executed every time you save a .tla file to get quicker response. text/html 2025-11-03T23:15:27+00:00 ahelwer (ahelwer@undisclosed.example.com) https://docs.tlapl.us/creating:safety?rev=1762211727&do=diff Model-Checking Safety Properties This has been a long journey. We learned scanning, then parsing, then how to interpret basic constant expressions. Statements were added next, then we mastered the difficult art of parsing conjunction & disjunction lists. Finally, we learned how to apply operators and move between states. Everything is in place; it is time to write a TLA⁺ model-checker. text/html 2025-11-03T23:08:24+00:00 ahelwer (ahelwer@undisclosed.example.com) https://docs.tlapl.us/creating:actions?rev=1762211304&do=diff Variables, States, and Actions Currently, our implementation is not significantly different from any other ordinary programming language. However, TLA⁺ is not an ordinary language - it isn't even a programming language! TLA⁺ specifications are not programs. Properly speaking, a TLA⁺ specification is a predicate over an infinite sequence of states, where states are an assignment of values to variables. TLA⁺ specs' closest analogue to program execution is enumerating the set of all unique reachab… text/html 2025-10-10T20:39:58+00:00 fponzi (fponzi@undisclosed.example.com) https://docs.tlapl.us/using:vscode:migrating_from_tlatoolbox?rev=1760128798&do=diff Migrating from TLA+ Toolbox TLA+ Toolbox is an IDE based on Eclipse, and for a long time it has been the official environment to work with TLA+ tools. See: <https://lamport.azurewebsites.net/tla/toolbox.html> Since around 2020 the development focus has moved to improve the VScode plugin experience. The TLA+ Toolbox has now moved to archived mode. The current bugs won't be fixed and as as dependency rots, eventually it will stop being distributed as well. Therefore it is not recommended for dai… text/html 2025-09-17T17:58:32+00:00 fponzi (fponzi@undisclosed.example.com) https://docs.tlapl.us/?image=using%3Avscode%3A490491581-c07ab104-e45c-43e3-bbc1-29a32cad6c74.png&ns=using%3Avscode&rev=1758131912&tab_details=history&media_do=diff&do=media <img src="https://docs.tlapl.us/_media/using:vscode:490491581-c07ab104-e45c-43e3-bbc1-29a32cad6c74.png?w=500&amp;h=500&amp;tok=13ba56" alt="490491581-c07ab104-e45c-43e3-bbc1-29a32cad6c74.png" loading="lazy" width="500" height="500" /> text/html 2025-05-31T22:48:29+00:00 fponzi (fponzi@undisclosed.example.com) https://docs.tlapl.us/?image=using%3Avscode%3Avscode-snippet-module.png&ns=using%3Avscode&rev=1748731709&tab_details=history&media_do=diff&do=media <img src="https://docs.tlapl.us/_media/using:vscode:vscode-snippet-module.png?w=500&amp;h=500&amp;tok=6881c6" alt="vscode-snippet-module.png" loading="lazy" width="500" height="500" /> text/html 2025-05-31T22:47:18+00:00 fponzi (fponzi@undisclosed.example.com) https://docs.tlapl.us/?image=using%3Avscode%3Avscode_select_language.png&ns=using%3Avscode&rev=1748731638&tab_details=history&media_do=diff&do=media <img src="https://docs.tlapl.us/_media/using:vscode:vscode_select_language.png?w=500&amp;h=500&amp;tok=500203" alt="vscode_select_language.png" loading="lazy" width="500" height="500" /> text/html 2024-10-02T17:44:53+00:00 fponzi (fponzi@undisclosed.example.com) https://docs.tlapl.us/?image=logo-150.png&ns=&rev=1727891093&tab_details=history&media_do=diff&do=media <img src="https://docs.tlapl.us/_media/logo-150.png?w=500&amp;h=500&amp;tok=4eafcc" alt="logo-150.png" loading="lazy" width="500" height="500" /> text/html 2024-10-02T17:42:16+00:00 fponzi (fponzi@undisclosed.example.com) https://docs.tlapl.us/?image=logo.png&ns=&rev=1727890936&tab_details=history&media_do=diff&do=media <img src="https://docs.tlapl.us/_media/logo.png?w=500&amp;h=500&amp;tok=e4424c" alt="logo.png" loading="lazy" width="500" height="500" /> text/html 2024-09-28T22:18:46+00:00 fponzi (fponzi@undisclosed.example.com) https://docs.tlapl.us/?image=learning%3Adistributed-toolbox.png&ns=learning&rev=1727561926&tab_details=history&media_do=diff&do=media <img src="https://docs.tlapl.us/_media/learning:distributed-toolbox.png?w=500&amp;h=500&amp;tok=4b22f0" alt="distributed-toolbox.png" loading="lazy" width="500" height="500" />