2.4 The First Machine: A Traffic Light Controller

$\includegraphics[width=7mm]{img/tick_64.png}$
Goals: The objective of this section is to get acquainted with the modeling 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.

$\includegraphics[]{img/tutorial/tut_03_trafficlight.png}$

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 we should add implemtation details (the traffic light’s colors).
Too keep the initial model simple, we will not include the push button yet. We will add it later.

Rodin Handbook

2.4 The First Machine: A Traffic Light Controller