TLA+ Wiki

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

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<html>^{</html>+<html>}</html> tools.
Java: Options allows to provide additional options that must be passed to the Java process when running TLA<html>^{</html>+<html>}</html> 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.
PDF: Comments Shade enables a gray background on comments (the reminder for the line starting from the first \*.).
PDF: Comments Shade Color if Comments Shade is enable, allows you to choose the backgroud color.
PDF: No Pcal Shade disable the "comment" shading for pcal specifications.
PDF: Number Lines add line number on to the generated pdf file.

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

Settings