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.

We provide all source files referenced in this tutorial as a ZIP archive download. We still recommend that you follow along typing the TLA+ examples yourself.

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 modules

  EXTENDS 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:

$ apalache-mc 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:

$ apalache-mc typecheck BakeryTyped.tla
...
[BakeryWoTlaps.tla:66:17-66: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:

$ apalache-mc 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:

$ apalache-mc apalache-mc 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:

$ apalache-mc apalache-mc 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:

$ apalache-mc apalache-mc 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:

$ apalache-mc apalache-mc 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 define-block. 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 define-block 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

• Entry-level 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+.