2.8.9 Discussion

There are a number of problems associated with the model in its current state. Let’s start with how the button is reset: The way we built our model so far, set_peds_red can be triggered at any time; there is not a single guard which prevents this. Therefore, the button could be reset any time without the pedestrian light ever turning green.

This could be prevented with additional guards. For instance, the traffic light events could require an actual change in the light’s status. This in turn could lead to deadlocks.

But even if we introduce such guards, we could get stuck in a situation where cars would never get green light any more. Consider the following scenario: (1) pedestrians get green light; (2) the light turns red; (3) a pedestrian presses the button again; (4) this prevents the car lights from turning green. Instead, the pedestrians get a green light again and the cycle continues.

There are tactics to address all these issues. However, it is rarely possible to generate proof obligations for such scenarios (without making the model much more complicated). It can be useful to use model checkers to validate the model’s behaviour or even to use temporal logic to articulate properties of the model.

As an exercise, try to improve the model to address these issues.