3.1.4 The Event-B Editor

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

The editor described here was made the default editor in Rodin 2.4 (February 2012) and still has some minor issues (see Section 4.3.12). The alternative structural editor is still available (see Section 3.1.5).

Figure 3.10: The Event-B editor

The editor allows you to edit the modelling elements of the context which are the dependencies, the carrier sets, the constants, and the axioms. By right-clicking in predefined places you can create new modelling elements. For instance, a symbol appears directly to the right of the name of the context (in this case, the name of the context is “ctx"). Place your cursor directly to the left of this symbol and right click. Select the element that you would like to add from the Add Child menu as shown in Figure 3.11.

Machine elements can also be added in the same way.

Figure 3.11: Adding a new modelling element

To remove a modelling element, right click on the modelling element and select Delete.

It is also possible to add modelling elements by using wizards (See 3.1.6).