2.4.4 Building the Model

Back to the problem: Our objective is to build a simplified traffic light controller as described in 2.4. We start with the model state. Two traffic lights will be modelled, and we will therefore create two variables called cars_go and peds_go.

2.4.4.1 Creating Variables

Under the MACHINE heading, you see the machine name mac. There is a small green arrow ( ) to the right of this label. Place your cursor directly to the left of the green arrow, right click, and select Add Child Event-B Variable to add a new variable. Optionally, you can also use the New Variable Wizard (the button ) to create your variable.

By default, the variable is named var1. Place your cursor inside the var1 label. The label will then turn into a textbox. Change the name to cars_go. You can add a comment to the variable by placing your cursor to the right of the little green arrow and typing into the text box that appears.

Comments: The comment field does not support line breaks, nor is is possible to “comment out” parts of the model as it is with most programming languages.

Create the second variable (peds_go) in the same way, or place your cursor directly to the left of the small green arrow next to the label cars_go and hit either CTRL-T or right click and select Add Sibling from the menu.

Upon saving, the variables will be underlined in red which indicates that an error is present as shown in Figure 2.7. The Rodin Problems view (3.1.2.5) shows corresponding error messages. In this case, the error message is “Variable cars_go does not have a type”.

Figure 2.7: Red highlighted elements indicate errors

Invariants are needed in order to specify the type of variables. Use the method described above to add invariants to your machine (except this time select Add Child Event-B Invariant from the menu or click the button to open up the New Invariant Wizard). Add two invariants (which will automatically be labelled inv1 and inv2). The actual invariant appears to the left of the label and is prepopulated with the symbol , which represents the logical value “true”. Placing your cursor inside the invariant field will change it to a text field and allow editing.

Change the first invariant (the symbol , not the label inv1) to and the second invariant to . Event-B provides the build-in datatype BOOL among others (3.3.1.1).

Mathematical Symbols: Every mathematical symbol has an ASCII-representation and the substitution occurs automatically. To generate “element of” (), simply type a colon (“:”). The editor will perform the substitution after a short delay. The Symbols view shows all supported mathematical symbols. The ASCII representation of a symbol can be found by hovering over the symbol in question. Symbols can also be added manually by selecting them from the Symbols view

After saving, you should see that the INITIALISATION event is underlined in yellow with a small warning sign to the left as demonstrated in Figure 2.8. Again, the Rodin Problems view displays the error message: “Variable cars_go is not initialized”. Every variable must be initialized in a way that is consistent with the model.

Figure 2.8: Yellow highlighted elements indicate warnings

To fix this problem, place your cursor to the left of the small green arrow next to the label INITIALISATION. Right click and add an Event-B Action. Repeat to add another event. In the action fields, enter and .

2.4.4.2 State Transitions with Events

Our traffic light controller cannot yet change its state. To make this possible, we create two events (3.2.4.4) in the manner described above and name them set_peds_go and set_peds_stop. This will model the traffic light for the pedestrians, and for each of these, we will add an Event-B action to each of the events. These actions will change peds_go to TRUE or FALSE, which simulates the changing of the traffic light.

From now on, we won’t describe the individual steps in the editor any more. Instead, we will simply show the resulting model.

The two events will look as follows:

Event

set_peds_go

begin

end

Event

set_peds_stop

begin

end

Within Camille this part of the model has a different textual representation. For example, the first event has to be written as follows:

event

set_peds_go

begin

end

From now on, we won’t describe the differences between the Rodin editor and Camille any more.

This contribution requires the Camille plugin. The content is maintained by the plugin contributors and may be out of date.

2.4.4.3 Event parameters

For the traffic light for the cars, we present a different approach and use only one event with a parameter. The event will use the new traffic light state as the argument. For this, we need to add an Event-B Event Parameter, which will appear under the heading ANY, and an Event-B Guard, which will appear under the heading WHERE:

Event

set_cars

any

where

then

end

Note how the parameter is used in the action block to set the new state.

2.4.4.4 Invariants

If this model was actually in control of a traffic light, we would have a problem because nothing is preventing the model from setting both traffic lights to TRUE. The reason is that so far we only modeled the domain (the traffic lights and their states) and not the requirements. We have the following safety requirement:

We can model this requirement with the following invariant:

Please add this invariant with the label inv3 to the model (Use the ASCII codes not and & to get the symbols and ).

Obviously, this invariant can be violated, and Rodin informs us of this. The Event-B Explorer (3.1.2.7) provides this information in various ways. Go to the explorer and expand the project (tutorial-03), the machine (mac) and the entry “Proof Obligations”. You should see four proof obligations, two of which are discharged (marked with ) and two of which are not discharged (marked with ).

Proof obligations: A proof obligation is something that has to be proven to show the consistency of the machine, the correctness of theorems, etc. A proof obligation consists of a label, a number of hypothesis that can be used in the proof and a goal – a predicate that must be proven. Have a look at the proof obligation labels. They indicate the origin in the model where they were generated. E.g. set_peds_go/inv3/INV is the proof obligation that must be verified to show that the event set_peds_go preserves the invariant (INV) with the label inv3. An overview about all labels can be found in Section 3.2.7. The proof obligations can also be found via other entries in the explorer, like the events they belong to. Elements that have non-discharged proof obligations as children are marked with a small question mark. For instance, inv3 has all proof obligations as children, while the event set_cars has one.

To prevent the invariant from being violated (and therefore to allow all proof obligations to be discharged), we need to strengthen the guards (3.2.4.4.2) of the events.

Before looking at the solution, try to fix the model yourself.

2.4.4.5 Finding Invariant Violations with ProB

A useful tool for understanding and debugging a model is a model checker like ProB. You can install ProB directly from Rodin by using the ProB Update Site. Just select Install New Software... from the Help menu and select “ProB” from the dropdown. You should see “ProB for Rodin2“ as an installation option, which you can then install using the normal Eclipse mechanism.

We will continue the example at the point where we added the safety invariant (REQ-1), but didn’t add guards yet to prevent the invariants from being violated.

We launch ProB by right-clicking on the machine we’d like to animate and select Start Animation / Model Checking. Rodin will switch to the ProB-Perspective, as shown in Figure 2.9. The top left pane shows the available events of the machines. Upon starting, only INITIALISATION is enabled. The middle pane shows the current state of the machine, and the right pane shows a history. On the bottom of the main pane we can see whether any errors occurred, like invariant violations. We can now interact with the model by triggering events. This is done by double-clicking on an enabled event or by right-clicking it and selecting a set of parameters, if applicable. We first trigger INITIALISATION. After that, all events are enabled. Next, we trigger set_cars and set_peds_go with the parameter . As expected, we will get an invariant violation. In the state view, we can “drill down” and find out which invariant was violated, and the history view shows us how we reached this state (Figure 2.10). After modifying a machine, ProB has to be restarted, which is done again by right-clicking the machine and selecting ProB. Triggering events to find invariant violations is not very efficient. But ProB can perform model checking automatically. To do so, select Model Checking from the Checks menu from the “Events” View (the view on the left). After optionally adjusting some parameters, the model checking can be triggered by pressing “Start Consistency Checking". Upon completion, the result of the check is shown. ProB has many more functions and also supports additional formalisms. Please visit the ProB Website for more information.

This contribution requires the ProB plugin. The content is maintained by the plugin contributors and may be out of date.

Figure 2.9: The ProB Perspective

Figure 2.10: An invariant violation, found by ProB