Rodin User’s Handbook v.2.8: Fixing Problems

2.9.3 Fixing Problems

Before proceeding, we will fix the problems shown in Figure 2.16. Let’s take a look at the warning stating that the event label “celebrity” is misused (“Inconsistent use of event label celebrity”). Double-click on this warning to open the Celebrity_1 machine. The line with the error is already underlined in yellow¹. This error is produced by the event called celebrity.

The problem is that the event is not declared as a refinement. To solve the problem, add an Event-B Refines Event Relationship child which will add a new entry in the REFINES section. To do so, right-click in the empty space to the left of the word celebrity or place your cursor directly to the left of the small green arrow ( $\includegraphics[height=2ex]{img/icons/rodin/structured_arrow.png}$ ) and right-click. Now select Add Child $\rangle$ Event-B Refines Event Relationship.

$\includegraphics[width=7mm]{img/warning_64.png}$
Make sure that the cursor is on the correct line before right-clicking. Otherwise, you will get the wrong context menu. Also, make sure that you are not in “text edit” mode (e.g. clicking on a word like “celebrity” that you can edit will bring you into “text edit” mode). This will give you the wrong context menu as well. See the FAQ for more info (4.3.12).

This declares that the event is a refinement of an event with the same name in the abstract machine (3.2.4.1). This is the case here, so we can now save the project and the warning should disappear.

The three remaining warnings state that witnesses (3.2.4.4.4) are missing. Double click on the warning to open the concrete model (here Celebrity_2). Then add an Event-B Witness child to the event called celebrity.

A default witness wit1 has been created, with a default value $\mathord {\top }$ (e.g. the predicate “true”) which we need to change. The name of a witness has to be the same as the parameter of the corresponding abstract event that it is refining. Here the name of the witness will have to be x so that it can be a witness for the parameter x of the corresponding abstract event in the machine Celebrity_1. The abstract event has the assignment $r \mathrel {:\mkern 1mu=}x$ , while the concrete one has the assignment $r \mathrel {:\mkern 1mu=}b$ . So the content of the witness should b = x. The event should now look as follows:

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

Event

celebrity $\mathrel {\widehat=}$

refines

celebrity

when

$\tt grd1 :$

$\it R = \emptyset$

with

$\tt x :$

$\tt b=x$

then

$\tt act1 :$

$\it r := b$

end

Edit the content and save the file. One warning will disappear, and only two will remain.

$\includegraphics[width=7mm]{img/info_64.png}$
Try completing the other two witnesses on your own. A hint: Both witnesses are simple equalities, and both can be found by comparing the third guard of the abstract event with the second guard of the concrete one. Remember to give the witness the name of the variable it stands for. If you completed this step correctly, there should be no warning, info or error left in the Rodin Problems view (3.1.2.5).

The following section (2.9.4) shows the corrected Celebrity_2 machine.

Footnotes

This is the behaviour of the default editor. Other editors may exhibit a different behaviour

Rodin Handbook

2.9.3 Fixing Problems