Troubleshooting

Here is the list of troubles the user may encounter and recipes for dealing with them.

The extension shows this message when it finds out that the version of the JVM you use for running the TLA⁺ tools is lower than 1.8 (aka Java 8). You need to install (or configure if it’s already installed) a JVM of a higher version.

You can find more information on how to do that here.

The extension shows this message when it cannot find a JVM it could use to run the TLA⁺ tools. You need to either install a JVM or provide the path to an already installed JVM via the extension settings.

You can find more information on how to do that here.

In order to generate PDFs from .tla files, the extension uses external tools (pdflatex by default). The message means that the such a tool command is not provided in the extension setting.

In order to generate PDFs from .tla files, the extension uses external tools (pdflatex by default). The message means that this tool exited with an error when executed.

When such an error occurs, the extension displays the output of this command along with the full command line that was executed. Check the output, it might provide useful information. Also, check the PDF tool command settings.