A Simple Spec

TLA+ started as a notation, and the model checker, TLC, only came out 5 years later. As it was never intended to be run, there’s some assumptions of it being a read document instead of being runnable code. That means that there’s a little bit of boilerplate we’ll need to get through first.

In order for TLC to analyze a spec, it must have the following format:

---- MODULE module_name ----
\* TLA+ code

(* --algorithm algorithm_name
\* PlusCal code
end algorithm; *)

TLC will only analyze the code between the ---- beginning and the ==== end. Anything outside of those boundaries is ignored. module_name must be the same as the filename, while algorithm_name can be whatever you want. \* is a line comment and (* is a block comment. Note we’re putting our algorithm in a comment. If you don’t put it in a comment, you’ll get a syntax error, because PlusCal isn’t TLA+.

PlusCal came out fifteen years after TLA+ did. TLC is supposed to perfectly follow the semantics of TLA+, and since PlusCal is a completely different style it can’t be fit into the same schema. Behind the scenes, we transpile the PlusCal to raw TLA+, and the --algorithm in comments is there to let the PlusCal translator know what it’s supposed to be translating.

You can only have one PlusCal algorithm per file.

As for the PlusCal itself, here’s the layout of a basic single process algorithm:

variables x = 1, y \in {3, 4}, z = {3, 4};
  \* your code here
end algorithm;

In the variables block, = is assignment. Everywhere else, = is the equality check and := is assignment.

You might have noticed the y \in {3, 4}. That’s set notation. It means that for the purposes of this algorithm, y can be 3 or 4. When you check the model, TLC will make sure it works for all possible values of y. It will first test that nothing fails with y = 3, and then test that nothing fails with y = 4.

Contrast y \in {3, 4} with z = {3, 4}, which means that z is the set {3, 4}. Any sort of data structure can be assigned to a variable in TLA+.

Since TLA+ is a specification language, it was designed to output really nice documents. That’s why we use TeX like \in and \union and such. Fun fact: Leslie Lamport, the inventor of TLA+, also invented LaTeX! Another fun fact: we won’t be talking about outputting as a specification in any way whatsoever. Cool stuff, but not immediately relevant to model checking.

Let’s get Hello World out of the way.


(* --algorithm hello_world
variable s \in {"Hello", "World!"};
    print s;
end algorithm; *)

The EXTENDS is the #include analog for TLA+. TLC is a module that adds print and assert. print is, incidentally, the only IO possible with TLA+ and is provided for debugging purposes.

The only thing that may be unusual here is the A:. That is called a label. TLC treats labels as the “steps” in a specification; everything in the label happens at once. It’s only between labels that the model can check invariants and switch processes. Also, you can’t assign to the same variable twice in the same label. For the most part, it isn’t too useful here. But it will be pretty important later.

If you leave the A: out, your PlusCal will still transpile. This is because the TLC can infer the labels in a single process app. For the most part it’s fine to leave them out in single process apps, but you should keep them in mind.

I assume that you’re familiar with other programming languages. To make modeling more familiar, PlusCal has similar constructs. The semantics are fairly obvious, so here’s what they look like. Assume all variables have been initialized before and we’re in a begin block.

Logic Operators

logic operator TRUE FALSE
equal = 1 = 1 1 = 2
not equal /= 1 /= 2 1 /= 1
not ~ ~FALSE ~TRUE


if x = 5 then
elsif x = 6 then
end if;


x := 5;
while x > 0 do
  x := x - 1;
end while;

This is the only form of looping.


  if TRUE then goto B else goto C endif;

Goto considered useful in PlusCal.