2.8.6 Discussion

Notice that we have used two very different approaches to model the traffic lights for cars and pedestrians. For the pedestrians, we created one event for each state transition. For the cars, we handled all states in one single event.

You will often be confronted with situations where many modelling approaches are possible. You should consider two main factors when modelling: (1) the readability of the model and (2) the ease of the proof. In this case, both approaches are equally good (although we wouldn’t recommend mixing different approaches in one model. We did it here only to demonstrate both approaches).

We will cover deadlocks later in Section 2.10.1. If you are interested in the topic, it may interest you to examine the traffic light model for deadlocks. Consider cars_colours = { green, red }. This is a legal state, but it would block set_cars_colours forever. A model checker (such as ProB) could find it. In this case, however, this is not a problem because with the given initialisation and events this state is not reachable in the first place.

We hope that this section helped you to understand the power of abstraction. The safety invariant from Section 2.4.4.4 was very simple. We could now introduce colours because we are confident that the invariant will still be valid (assuming, of course, that our gluing invariant is correct).