---

abstract: | This document is intended to summarize the main constructs that a user of PlusCal and TLA^+^ who is using the Toolbox and TLC is likely to encounter. It does not replace the available introductory material about TLA^+^ and is also not meant as a reference manual. Feedback to the author is welcome. author:

• | Stephan Merz
  stephan.merz@loria.fr title: 'PlusCal / : An Annotated Cheat Sheet'

---

PlusCal

PlusCal is an algorithmic language that has the "look and feel" of imperative pseudo-code for describing concurrent algorithms. It has a formal semantics, through translation to TLA^+^, and algorithms can be verified using the TLA^+^ tools. We describe here the "C syntax" of PlusCal, but there is also a "P syntax" closer to the Pascal programming language.

A PlusCal algorithm appears inside a comment within a TLA^+^ module. Its top-level syntax is as follows.

--algorithm name {
  (* declaration of global variables *)
  (* operator definitions *)
  (* macro definitions *)
  (* procedures *)
  (* algorithm body or process declarations *)
}

Variable declarations, operator and macro definitions, as well as procedures are optional. There must either be an algorithm body (for a sequential algorithm) or process declarations (for a concurrent algorithm).

The PlusCal translator embeds the TLA^+^ specification corresponding to the PlusCal algorithm in the module within which the algorithm appears, immediately following the algorithm. The translation is delimited by the lines

\* BEGIN TRANSLATION
...
\* END TRANSLATION

Users should not touch this area, as it will be overwritten whenever the PlusCal translator is invoked. However, TLA^+^ definitions may appear either before the PlusCal algorithm or after the generated TLA^+^ specification. In particular, operators defined before the PlusCal algorithm may be used in the algorithm. Correctness properties are defined below the generated specification because they refer to the variables declared by the translator.

Variable declarations.

Variables are declared as follows, they may (but need not) be initialized:

variables x, y=0, z \in {1,2,3};

Note that there may be at most one "variables" clause, but that it may declare any number of variables. This example declares three variables $x$, $y$, and $z$. The variable $x$ is not initialized, $y$ is initialized to $0$, and $z$ may take either $1$, $2$ or $3$ as initial values. During model checking, TLC will assign $x$ a default value that is different from all ordinary values and will explore all three initial values for $z$.

Operator definitions.

As in TLA^+^(see below), operators represent utility functions for describing the algorithm. The syntax is the same as for TLA^+^ definitions, explained below. For example,

define {
  Cons(x,s) == << x >> \o s
  Front(s)  == [i \in 1 .. Len(s)-1 |-> s[i]]
}

declares an operator $\mathit{Cons}$ that prepends an element $x$ to a sequence $s$ and an operator $\mathit{Front}$ that returns the subsequence of a non-empty sequence without the last element. Again, there can be a single "define" clause, but it may contain any number of operator definitions, without any separator symbol.

Macros.

A macro represents several PlusCal statements that can be inserted into an algorithm, and it may have parameters. In contrast to a defined operator, a macro need not be purely functional but may have side effects. In contrast to a procedure, it cannot be recursive and may not contain labels or complex statements such as loops or procedure calls or return statements. Here are two examples:

macro send(to, msg) {
  network[to] := Append(@, msg)
}
macro rcv(p, var) {
  await Len(network[p]) > 0;
  var := Head(network[p]);
  network[p] := Tail(@)
}

These macros represent send and receive operations in a network represented by FIFO queues indexed by processes. The first macro appends a message to the queue of the destination process. The second macro blocks until the queue of process $p$ contains at least a message, then assigns the first message in the queue to variable $\mathit{var}$ and removes it from that queue. When using a macro, simply insert an invocation as a statement in the code, such as send(p, x+1) for sending the value $x+1$ to process $p$.

Procedures.

A procedure declaration is similar to that of a macro, but it may also contain the declaration of local variables.[^1] The procedure body may contain arbitrary statements, including procedure calls (even recursive calls).

procedure p(x,y)
    variable z=x+1  \* procedure-local variable
{
    call q(z,y);
l:  y := y+1;
    return
}

Procedure parameters are treated as variables and may be assigned to. Any control flow in a procedure should reach a return statement, any result computed by the procedure should be stored in a variable---possibly a parameter. Procedure calls are preceded by the keyword call and must be followed by a label.

Since the PlusCal translator introduces a stack for handling procedures, a PlusCal algorithm using procedures must appear in a module [[extend]{.smallcaps}]{.nodecor}ing the standard module Sequences.

Processes.

A PlusCal algorithm may declare one or more process templates, each of which can have several instances. A process template looks as follows:

process (name [= | \in] e)
   variables ...   \* process-local variables
{
   (* process body *)
}

The form "$name = e$" will give rise to one instance of the process whose process identity is (the value of expression) $e$, whereas "$name \in e$" will create one process instance per element of the set $e$. When creating several process instances from different templates, it is important to ensure that all process identities are comparable and different: for example, use only integers, only strings or only model values. Within the process body, the process identity is referred to as self (and not as name as the syntax might suggest). Processes conceptually execute (asynchronously) in parallel, from the start of execution of the algorithms: PlusCal does not support dynamically spawning processes during execution.

PlusCal statements.

The statements of PlusCal are those expected of a simple imperative language, with the addition of primitives for synchronization and for non-deterministic choice that are useful for specifications.

Assignments are written x := e, but PlusCal also supports assignments to components of an array x[i,j] := e whose translation involves [[except]{.smallcaps}]{.nodecor} forms in TLA^+^. PlusCal also has a statement print e for printing the value of an expression.[^2] However, due to the breadth-first state enumeration strategy used by default in TLC, it may not always be obvious to understand the relationship between outputs to the console and actual execution flow.

The conditional statement has the usual form

   if (exp) ... else ...

where the "else" branch is optional; compound statements are enclosed in braces. Similarly, while loops are written

   while (exp) ...

Other statements for transferring the flow of control are procedure call and return (see above), as well as goto l for jumping to label $l$---see below for a more detailed explanation of labels in PlusCal.

Assertions can be embedded in PlusCal in the form assert e. This statement has no effect if the predicate $e$ is true and otherwise aborts (producing a counter-example trace in TLC). There is also skip, which does nothing and is equivalent to assert TRUE.

The statement await e (which can alternatively be written when e) blocks execution until the condition is true. This is useful for synchronizing parallel processes, for example for blocking message reception until a message has actually been received.

Finally, PlusCal offers two statements for modeling non-determinism. The first form,

  either \* first choice
  or     \* second choice
  or     \* ...

is useful for expressing the choice between a fixed number of alternatives. A useful idiom for restricting this choice is to add await statements to branches: only those choices whose condition evaluate to [[true]{.smallcaps}]{.nodecor} can indeed be executed. (This is PlusCal's version of Dijkstra's guarded commands.)

Second, the form

   with (x \in S) ...

allows for choices based on the elements of set $S$: the variable $x$ acts as a local variable whose scope is restricted to the body of the with statement. For example, in a model where communication is not necessarily FIFO, $S$ could be the set of messages that a process has received, and a with statement could be used to handle any one of these messages.

Semicolons.

Unlike in C and similar languages, PlusCal uses semicolons to separate (and not end) statements. In particular, this means that no semicolon is required before the closing brace of a compound statement (although it is not considered as a syntax error). However, a semicolon is required after the closing brace if it is followed by another statement.

Labels.

PlusCal statements can be labeled, and the primary purpose of labels is to indicate the "grain of atomicity" in the execution of parallel processes. The idea is that a group of statements that appears between two labels is executed without interruption by any other process. However, the PlusCal translator imposes certain labeling rules. The most important ones are:

• The first statement in the body of a procedure, a process or of the algorithm body must be labeled.

• A while statement must be labeled.

• Any statement following a call, a return or an if or either statement that contains a labeled statement must be labeled.

• A macro body and the body of a with statement may not contai