https://docs.tlapl.us/ 2026-05-23T21:45:47+00:00 https://docs.tlapl.us/ https://docs.tlapl.us/_media/logo.png text/html 2025-11-04T09:24:39+00:00 Anonymous (anonymous@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 2024-10-19T20:23:30+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:boxed_comments?rev=1729369410&do=diff Boxed Comments It’s a common practice to use boxed comments in TLA+ specifications: (**************************************************************) (* This is a boxed comment. *) (* Such comment format is used in lots of specifications. *) (**************************************************************) text/html 2024-10-19T18:55:50+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:caveats?rev=1729364150&do=diff Caveats Here you can find a list of known minor problems that you might encounter while working with the extension. We hope they’ll be fixed some day, but at the moment, just be aware of them. PlusCal algorithm boundaries detection The following PlusCal algorithm declarations are totally correct: text/html 2024-10-19T18:56:04+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:commands?rev=1729364164&do=diff Commands The extension provides the following commands in the Command Palette: * TLA+: Parse module for translating PlusCal to TLA+ and checking syntax of the resulting specification. * TLA+: Check model for running the TLC model checker on the TLA+ specification. text/html 2024-10-19T19:21:29+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:fonts?rev=1729365689&do=diff Fonts TLA+ widely uses the language of mathematics, and its syntax contains great deal of character sequences that represent mathematical symbols. So why not use those symbols directly when displaying specifications in the text editor? There’re two levels of visualization improvements: text/html 2024-10-19T19:03:13+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:formatting_preferences?rev=1729364593&do=diff Formatting Preferences By default, the extension is configured to help you with formatting the code while you’re typing. If you want to change any aspect of this behavior, you can do it by editing the tlaplus language settings. To do that: * Open the text/html 2025-09-17T18:00:21+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:getting_started?rev=1758132021&do=diff Getting Started The easiest way to get a simple working model is to create an empty PlusCal algorithm, translate it into a TLA+ specification and run the TLC tool on it. Here’s a step by step instruction: Create a specification file. Let’s name it text/html 2024-10-25T16:58:09+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:installing_java?rev=1729875489&do=diff Installing Java Why Java? The extension uses the official TLA⁺ tools to support such features as PlusCal-to-TLA+ translation, module parsing, model checking etc. These tools need JVM (Java Virtual Machine) to run, and the extension doesn’t come with a JVM onboard. Thus, it requires a JVM to be installed on the user’s computer. text/html 2024-10-19T19:23:01+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:java_options?rev=1729365781&do=diff Java Options The Java: Options setting allows you to provide additional options that will be passed to the Java process when running TLA+ tools. At the same time, the extension itself adds a couple of default options when running Java. Thus, it sometimes has to “merge” those default options with ones provided by the user. During this merging, the user settings always take precedence. text/html 2024-10-19T20:24:31+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:keyboard_shortcuts?rev=1729369471&do=diff Keyboard Shortcuts The extension provides various commands, at least some of which you’ll probably want to use often enough to have keyboard shortcuts for them. The extension purposefully doesn’t provide predefined shortcuts to not meddle with the existing user settings. text/html 2025-10-10T20:39:58+00:00 Anonymous (anonymous@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-11-04T09:29:20+00:00 Anonymous (anonymous@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-05-31T22:41:42+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:start?rev=1748731302&do=diff Visual Studio Code Extension This is the fastest and easiest way to get started with TLA+ and TLC. * Download and install Visual Studio Code * Open it, go to the Marketplace panel, find the "TLA+" extension and click "Install". Make sure to install TLA+ from TLA+ Foundation. Url: text/html 2024-10-19T18:59:49+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:troubleshooting?rev=1729364389&do=diff Troubleshooting Here is the list of troubles the user may encounter and recipes for dealing with them. Message: Unsupported Java version: X The extension shows this message when it finds out that the version of the JVM you use for running the TLA+ text/html 2024-10-19T20:22:28+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/using:vscode:visualizing_states?rev=1729369348&do=diff Visualizing States TLC model checker can dump generated states to a file in DOT notation. Such .dot files can be visualized as graphs right in VS Code with the help of additional extensions. Here’re the most popular of them: - Graphviz Interactive Preview, - Graphviz Preview, - Graphviz (dot) language support for Visual Studio Code. To generate .dot files while running model checking, add