Tutorial on checking PlusCal specifications with Apalache
Difficulty: Blue trail – Easy
In this short tutorial, we show how to annotate a PlusCal specification of the Bakery algorithm, to check it with Apalache. In particular, we check mutual exclusion by bounded model checking (which considers only bounded executions). Moreover, we automatically prove mutual exclusion for unbounded executions by induction.
We only focus on the part related to Apalache. If you want to understand the Bakery algorithm and its specification, check the comments in the original PlusCal specification.
Setup
We assume that you have Apalache installed. If not, check the manual page on Apalache installation. The minimal required version is 0.22.0.
Running example: Bakery
We start with the PlusCal specification of the Bakery algorithm. This specification has been checked with the model checker TLC. Moreover, Leslie Lamport has proved safety of this algorithm with the TLAPS.
Step 0: Remove the TLAPS proof
Since we are not interested in the TLAPS proof, we copy Bakery.tla to BakeryWoTlaps.tla and modify it as follows:

Remove
TLAPS
from the list of extended modulesEXTENDS Naturals

Remove the theorem and its proof:
THEOREM Spec => []MutualExclusion ...
Step 1: Add a module with type annotations
Let us check the types of BakeryWoTlaps.tla with Apalache:
$ apalachemc typecheck BakeryWoTlaps.tla
...
Typing input error: Expected a type annotation for VARIABLE max
The type checker complains about missing type annotations. See the Tutorial on Snowcat for details. When we try to add type annotations to the variables, we run into an issue. Indeed, the variables are declared with the PlusCal syntax:
algorithm Bakery
{ variables num = [i \in Procs > 0], flag = [i \in Procs > FALSE];
fair process (p \in Procs)
variables unchecked = {}, max = 0, nxt = 1 ;
The most straightforward approach would be to add type annotations directly in the PlusCal code. As reported in Issue 1412, this does not work as expected, as the PlusCal translator erases the comments.
A simple solution is to add type annotations directly to the declarations in
the generated TLA+ code. However, this solution is fragile. If we change the
PlusCal code, our annotations will get overridden. We propose another solution
that is stable under modification of the PlusCal code. To this end, we
introduce a new module called BakeryTyped.tla
with the following contents:
 MODULE BakeryTyped 
CONSTANT
\* @type: Int;
N
VARIABLES
\* @type: Int > Int;
num,
\* @type: Int > Bool;
flag,
\* @type: Int > Str;
pc,
\* @type: Int > Set(Int);
unchecked,
\* @type: Int > Int;
max,
\* @type: Int > Int;
nxt
ConstInit4 ==
N = 4
INSTANCE BakeryWoTlaps
==============================================================================
Due to the semantics of INSTANCE
, the constants and variables declared in
BakeryTyped.tla
substitute the constants and variables of
BakeryWoTlaps.tla
. By doing so we effectively introduce type annotations.
Since we introduce a separate module, any changes in the PlusCal code do not
affect our type annotations.
Additionally, we add a constant initializer ConstInit4
, which we will use
later. See the manual section about the ConstInit predicate for a detailed
explanation.
Step 2: Annotate the operator \prec
Let us run the type checker against BakeryTyped.tla
:
$ apalachemc typecheck BakeryTyped.tla
...
[BakeryWoTlaps.tla:66:1766:20]: Cannot apply a to the argument 1 in a[1].
...
The type checker complains about types of a
and b
in the operator \prec
:
a \prec b == \/ a[1] < b[1]
\/ (a[1] = b[1]) /\ (a[2] < b[2])
The issue is that the type checker is not able to decide whether a
and b
are functions, sequences, or tuples. We help the type checker by adding type
annotations to the operator \preceq
.
\* A type annotation introduced for Apalache:
\*
\* @type: (<<Int, Int>>, <<Int, Int>>) => Bool;
a \prec b == \/ a[1] < b[1]
\/ (a[1] = b[1]) /\ (a[2] < b[2])
When we run the type checker once again, it computes all types without any problem:
$ apalachemc typecheck BakeryTyped.tla
...
Type checker [OK]
Note that our annotation of \preceq
would not get overwritten, when we update
the PlusCal code. This is because \preceq
is defined in the TLA+ section.
Step 3: Checking mutual exclusion for bounded executions
Once we have annotations, we run Apalache to check the property of mutual exclusion for four processes and executions of length up to 10 steps:
$ apalachemc apalachemc check \
cinit=ConstInit4 inv=MutualExclusion BakeryTyped.tla
...
It took me 0 days 0 hours 32 min 2 sec
Apalache reports no violation of MutualExclusion
. This is a good start.
However, since Apalache only analyzes executions that make up to 10
transitions by default, this analysis is incomplete.
Step 4: Checking mutual exclusion for unbounded executions
To analyze executions of arbitrary length with Apalache, we can check an inductive invariant. For details, see the section on Checking inductive invariants. The Bakery specification contains such an invariant written by Leslie Lamport:
(***************************************************************************)
(* Inv is the complete inductive invariant. *)
(***************************************************************************)
Inv == /\ TypeOK
/\ \A i \in Procs :
/\ (pc[i] \in {"e4", "w1", "w2", "cs"}) => (num[i] # 0)
/\ (pc[i] \in {"e2", "e3"}) => flag[i]
/\ (pc[i] = "w2") => (nxt[i] # i)
/\ pc[i] \in {(*"e2",*) "w1", "w2"} => i \notin unchecked[i]
/\ (pc[i] \in {"w1", "w2"}) =>
\A j \in (Procs \ unchecked[i]) \ {i} : Before(i, j)
/\ /\ (pc[i] = "w2")
/\ \/ (pc[nxt[i]] = "e2") /\ (i \notin unchecked[nxt[i]])
\/ pc[nxt[i]] = "e3"
=> max[nxt[i]] >= num[i]
/\ (pc[i] = "cs") => \A j \in Procs \ {i} : Before(i, j)

To prove that Inv
is an inductive invariant for N = 4
, we run Apalache
twice. First, we check that the initial states satisfy the invariant Inv
:
$ apalachemc apalachemc check cinit=ConstInit4 \
init=Init inv=Inv length=0 BakeryTyped.tla
...
The outcome is: NoError
It took me 0 days 0 hours 0 min 6 sec
Second, we check that for every state that satisfies Inv
, the following
holds true: Its successors via Next
satisfy Inv
too. This is done as
follows:
$ apalachemc apalachemc check cinit=ConstInit4 \
init=Inv inv=Inv length=1 BakeryTyped.tla
...
The outcome is: NoError
It took me 0 days 0 hours 0 min 28 sec
Now we know that Inv
is indeed an inductive invariant. Hence, we check
the property MutualExclusion
against the states that satisfy Inv
:
$ apalachemc apalachemc check cinit=ConstInit4 \
init=Inv inv=MutualExclusion length=0 BakeryTyped.tla
...
The outcome is: NoError
It took me 0 days 0 hours 0 min 9 sec
In particular, these three results allow us to conclude that MutualExclusion
holds for all states that are reachable from the initial states (satisfying
Init
) via the available transitions (satisfying Next
). Since we have fixed
the constant N
with the predicate ConstInit4
, this result holds true for N = 4
. If you want to check MutualExclusion
for other values of N
, you can
define a predicate similar to ConstInit4
. We cannot check the invariant for
all values of N
, as this would require Apalache to reason about unbounded
sets and functions, which is currently not supported.
Dealing with the define block
PlusCal specifications may contain the special defineblock. For example:
 MODULE CountersPluscal 
(*
Pluscal code inside TLA+ code.
algorithm Counters {
variable x = 0;
define {
\* This is TLA+ code inside the PlusCal code.
IsPositive(x) == x > 0
}
...
}
*)
================================
Unfortunately, the PlusCal transpiler erases comments when translating PlusCal code to TLA+. Hence, the simplest solution is to move the defineblock outside the PlusCal code. For example:
 MODULE CountersPluscal 
\* @type: Int => Bool;
IsPositive(x) == x > 0
(*
algorithm Counters {
variable x = 0;
...
}
*)
================================
Conclusion
The final specifications can be found in BakeryTyped.tla and BakeryWoTlaps.tla.
In this tutorial we have shown how to:
 Annotate a PlusCal spec with types by introducing an additional TLA+ module.
 Check safety of Bakery for bounded executions by bounded model checking (for
N=4
).  Check safety of Bakery for unbounded executions by invariant checking (for
N=4
).
If you are experiencing a problem with Apalache, feel free to open an issue or drop us a message on Zulip chat.
Further reading
 Entrylevel Tutorial on the Model Checker
 Tutorial on Snowcat shows how to write type annotations for Apalache.
 TLA+ Cheatsheet in HTML summarizes the common TLA+ constructs. If you prefer a printable version in pdf, check the Summary of TLA+.