Model a traffic light with the usual three phases "red", "green", and "yellow".

Add assertions to check the safety property that every red phase is immediately preceded by a yellow phase. You may add auxiliary variables.

Use the variable names red, green, yellow.
