Using the TLA⁺ Command Line Interface

TLA⁺ is a formal language for modelling concurrent and distributed systems in the form of a mathematical specification. TLA⁺ is often used with a set of tools, such as the TLC model checker, distributed with the official TLA⁺ IDE: the TLA⁺ toolbox.

The toolbox is fine, but I personally prefer to edit my specifications using my favorite editor rather than a specialized IDE. Turns out running the TLA⁺ tools from the command line is quite simple yet not very well documented, that’s why I decided to write down my process for using TLA⁺ outside of the toolbox, hope it helps!

Downloading the tools

The tools are developed on Github and written in Java, each release consists in a few assets such as OS specific versions of the toolbox but also contains a standalone version of the tools in the form of the tla2tools.jar file. To download the tools simply grab the last tla2tools.jar on the release page. At the time of writing, the latest stable release is 1.7.1 and it can be downloaded with:

wget https://github.com/tlaplus/tlaplus/releases/download/v1.7.1/tla2tools.jar

Next, you need a version of Java on your system, I’m using java 11 and it works just fine. You can check your Java installation with java --version. Then running the tools is pretty simple:

java -cp tla2tools.jar tlc2.TLC

This should raise an error (Missing input TLA+ module) but you should also get the version of TLC (TLC2 Version 2.16 in my case) so it’s a good sign that the installation is working.

Using convenient wrappers

For ease of use, I use small bash wrappers around the tools so that I can call tlc directly from command line. You can copy the following scripts and put them somewhere in your $PATH to do the same.

Here are the tools:

TLC

Used to check models. See the TLC section for an example of usage.

#!/usr/bin/env bash

java -cp </path/to/tla2tools.jar> tlc2.TLC $@

TLAToTeX

Produces a .tex file from a TLA⁺ specification that can in turn be used to produce a PDF.

#!/usr/bin/env bash

java -cp </path/to/tla2tools.jar> tla2tex.TLA $@

TeXToTLA

Given a .tex file containing some TLA⁺ in a tla environment, produces a new .tex file with code for rendering the specification. Rendering the final .tex requires having tlatex.sty in scope.

#!/usr/bin/env bash

java -cp </path/to/tla2tools.jar> tla2tex.TeX $@

SANY

A TLA⁺ parser that can report syntax errors in a spec.

#!/usr/bin/env bash

java -cp </path/to/tla2tools.jar> tla2sany.SANY $@

The TLC model checker

Working with TLC from the command line requires to create a few additional files that the toolbox usually generates automatically. Imagine you wan to specify a two bits clock, dump the following spec in a Clock.tla file (the name is important, TLC will complain otherwise):

---------------------- MODULE Clock ----------------------

CONSTANT InitialValue

VARIABLE clock

Init == clock = InitialValue
Tick == IF clock = 0 THEN clock' = 1 ELSE clock' = 0

IsValid == clock \in {0, 1}
Spec    == Init /\ [][Tick]_<<clock>>

==========================================================

So nothing too fancy here, we describe a clock that can take two values: 0 and 1. When doing model checking, we want to give a concrete value to the InitialValue constant, we also want to tell TLC to check some properties such as IsValid.

To do that we need another module, dump the following specification in a ClockModel.tla file:

------------------- MODULE ClockModel --------------------

EXTENDS Clock

InputInitialValue == 0
PropertyIsValid   == []IsValid

==========================================================

This module extends the clock specification Clock (file name are important for this to work!) and defines two predicate. I like to prefix my predicate with Input or Property depending on what they represent. Here we defined an initial value and a temporal property.

Then we need to tell TLC what are the inputs, properties and specifications to check, this is done using a last file ClockModel.cfg (once again, the name is important, it must be the same as the model filename with the .cfg extension instead of .tla).

Copy the following in ClockModel.cfg:

CONSTANT InitialValue <- InputInitialValue
PROPERTY PropertyIsValid
SPECIFICATION Spec

This file tells TLC that the InitialValue constant must take the value InputInitialValue we defined in our model, that it has to check the PropertyIsValid temporal property and that specification is defined by the Spec predicate.

And that’s it, now we can check our model using TLC:

tlc ClockModel.tla

Which should return without error.

Conclusion

I hope this was helpful, you can also find some documentation here or with the -help flag for most tools. Feel free to report issues or corrections here and enjoy writing TLA⁺ specs outside of the toolbox!