https://docs.tlapl.us/ 2026-04-08T11:40:18+00:00 https://docs.tlapl.us/ https://docs.tlapl.us/_media/logo.png text/html 2024-10-25T16:51:20+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:ai_linter?rev=1729875080&do=diff AI Linter TLA+ does not come with a traditional linter or formatter. The TLA+ AI Linter is a GenAI script that uses LLMs to lint TLA+ files. Find more info on: <https://microsoft.github.io/genaiscript/case-studies/tla-ai-linter/> text/html 2024-09-28T23:23:52+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:ci_for_specs?rev=1727565832&do=diff CI for your specifications If you want to quickly have a repository with CI running to verify your specs, please check out this template: <https://github.com/FedericoPonzi/tlaplus-specs-template> text/html 2024-09-28T23:24:33+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:community_modules?rev=1727565873&do=diff Community Modules What are community modules How to use from CLI How to use with vscode text/html 2024-10-07T16:42:29+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:coverage?rev=1728319349&do=diff Coverage (draft) Coverage measures how many times each action is executed to generate a new state. This helps identify actions that never run (potential errors) and highlights performance bottlenecks during model checking. How to read coverage? // Determine if the mapping from the action's name/identifier/declaration to the // action's definition is 1:1 or 1:N. // // Act == /\ x = 23 // /\ x' = 42 // vs // Act == \/ /\ x = 23 // /\ x' = 42 // \/ /\ x = 123 // … text/html 2024-09-28T23:26:44+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:debugger?rev=1727566004&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>. text/html 2024-11-17T13:00:07+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:experimental?rev=1731848407&do=diff Experimental Features These features are experimental. They are expected to work correctly but are not officially supported. If you are want, you can test them out and report your feedback on Github. Also, other than experimental features, it's possible to tweak some of the default values using system properties. text/html 2024-09-28T15:58:48+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:generating_animation?rev=1727539128&do=diff Generating Animations of State Changes Writing animation specifications is straightforward. There is a module that provides TLA+ definitions of SVG primitives. Below are a few examples. The first three are for TLC, and the other ones are for Will Schultz’s TLA-web. Despite being for different systems, the definitions are quite similar. text/html 2024-09-28T15:58:40+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:generating_sequence_diagrams?rev=1727539120&do=diff Generating sequence diagrams This is a tool for generating sequence diagrams from TLC state traces. It produces SVGs that look like: [Sequence diagram] or like this PDF. Link to the tool here. text/html 2025-02-18T13:01:38+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:generating_state_graphs?rev=1739883698&do=diff Generating state graphs to visualize the state space TLC support the generation of a dot file that can be used to visualize the state space. first generate dot file: java -cp ./dist/tla2tools.jar tlc2.TLC -dump dot test.dot /home/fponzi/dev/tla+/Examples/specifications/glowingRaccoon/clean.tla text/html 2024-09-28T15:58:41+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:generating_tests_from_models?rev=1727539121&do=diff Generating tests from models You can use modelator: https://github.com/informalsystems/modelator It can be installed through pip (python’s package manager): pip install modelator text/html 2024-12-26T08:40:31+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:large_scale_model_checking?rev=1735202431&do=diff Large Scale Model Checking If you need to model check a very large state space, then it is a good idea to watch this video from TLA+ conf from 2018 where Markus Kuppe shares some tricks on how to improve TLC model checker performances: text/html 2024-09-28T15:58:54+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:limitations?rev=1727539134&do=diff Limitations text/html 2024-09-28T15:58:52+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:operator_override?rev=1727539132&do=diff Operator override TODO: <https://github.com/tlaplus/tlaplus/issues/413#issuecomment-571330604> text/html 2024-09-28T18:21:28+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:pgo_generating_go_from_pluscal?rev=1727547688&do=diff Generating GO from pluscal specs PGo is a source to source compiler that translates Modular PlusCal specifications (which use a superset of PlusCal) into Go programs. * Homepage: https://distcompiler.github.io/ * Repo: https://github.com/DistCompiler/pgo text/html 2024-09-28T23:28:20+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:sany?rev=1727566100&do=diff Exploring the semantic graph the ExplorerVisitor received an extension to export the semantic graph into dot notation, which can be rendered with GraphViz: java -cp tla2tools.jartla2sany.SANY -d ATLA+Spec.tla dot It optionally includes line numbers if the system property text/html 2024-10-10T16:42:54+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:standard_lib?rev=1728578574&do=diff Standard Library Modules ''Naturals'', ''Integers'', ''Reals'' * Nat, Int, Real * +, −, ∗, /, ^ * <=, >=, >, < * .. * Infinity Module ''Sequences'' The Sequences module defines operations on finite sequences. We represent a finite sequence as a tuple, so the sequence of three numbers 3, 2, 1 is the triple <<3, 2, 1>>. The Sequences module defines the following operators on sequences: text/html 2025-11-04T09:29:47+00:00 Anonymous (anonymous@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 2024-10-10T16:59:47+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:syntax_aliases?rev=1728579587&do=diff Syntax Aliases Different ways of writing the same symbol. The first column shows the canonical way, but the second column are aliases and will work as well. Symbol Synonym(s) \lnot ~, \neg, ¬ [] □ <> ◇ \land /\, ∧ \lor \/, ∨ \equiv text/html 2024-10-25T17:01:05+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:tla_web_explorer?rev=1729875665&do=diff TLA+ Web Explorer Homepage and the source code is hosted on GitHub. The current version of the tool utilizes the TLA+ tree-sitter grammar for parsing TLA+ specs and implements a TLA+ interpreter/executor on top of this in Javascript. This allows the tool to interpret specs natively in the browser, without relying on an external language server. The Javascript interpreter is likely much slower than TLC, but efficient model checking isn’t currently a goal of the tool. text/html 2024-10-25T17:06:46+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:tlaplus_formatter?rev=1729876006&do=diff TLA+ Formatter There is a TLA+ formatter available here: <https://github.com/FedericoPonzi/tlaplus-formatter> The formatter is still work in progress. It uses the official SANY implementation from tlatools. It's open for contributions as well, if you have experience in crafting formatters or compilers please do reach out. text/html 2024-10-10T09:13:17+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:toolbox?rev=1728551597&do=diff TLA+ Toolbox The TLA Toolbox is an IDE (integrated development environment) for the TLA+ tools. Users who would prefer a more lightweight IDE for TLA+ may want to try the Visual Studio Code extension for TLA+. However, it lacks many of the Toolbox's features.