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 Extensions → 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 the Java process when running TLA⁺ tools. More details
• 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. This setting supports variables ${specName} and ${modelName} that are automatically substituted to the .tla and .cfg file names (without extensions) respectively. More details
• TLC Model Checker: Statistics Sharing allows to opt-in / opt-out sharing of TLC usage statistics. More details.
• 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 itself, but leverage the general VS Code platform capabilities:

• Keyboard Shortcuts
• Automatic Module Parsing
• Formatting Preferences