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.
• TLA+: Check model with non-default config... for running the TLC model checker on the TLA⁺ specification. Lets the user select a non-default model config file.
• TLA+: Run last model check again for running TLC again without switching to the spec or model file.
• TLA+: Stop model checking for stopping currently running TLC process. The command is only available when a model checking is in progress.
• TLA+: Evaluate constant expression for evaluating an expression selected in the active editor. This command is also available in the editor context menu.
• TLA+: Evaluate expression... for evaluating an arbitrary TLA⁺ constant expression in the context of the currently open model.
• TLA+: Visualize TLC output for presenting model checking results.
• TLA+: Export module to LaTeX for generating a .tex and .dvi files from a TLA⁺ specification.
• TLA+: Export module to PDF for generating a PDF document from a TLA⁺ specification.

You’ll probably want to add keyboard shortcuts to some of these commands, or even make them run automatically.