Writing Lines Of Code

It is easy to convince ourselves of the correctness of our toy spec. We can see that from the initial state, the light turns green, then yellow, then red, then green again, and so on. What do these states share in common? What is something that is true for all them?

For our traffic light to function correctly, only one light can be on at a time. In the spec, this requirement translates into allowing only one of the variables to be set to 1; the other two must be set to zero. We can partially capture this by defining OnlyOneLightOn as the state predicate cheking if the sum of the variables is equal to one:

OnlyOneLightOn == red + yellow + green = 1

OnlyOneLightOn can be true with variables having values different from 0 and 1. For instance, it would be true if red = -2, yellow = 4, and green = -1. To ensure that our variables can only take the values of 0 or 1, we can define TypeOk as:

TypeOk == /\ red \in {0,1}
          /\ yellow \in {0,1}
          /\ green \in {0,1}

TypeOk checks that red, yellow and green are in the set of numbers containing only 0 and 1. In TLA+, sets are written using curly brackets (e.g., {0, 1}). \in is used to determine if an element is in a set.

This is a good time to bring up that TLA+ is not a typed language. You might remember from a prior post that there is nothing constraining what values variables can take on. So to ensure that variables take only values of specific types you always need to define an equivalent of TypeOk.

Below is an updated specification incorporating OnlyOneLightOn and TypeOk:

---------------------------- MODULE TrafficLight ----------------------------

EXTENDS Naturals

VARIABLES red, yellow, green

TypeOk == /\ red \in {0,1}
          /\ yellow \in {0,1}
          /\ green \in {0,1}
          
OnlyOneLightOn == red + yellow + green = 1

Init == /\ TypeOk
        /\ OnlyOneLightOn

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

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

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

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

Spec == Init /\ [][Next]_<<red, yellow, green>>


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

A few things to note in the updated spec:

EXTENDS Naturals was added to line 3. This is because we are using addition in the defintion of OnlyOneLightOn. Addition is defined in the module Naturals.
The definition of Init has changed. In the previous version, our behavior started from a red light (red = 1, yellow = 0, green = 0). Now behaviors can start from any state where TypeOk and OnlyOneLightOn are both true.

This is a state graph of our algorithm:

state graph

One important question remains: where are we checking that OnlyOneLightOn is an invariant? I will address this question in a post about TLC, the model checker for TLA+ specifications. I will also show how to use TLC to generate state graphs like the one above.