3.1.5 The Structural Event-B Editor

The editor described here was the default editor until Rodin 2.3. It is still available. To use this editor, right click on a machine or context file in the Event-B Explorer and select Open With Event-B Machine Editor.

Once a context or a machine is created, a window appears in the editing area as shown in Figure 3.12.

Figure 3.12: The Structured Event-B editor

By default, you are in Edit mode which allows you to edit the modelling elements of the context (the dependencies, the carrier sets, the constants, and the axioms). By right-clicking on the modelling elements you can create new child and sibling elements. For instance, by pressing the triangle ( ) next to each keyword, you can see the different modelling elements and also add, remove, or move them. Figure 3.13 shows what the section looks like after pressing the triangle next to the keyword "AXIOMS".

Figure 3.13: By pressing the triangle you can collapse/expand context sections

By pressing the button, you can add a new modelling element. For instance, clicking on the button in the AXIOMS section will add a new axiom element. You can now enter a new axiom and a comment in the corresponding boxes as indicated in Figure 3.14.

Figure 3.14: Adding a new modelling element

To remove a modelling element, press the button. You can also move an modelling element up or down by selecting it and then pressing one of the two arrows ( or ).

3.1.5.1 Dependencies (Context)

By selecting the Dependencies tab at the bottom of the Event-B editor, you obtain the window shown in Figure 3.15.

Figure 3.15: Dependencies tab of the Event-B editor

The dependencies tab allows you to control the other contexts that the current context extends. To add the context that you want to extend, select the name of the context from the drop-down menu at the bottom of the window and then hit the Add button.

There is also another way to create a new context as an extension existing one. Select the context in the project window and then press the right mouse key. Then select Extend from the menu that opens up. This should bring up the window as shown in Figure 3.16.

Figure 3.16: New EXTENDS Clause window

You can then enter the name of the new context which will automatically extend your chosen context.

3.1.5.2 Dependencies (Machine)

The Dependencies tab for machines is very similar to the one for contexts that is described in the previous section. The main difference is that there are two kinds of dependencies that can be established: machines on which the current machine depends are listed in the upper part and contexts on which the current machine depends are listed in the lower part.

3.1.5.3 Synthesis (Context)

Selecting the Synthesis tab brings up a global view of your context’s elements (carrier set / constant / axiom / extended context) as demonstrated in Figure 3.17.

Figure 3.17: The Synthesis tab of the Event-B editor

By pressing the set, cst, or axm buttons in the upper right corner, you can filter out the carrier sets, constants or axioms of your context respectively.

If you select an element, you can change its priority by pressing the button or the button. You do this for axioms, carrier sets, constants and extended contexts.

Right clicking in this view will bring up a context menu that allows you to add a new carrier set, constant, axiom or extended context.

3.1.5.4 Synthesis (Machine)

The Synthesis tab for machines is very similar to the one of contexts (see above) except that you have a global view of your machine’s elements (refined machines, seen contexts, variables, invariants, events, and variants).

3.1.5.5 Pretty Print

Selecting the Pretty Print tab gives you a global view of your context or machine as if it had been entered through with an input text file as seen in Figure 3.18.

Figure 3.18: The Pretty Print tab of the Event-B editor