Modeling a traffic light - Part 3: Specification

In this post we are going to write a specification for a traffic light.

The goal of a specifiation is to define which behaviors describe a properly working system. To do that, a specification has two key components: an initial state, and something describing how to transition from one state to another.

Before getting started with the specification, let's recall from prior posts that in TLA+

• a state is an assignment of values to variables, and
• a behavior is an infinite sequence of states.

We are going to define the traffic light's state in terms of three variables: red, yellow and green. Their values can be either 1 (on), or 0 (off).

There are three valid initial states where only one of the lights is on.

Thre are also three ways that the traffic light can change state:

• Turn green: If red is on, and both green and yellow are off then turn green on, red off, and keep yellow off.
• Turn yellow: If green is on, and both red and yellow are off then turn yellow on, green off, and keep red off.
• Turn red: If yellow is on, and both red and green are off then turn red on, yellow off, and keep green off.

For our specification we can say that:

• The initial state is when the light is red. (red = 1, yellow = 0, green = 0)
• We can transition to another state by either turning green, or turning yellow, or turning red.

Below is what this might look like in TLA+

---- MODULE TrafficLight ----

VARIABLES red, yellow, green

Init == /\ red = 1 
        /\ yellow = 0 
        /\ green = 0

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

====

Let's look into the TLA+ syntax to better understand the spec.

• /\ represents the logical operator AND
• \/ represents OR
• [] is a temporal-logic operator indicating that Next is always true.

Indentation in TLA+ matters. Notice how in Init all the ANDs are lined up.

Also notice how TurnGreen, TurnYellow, and TurnRed follow the same pattern:

• The first line acts as a guard. Prior to turning green, red has to be on AND yellow has to be off AND green has to be off.
• The following two lines have primed variables (e.g., red'). These indicate the expected values for those variables in the next state.
• The last line is for explicitly calling out the variable that remains unchanged.

Finally, in line 28, we can see the Spec defined in terms of Init (defining the initial state) and Next (determining valid transition between states).