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<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 detailsPlusCal: 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 detailsTLC 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.
Other Useful Settings
These settings and configuration tricks are not provided by the extension itself, but leverage the general VS Code platform capabilities: