====== Commands ======

The extension provides the following commands in the [[https://code.visualstudio.com/docs/getstarted/userinterface#_command-palette|Command Palette]]:

  * ''%%TLA+: Parse module%%'' for translating PlusCal to TLA<sup>+</sup> and checking syntax of the resulting specification.
  * ''%%TLA+: Check model%%'' for running the TLC model checker on the TLA<sup>+</sup> specification.
  * ''%%TLA+: Check model with non-default config...%%'' for running the TLC model checker on the TLA<sup>+</sup> 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<sup>+</sup> 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<sup>+</sup> specification.
  * ''%%TLA+: Export module to PDF%%'' for generating a PDF document from a TLA<sup>+</sup> specification.

You’ll probably want to [[alygin/vscode-tlaplus/wiki/Keyboard-Shortcuts|add keyboard shortcuts]] to some of these commands, or even make them [[alygin/vscode-tlaplus/wiki/Automatic-Module-Parsing|run automatically]].