Modeling a traffic light - Part 1: State

This is the first in a series of posts to model a traffic light. The goal is to showcase TLA+ usefulness in modeling software, and along the way, introduce concepts key to the language. One of those key concepts is that of state

In TLA+, a system's state is defined by the assignment of values to variables. A traffic light has three signals: red, yellow, and green. We can say that these are the traffic lights' variables. The values these variables can take are either on or off. We can represent on with a one, and off with a zero.

Thus a traffic light can have three valid states:

• red = 1, yellow = 0, and green = 0 (this is when we say the light is red).
• red = 0, yellow = 1, and green = 0 (this is when we say the light is yellow).
• red = 0, yellow = 0, and green = 1 (this is when we say the light is green).

A traffic light transitions between these three states. These transitions between states are called steps.