TLA+ Wiki

This is an old revision of the document!

PHP's gd library is missing or unable to create PNG images

The extension provides the following commands in the Command Palette:

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

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