Skip to content

Commands

Federico Ponzi edited this page Oct 19, 2024 · 7 revisions

This page was moved to: https://docs.tlapl.us/using:vscode: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.

Clone this wiki locally