add the missing constraints

During the exploration of the possible states we observed the following invalid states:

• C7: when [ yellow.flashing ], both red and green lamps can be on, which should not be allowed.
• C8: when [ red.flashing ], both yellow and green lamps can be on, which should not be allowed
• C9: when [ green.flashing ], only [ red.on || red.off] should be allowed
• C10: when [ advancedOrExtendedLeft.leftSignalType.leftArrow ] is used, [green.flashing] should not be allowed
• C11: when [ redAndYellowToGreen ] is used, the only two lamps that can be on at the same time are red and yellow, otherwise, at most one light can be on or flashing.

Let’s specify the missing constraints and check the possible states again.

The constraint C11 means that either at most one light is on at any given moment unless redAndYellowToGreen is used then both red and yellow can be on at the same time.

Let’s inspect the states assuming

We want to see whether it’s still possible to have both red and green lamps on at the same time.

As we can see, despite adding many constraints we still have not restricted the state space properly. Furthermore, the domain knowledge is completely lost in these constraints, as they do not correspond to what the traffic light should achieve. What we are missing, is that a traffic light is there to communicate a particular set of signals, which carry particular semantics.

Let’s add the traffic light signals which in turn determine the state of the lamps.

1. control software
2. lamp abstraction
3. valid states