TLA+ Wiki

This is an old revision of the document!

The extension provides the TLA+: Parse module command for both translating a PlusCal algorithm to TLA<html>^{</html>+<html>}</html> code and parsing the resulting TLA<html>^{</html>+<html>}</html> 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.

There’s a simple way to do that:

Open the Command Palette and execute the command Preferences: Configure Language Specific Settings... → TLA+.
Set the source property of the editor.codeActionsOnSave setting to true. The final result should look like this:

    "[tlaplus]": {
        "editor.codeActionsOnSave": {
            "source": true
        }
    }

That’s it. From now on, every time you save a .tla file the extension will automatically run the TLA+: Parse module on it and report errors if there any.

Automatic Module Parsing