2.4 The First Machine: A Traffic Light Controller

Goals: The objective of this section is to get acquainted with the modelling environment. We will create a very simple model consisting of just one file to develop a feeling for Rodin and Event-B.

In this tutorial, we will create a model of a traffic light controller. We will use this example repeatedly in subsequent sections. Figure 2.4 depicts what we are trying to achieve.

There is a four-page Event-B Cheat Sheet, representing a concise summary of the Event-B mathematical toolkit. Thanks to Ken Robinson for making it available.

Figure 2.4: The traffic light controller

In this section, we will implement a simplified controller with the following characteristics:

• We will model the signals with Boolean values to indicate “stop” (false) and “go” (true). We do not model colors (yet) because we think we should first specify our goal (regulating the traffic) and later add implementation details (the traffic light’s colors).

• To keep the initial model simple, we will not include the push button yet. We will add it later.