Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License |
3.1.2 The Event-B PerspectiveFigure 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. 3.1.2.1 Menu barThe 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 menuWhen 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).
Three actions are available for machine files (see Figure 3.5).
3.1.2.1.2 Event-B menuWhen 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 barThe 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 ViewThe editor view contains the active Event-B editor which is described in Section 3.1.4. 3.1.2.4 Outline ViewThe outline view displays the outline of the active Event-B editor and lists elements like axioms, variables, etc.. 3.1.2.5 Rodin Problems ViewWhen an error is discovered in a project, a 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 . 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 ViewThe 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. 3.1.2.7 Event-B ExplorerProjects 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 button. By pressing it, one can expand a project and see the machines and contexts that it contains. The icons ( or ) 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). |