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 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.

\includegraphics[width=7mm]{img/info_64.png}

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.

\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: