2.8.3 The Actual Data Refinement

The easiest way to create a refinement is by right-clicking on the machine in the project browser and selecting Refine (in this case, we will be refining the machine mac from the project tutorial-3). This will create a “stub” consisting of all variables and events. Please use this method to create a machine with name mac1.

When you have refined a machine, the Rodin Editor will show you all the elements of the abstracted machine, but the inherited actions will be shown in grey. This means that you can add actions to the event, but you cannot edit the actions that are already there.

For this tutorial, make sure that you right-click on the machine and select refine from the drop-down menu. If you have created a machine the normal way and later edited the refines section, the tutorial will assume that you have events (e.g. set_peds_go) and variables that you do not have.

First we have to make the machine aware of the context by adding a sees (3.2.4.2) statement. To do this, place your cursor to the left of the small green arrow ( ) next to your machine name mac1. Right click and select Add Child Event-B Sees Context Relationship. A SEES heading will appear with the value –undefined–. Place your cursor over the undefined section and click. A small box listing all of the contexts in the project will pop up. Select ctx1:

MACHINE

mac1

REFINES

mac

SEES

ctx1

We will start with the traffic lights for the pedestrians. It has only two colours (red and green) and only one of them is shown at a time. We introduce a new variable called peds_colour to represent which of the lights is shown. The variable has a corresponding invariant and initialisation (the changes are shown in the following code snippet). The extended keyword in the initialisation means that all actions from the refined initialisation are copied:

VARIABLES

INVARIANTS

EVENTS

Initialisation

extended

begin

end

END

Next, we will create a gluing invariant (3.2.4.1) that associates peds_go from the abstract machine with the variable peds_colour that we just created. The gluing invariant will map TRUE to green and FALSE to red:

INVARIANTS

In its current state, this gluing invariant can be violated: if the event set_peds_go is triggered, for instance, the variable peds_go will change but peds_colour will not. We expect that this will result in undischarged proof obligations (3.2.7). We can check this by expanding the machine in the Event-B Explorer. Indeed, we now see two undischarged proof obligations (compare with Figure 2.14).

Figure 2.14: Mapping between Abstract and Concrete Events

To fix this, we have to modify the two events in question. Let’s start with set_peds_go. First, we change the event from extended to not extended in the Editor by placing our cursor over the keyword extended and clicking. This is shown in Figure 2.15.

Figure 2.15: Switch from extended to not extended

This change will copy the guard and action from the abstract machine, so that we can modify it. We can now replace the action with the corresponding action regarding peds_colour (replacing peds_go := true with peds_colour := green). While we are at it, we can also rename the name of the event to something more fitting (e.g. set_peds_green).

Next, we perform the corresponding change on set_peds_stop (change the action to peds_colour := red and rename the event set_peds_red). Lastly, the event set_cars also contains a reference to peds_go that must be replaced (in the second guard, replace peds_go = FALSE with peds_colour = red).

Once all references to peds_go have been replace, we can remove the variable peds_go from the VARIABLES section. You will also need to change the INITIALISATION event to not extended and remove the action which initialises the variable peds_go. Now you shouldn’t have any errors or warnings, and all proof obligations should be discharged.

If you get the error message “Identifier peds_go has not been declared”, then there are references to the refined variable left somewhere in the model.