TLA+ Wiki

This is an old revision of the document!

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

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.

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

settings