User Manual for Rodin v.2.3: Building the Model

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

Go to the Edit tab in the editor and expand the VARIABLES section. Click on the $\includegraphics[height=2ex]{img/icons/rodin/add.png}$ button to create a new variable. You will see two fields. The left one is filled with the word var1. Change this to cars_go. The second field (after the double-slash “//”) is a comment field in which you can write any necessary notes or explanations.

$\includegraphics[width=7mm]{img/info_64.png}$
Comments: The comment field supports line breaks. Note that it is not possible to “comment out” parts of the model, as is possible with most programming languages. You can use the comment field to “park” predicates and other strings temporarily.

Create the second variable (peds_go) in the same way.

Upon saving, the variables will be highlighted in red, indicating an error 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”.

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

Figure 2.7: Red highlighted elements indicate errors

Types are provided by invariants. Expand the INVARIANTS section and add two elements by following the same steps as above. Invariants have labels. Default labels are generated (inv1 and inv2). The actual invariant is prepopulated with $\mathord {\top }$ , which represents the logical value “true”. Change the first invariant (the $\mathord {\top }$ , not the label inv1) to $cars\_ go \in BOOL$ and the second invariant to $peds\_ go \in BOOL$ . Event-B provides the build-in datatype BOOL amongst others (3.3.1.1).

$\includegraphics[width=7mm]{img/info_64.png}$
Mathematical Symbols: Every mathematical symbol has an ASCII-representation and the substitution occurs automatically. To generate “element of” ( $\in$ ), 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.

After saving, you should see that the EVENTS section is highlighted in yellow as demonstrated in Figure 2.8. Again, the Rodin Problems view gives us the error message: “Variable cars_go is not initialized”. Every variable must be initialized in a way that is consistent with the model.

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

Figure 2.8: Yellow highlighted elements indicate warnings

To fix this problem, expand the EVENTS section and then the INITIALIZATION event. Add two elements in the THEN block. These are actions that also have labels. In the action fields, enter $cars\_ go := FALSE$ and $peds\_ go := FALSE$ .

2.4.4.2 State Transitions with Events

Our traffic light controller cannot yet change its state. To make this possible, we create events (3.2.3.4). We will first consider the traffic light for the pedestrians, and we will create two events. One will set it to “go” and one will set it to “stop”.

$\includegraphics[width=7mm]{img/warning_64.png}$
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:

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

Event

set_peds_go $\mathrel {\widehat=}$

begin

$\tt act1 :$

$\it peds\_ go := TRUE$

end

Event

set_peds_stop $\mathrel {\widehat=}$

begin

$\tt act1 :$

$\it peds\_ go := FALSE$

end

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. The parameter is declared in the any section and typed in the where section:

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

Event

set_cars $\mathrel {\widehat=}$

any

$\it new\_ value$

where

$\tt grd1 :$

$\it new\_ value \in BOOL$

then

$\tt act1 :$

$\it cars\_ go := new\_ value$

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:

REQ-1: Both traffic lights must not be TRUE at the same time.

We can model this requirement with the following invariant:

$\lnot (cars\_ go = TRUE \land peds\_ go = TRUE)$

Please add this invariant with the label inv3 to the model, use not and & for $\lnot$ and $\land$ .

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 $\includegraphics[height=2ex]{img/icons/rodin/discharged}$ ) and two of which are not discharged ( $\includegraphics[height=2ex]{img/icons/rodin/pending}$ ).

$\includegraphics[width=7mm]{img/info_64.png}$
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 the event set_peds_go preserves the invariant (INV) with the label inv3. An overview about all labels can be found in 3.2.6. 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.3.4.2) of the events.

$\includegraphics[width=7mm]{img/warning_64.png}$
Before looking at the solution, try to fix the model yourself.

2.4.4.5 Finding Invariant Violations with ProB

$\includegraphics{img/prob.png}$ A useful tool for understanding and debugging a model is a model checker like ProB. You can install ProB from the ProB Update Site, directly from Rodin. 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 INITIALIZATION 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 INITIALIZATION. After that, all events are enabled. Next, we trigger set_cars and set_peds_go with the parameter $TRUE$ . 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 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.