The class will be illustrated with the languages PlusCal/TLA+ and related tools. There are two options to write and verify PlusCal/TLA+ models. The first one consists in using Codium or VS Code. However, it may not be available on the computers at ENSEIRB-MATMECA due to lack of disk space. The other option is to use the TLA+ toolbox.

Using Codium or VS Code

An extension supporting PlusCal and TLA+ is provided by the VS Code market place. The extension is called TLA+.

Codium is the open-source version of VS Code which does not contain some features added by Microsoft (as telemetry). In order to install the extension in Codium, you first need to download it here.

The TLA+ toolbox

The TLA+ toolbox is the official tool to write and verify PlusCal/TLA+ models. It is based on eclipse (for the best and the worst). It is available on the computers at ENSEIRB-MATMECA at the followign path ~herbrete/public/TLA/toolbox. You can add this path to your environment variable PATH. The toolbox is launched via the command toolbox in a terminal.

Command line tools

Command line tools are also convenient to launch verification from a script and to access features that are not provided by the GUIs. The command-line tools can be download from the GitHub page of the TLA+ project. It is also available on your account at ENSEIRB-MATMECA as ~herbrete/public/TLA/tla2tools.jar.

Run java -jar ~herbrete/public/TLA/tla2tools.jar -help to obtain the list of available options, as well as instructions on how to invoke the tools.

One particular useful feature is accessible through the command line tool: state-space dumping. If option -dump is specified, TLC will output the explored state-space in the graphviz file format. The state-space may then be visualized using the tool dot (if it is not too big), or even manipulated using the graphviz library. For instance, pygraphviz is a Python library that allows to manipulate graphviz files. Here is an example on how to dump the state-space of the model in model.tla:

java -jar tla2tools.jar -dump dot model.dot -config model.cfg model.tla

Then, this dot file can be visualized either directly within VS Code using a plugin (e.g. GraphViz preview). Or generating a PDF file using the command line:

dot -T pdf -o model.pdf model.dot