Settings

This section provides the list of various settings that allow you to configure the extension to fit your preferences.

Extension Settings

These settings are available in the TLA+ section of the Settings panel:

• Java: Home allows to provide location of the JVM that the extension must use for running TLA⁺ tools.
• Java: Options allows to provide additional options that must be passed to a Java process when running TLA⁺ tools.
• PlusCal: Options allows to provide additional options to the PlusCal transpiler.
• TLC Model Checker: Create Out Files defines if TLC model checker output should be sent to a .out file.
• TLC Model Checker: Options allows to provide additional options to the TLC model checker.
• PDF: Convert Command specifies what command should be used to generate PDF documents from .tla files.

Other Useful Settings

These settings and configuration tricks are not provided by the extension itsel, but leverage the general VS Code platform capabilibies:

• Keyboard Shortcuts
• Automatic Module Parsing
• Formatting Preferences