Rodin User’s Handbook v.2.4: The Event-B Perspective

3.1.2 The Event-B Perspective

Figure 3.3 shows an overview of the opening window of the Event-B Perspective. The following subsections identify the different Rodin GUI elements (i.e. views) which are visible and explain their functions.

$\includegraphics{img/reference/ref_01_eventb_perspective1.png}$

Figure 3.3: Overview of the Event-B Perspective

3.1.2.1 Menu bar

The menu bar provides file and edit operations and other useful Event-B specific operations. We will briefly describe the most important menu items here.

3.1.2.1.1 Rename menu

When opening a machine or context file, the following actions for automatically renaming the Event-B model elements are available for the user:

One action is available when editing context files (see Figure 3.4).

Automatic Axiom Labelling: this action will rename the axioms alphanumerically according to their order of appearance.

$\includegraphics{img/reference/ref_01_menubar2.png}$

Figure 3.4: Automatic rename actions for context files

Three actions are available for machine files (see Figure 3.5).

Automatic Invariant Labelling: this action will rename the invariants alphanumerically according to their order of appearance.
Automatic Guard Labelling: this action will rename the guards alphanumerically according to their order of appearance,
Automatic Action Labelling: this action will rename the actions alphanumerically according to their order of appearance.

$\includegraphics{img/reference/ref_01_menubar1.png}$

Figure 3.5: Automatic rename actions for machine files

3.1.2.1.2 Event-B menu

When opening a machine or context file, some wizards for creating Event-B model elements are available for the user. The different wizards are described in Section 3.1.6.

3.1.2.2 Tool bar

The tool bar provides shortcuts for familiar commands like save, print, undo and redo. The tool bar also provides shortcuts to the wizards for creating elements like axioms, constants, enumerated sets, etc., which are described in Section 3.1.6.

3.1.2.3 Editor View

The editor view contains the active Event-B editor which is described in Section 3.1.4.

3.1.2.4 Outline View

The outline view displays the outline of the active Event-B editor and lists elements like axioms, variables, etc..

3.1.2.5 Rodin Problems View

When an error is discovered in a project, a $\includegraphics[height=2ex]{img/icons/rodin/error_ovr2.png}$ marker appears next to the line with the problem in the editor view, and the faulty component in the Event-B Explorer is also similarly marked with $\includegraphics[height=2ex]{img/icons/rodin/error_ovr.png}$ . The error itself (e.g. a syntax error) is shown in the Rodin Problems view.

By double-clicking on the error statement, you are transferred automatically to the place where the error has been detected so that you can correct it easily.

3.1.2.6 Symbols View

The symbols view is intended to give users a convenient way to add mathematical symbols to the various model editors. If an editor is open and a text field is active (the cursor is blinking), clicking a symbol will insert it at the current position (see Figure 3.6).

The ASCII code corresponding to the symbol over which the mouse hovers is also displayed as a tooltip so that the user can also learn how to input symbols directly.

$\includegraphics{img/reference/ref_01_symbol_table1.png}$

Figure 3.6: Clicking a symbol inserts it at the current position

3.1.2.7 Event-B Explorer

Projects can be found in the RODIN platform in the Event-B Explorer. This is usually situated on the left hand side of the screen as shown in Figure 3.3. The Event-B Explorer contains a list of name of the current projects. Next to each project name is a $\includegraphics[height=2ex]{img/icons/rodin/collapsed.png}$ button. By pressing it, one can expand a project and see the machines and contexts that it contains.

The icons ( $\includegraphics[height=2ex]{img/icons/rodin/ctx_obj.png}$ or $\includegraphics[height=2ex]{img/icons/rodin/mch_obj.png}$ ) next to the component name identifies whether it is a context or machine respectively.

When expanding a machine or a context, you can explore its elements. Double clicking on a specific element (i.e. a variable) opens the Event-B editor and marks the position of the variable in the machine or context as shown in Figure 3.7. Furthermore, proof obligations are displayed when clicking on the small triangle next to the label Proof Obligations (for more information see Section 3.1.7).

$\includegraphics{img/reference/ref_01_project_explorer1.png}$

Figure 3.7: Double clicking on an element opens the Event-B editor and marks the corresponding position