PlusCal

In the series of posts about TLA+ we completed a specification for a traffic light. If we were to stop there, it would be hard to see the benefits of writing specifications. The code was simple enough that we could convince ourselves of its correctness.

Where TLA+ shines is when we have to think about concurrency. What is concurrency? Concurrency is a way of solving problems by breaking them into tasks that can be executed in different orders. Imagine that we have a single vending machine and 20 customers to serve. We can line up the customers into a single queue. Or we can line them up into two queues, and have yet more options: we can alternate between the queues, having a customer from queue A use the machine, then a customer from queue B, and so on. Or we can let queue A go, and then queue B.

Because there are so many options, reasoning about concurrency can be very hard. Testing may not be enough to convince us that the program is behaving as we expect. For example, there may be flaky tests that sporadically fail, and we don't know why.

To reason about concurrency, then, we need proper tooling. To facilate the use of TLA+, this post will introduce PlusCal. PlusCal is a language to write algorithms that gets translated into TLA+. Some of the advantages of using PlusCal are:

• Because it resembles more common programming languages, it is easier to work with. It is also easier to share our specifications with others that may not be familiar with TLA+.
• Once we have a specification, it becomes easier to translate that specification into the language that we are actually working with.

To become familiar with the language, let's look at a version of our traffic light specification in PlusCal¹:

------------------------ MODULE PlusCalTrafficLight ------------------------

EXTENDS Naturals

(*

--algorithm PlusCalTrafficLight
{
    variables red = 1, yellow = 0, green = 0;
    {
        TurnGreen: if (red = 1 /\ yellow = 0 /\ green = 0) 
        {
            red := 0;
            green := 1;
        };
        
        TurnYellow: if (red = 0 /\ yellow = 0 /\ green = 1)
        {
            green := 0;
            yellow := 1;
        };
        
        TurnRed: if (red = 0 /\ yellow = 1 /\ green = 0)
        {
            red := 1;
            yellow := 0;
        };
    }
}

*)

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

The PlusCal algorithm appears between the delimeters (* (on line 5) and *) (on line 31). It starts with --algorithm PlusCalTrafficLight and is contained between two curly brackets (lines 32 and 53).

In line 9, we see the algorithm's variables declared. In lines 11, 17, and 23, we see three if statements that are preceeded by the labels TurnGreen, TurnYellow, and TurnRed. These labels indicate that everything related to the label should happen in one step.

Finally, in PlusCal assignment is done using :=. Lines 25 and 26 are examples.

When translating the PlusCal algorithm into TLA+, we get a spec similar to ours starting on line 33. The start and end of the translation are marked with comments (see lines 32 and 80). We don't want to make any modifications between these lines as they will get removed if we regenerate the translation.

------------------------ MODULE PlusCalTrafficLight ------------------------

EXTENDS Naturals

(*

--algorithm PlusCalTrafficLight
{
    variables red = 1, yellow = 0, green = 0;
    {
        TurnGreen: if (red = 1 /\ yellow = 0 /\ green = 0) 
        {
            red := 0;
            green := 1;
        };
        
        TurnYellow: if (red = 0 /\ yellow = 0 /\ green = 1)
        {
            green := 0;
            yellow := 1;
        };
        
        TurnRed: if (red = 0 /\ yellow = 1 /\ green = 0)
        {
            red := 1;
            yellow := 0;
        };
    }
}

*)
\* BEGIN TRANSLATION (chksum(pcal) = "9f6aa7a3" /\ chksum(tla) = "c9d59226")
VARIABLES red, yellow, green, pc

vars == << red, yellow, green, pc >>

Init == (* Global variables *)
        /\ red = 1
        /\ yellow = 0
        /\ green = 0
        /\ pc = "TurnGreen"

TurnGreen == /\ pc = "TurnGreen"
             /\ IF red = 1 /\ yellow = 0 /\ green = 0
                   THEN /\ red' = 0
                        /\ green' = 1
                   ELSE /\ TRUE
                        /\ UNCHANGED << red, green >>
             /\ pc' = "TurnYellow"
             /\ UNCHANGED yellow

TurnYellow == /\ pc = "TurnYellow"
              /\ IF red = 0 /\ yellow = 0 /\ green = 1
                    THEN /\ green' = 0
                         /\ yellow' = 1
                    ELSE /\ TRUE
                         /\ UNCHANGED << yellow, green >>
              /\ pc' = "TurnRed"
              /\ red' = red

TurnRed == /\ pc = "TurnRed"
           /\ IF red = 0 /\ yellow = 1 /\ green = 0
                 THEN /\ red' = 1
                      /\ yellow' = 0
                 ELSE /\ TRUE
                      /\ UNCHANGED << red, yellow >>
           /\ pc' = "Done"
           /\ green' = green

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == TurnGreen \/ TurnYellow \/ TurnRed
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION 

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

For comparison, this is what TurnGreen looked like in our spec:

TurnGreen == /\ red = 1 /\ yellow = 0 /\ green = 0
             /\ red' = 0
             /\ green' = 1
             /\ UNCHANGED yellow

Additional resources

There are a number of resources available to learn more about PlusCal. Leslie Lamport, the creator of both TLA+ and PlusCal, has a fantastic tutorial: https://lamport.azurewebsites.net/tla/tutorial/intro.html

Stephan Merz, an active member of the TLA+ community, has a handy cheat sheet: https://github.com/tlaplus/PlusCalCheatSheet

Finally, Hillel Wayne has site (https://www.learntla.com) as well as a book (https://www.goodreads.com/book/show/42389860-practical-tla) devoted to PlusCal and TLA+.