Modeling a traffic light - Part 2: Behavior

In the prior post in the series, we decided to specify the state of a traffic light using three variables to track which lights are on or off. We also defined a step as the transition from one state to another.

In this post we'll introduce the concept of a behavior. A behavior is an infinite sequence of steps.

A behavior capturing how we expect a traffic light is this:

Below is another behavior. It does not match our expectation of a properly functioning traffic light because the second state has both the yellow and green lights on:

Below is yet another behavior. There is nothing constraining what values variables can take on:

In our design, the variable red should only have the value of either 1 or 0. But in the universe of possible behaviors there is nothing preventing that variable from being a string, or a decimal, or the number pi.

Of all behaviors, how can we specify only those that represent a traffic light working correctly?