Java Options

The Java: Options setting allows you to provide additional options that will be passed to the Java process when running TLA⁺ tools.

At the same time, the extension itself adds a couple of default options when running Java. Thus, it sometimes has to “merge” those default options with ones provided by the user. During this merging, the user settings always take precedence.

The following sections describe how it works.

Some useful information, related to class path:

1. The only class path item that the extensions provides is the path to tla2tools.jar which is bundled with the extension package.
2. The current directory of any TLA⁺ command is always the directory of the file on which you run the command (a spec or a model file). So, it’s possible to use relative paths to dependencies when needed.
3. You can always see the full command line that the extension uses when running a TLA⁺ command by opening the Output panel and switching to the channel of that command.

The examples below use colon (:) to separate paths, which is the Unix-way of doing it. On Windows, use semicolon (;) for that purpose.

If you provide a -cp or -classpath option that doesn’t explicitly contain a path to the tal2tools.jar library, the exstension will add the default class path to the end of the option value.

For instance, if you want to include the Community Modules library in the class path, just add the -cp /somewhere/CommunityModules.jar option, and the extension will run JVM with the following line: -cp /somewhere/CommunityModules.jar:/path/to/tla2tools.jar.

If you want to use a non-default tla2tools.jar library version, you can put the path to this library to your -cp option, and the extension will not use the default one.

The place of the library inside the full class path string doesn’t matter. The only rule is to specify the name of the library explicitly.

For instance, the -cp /custom/path/to/tla2tools.jar:/somewhere/MyLibrary.jar option will make the extension use this class path without any modifications.

Following official recommendations, the extension passes the -XX:UseParallelGC option to JVM, forcing it to use the Parallel Garbage Collector, which is throughput-oriented and usually makes TLA⁺ tools work faster.

But if you want to use a different GC, just provide the option for switching to it (for example, -XX:UseG1GC), and the extension will stop using the default one.