Rodin Handbook





 

Feedback

2.4.2 Project Setup

Models typically consist of multiple files that are managed in a project. Create a new Event-B Project File $\rangle $ New $\rangle $ Event-B Project. Give the project the name tutorial-03 as shown in Figure 2.5.

\includegraphics[]{img/tutorial/tut_03_tutorial-3.png}
Figure 2.5: New Event-B Project Wizard

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

Eclipse supports different types of projects. The project must have the Rodin Nature (3.1.1.2) to work. A project can have more than one nature.

Next, create a new Event-B Component. Either use File $\rangle $ New $\rangle $ Event-B Component or right-click on the newly created project and select New $\rangle $ Event-B Component. Use mac as the component name, select Machine as component-type, and click Finish as shown in Figure 2.6. This will create a Machine (3.2.3) file.

\includegraphics[]{img/tutorial/tut_03_mac.png}
Figure 2.6: New Event-B Component Wizard

The newly created component will open in the structural editor. The editor has four tabs at the bottom. The Pretty Print shows the model as a whole with color highlighting, but it cannot be edited here. This is useful to inspect the model. The Edit allows editing of the model. It shows the six main sections of a machine (REFINES, SEES, etc.) in a collapsed state. You can click on the \includegraphics[height=2ex]{img/icons/rodin/collapsed.png} button to the left of a section to expand it.

The editor is form-based. This means that in well-defined places an appropriate control (text field, dropdown, etc.) allows modifications.

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

Alternative editors are available as plug-ins. The form editor has the advantage of guiding the user through the model, but it takes up a lot of space and can be slow for big models. The text-based Camille Editor (2.4.3) is very popular. Please visit the Rodin Wiki (1.1.2) for the latest information.