valid states

Our current model allows many invalid states. Some of them are obvious, such as, when all lights are on or flashing, others are more subtle and depend on particular variants, such as the green light cannot be flashing when the left green arrow is used. In Clafer, we can use the constraints to prohibit certain states or formulate state invariants. We cannot write temporal constraints or state transitions in the current version of the language (there’s; however, ongoing work on the topic).

Given our domain knowledge, let’s first formulate which states are invalid:

• C1: we cannot have all lamps on, off, or flashing at the same time.
• C2: we cannot have more than one lamp flashing at a time
• C3: we cannot have an arrow lamp on or flashing together with yellow on or flashing

The following states are valid:

• C4: we should always have one of the main lamps on or flashing
• C5: we can have both red and yellow lamps on but only if redAndYellowToGreen feature is used
• C6: we can only have an arrow lamp on or flashing together with red or green lamps on

Let’s now add these constraints and invariants to our model and see whether we can still get some invalid states.

The quantifier lone means less than or equal to one or there exists at most one.

The remaining constraints must be specified in the context of the TrafficLight.

Let’s inspect the states allowed by our constrained model assuming that redAndYellowToGreen is not chosen first.

In the window Input Clafer Model and Options, add additional constraints to restrict the state space. For example,

• what happens when we require [ yellow.flashing ]?
• can we have both [ red.on && green.on ]?
• what other cases you can think of?

Then change the constraint [ no redAndYellowToGreen ] to [ redAndYellowToGreen ] and see whether it is allowed to have both [ red.on && yellow.on]?

As you can see, our model still allows many states which are not valid. Let’s add the missing constraints.

1. control software
2. lamp abstraction