Project (Rodin User Manual)

From Event-B

Jump to: navigation, search


Contents

Project Constituents and Relationships

The primary concept in doing formal developments with the Rodin Platform is that of a project. A project contains the complete mathematical development of a Discrete Transition System. It is made of several components of two kinds: machines and contexts. Machines contain the variables, invariants, theorems, and events of a project, whereas contexts contain the carrier sets, constants, axioms, and theorems of a project:

We remind the reader of the various relationships existing between machines and contexts. This is illustrated in the following figure. A machine can be "refined" by another one, and a context can be "extended" by another one (no cycles are allowed in both these relationships). Moreover, a machine can "see" one or several contexts. A typical example of machine and context relationship is shown below:

The Project Explorer

Projects are reachable in the RODIN platform by means of a window called the "Project Explorer". This window is usually situated on the left hand side of the screen (but, in Eclipse, the place of such windows can be changed very easily). Next is a screen shot showing a "Project Explorer" window:

As can be seen on this screen shot, the Project Explorer window contains the list of current project names. Next to each project name is a little triangle. By pressing it, one can expand a project and see its components as shown below.

We expanded the project named "celebrity". This project contains 2 contexts named "celebrity_ctx_0" and "celebrity_ctx_1". It also contains 4 machines named "celebrity_0" to "celebrity_3". The icons (
context
or
machine
) situated next to the components help recognizing their kind (context or machine respectively)

In the remaining parts of this section we are going to see how to create (section 1.3), remove (section 1.4), export (section 1.5), import (section 1.6), change the name (section 1.7) of a project, create a component (section 1.8), and remove a component (section 1.9). In the next two sections (2 and 3) we shall see how to manage contexts and machines.

Creating a Project

In order to create a new project, simply press the
Create new project
button as indicated below in the "Project Explorer" window:

The following wizard will then appear, within which you type the name of the new project (here we type "alpha"):

After pressing the Finish button, the new project is created and appears in the "Project Explorer" window.

Removing a Project

In order to remove a project, you first select it on the "Project Explorer" window and then right click with the mouse. The following contextual menu will appear on the screen:

You simply click on Delete and your project will be deleted (confirmation is asked). It is then removed from the Project Explorer window.

Exporting a Project

Exporting a project is the operation by which you can construct automatically a "zip" file containing the entire project. Such a file is ready to be sent by mail. Once received, an exported project can be imported (next section), it then becomes a project like the other ones which were created locally. In order to export a project, first select it, and then click on File > Export from the menubar as indicated below:

The Export wizard will pop up. In this window, select General > Archive File and click Next >. Specify the path and name of the archive file into which you want to export your project and finally click Finish. This menu sequence belongs (as well as the various options) to Eclipse. For more information, have a look at the Eclipse documentation.

Importing a Project

A ".zip" file corresponding to a project which has been exported elsewhere can be imported locally. In order to do that, click on File > Import from the menubar. In the import wizard, select General > Existing Projects into Workspace and click Next >. Then, enter the file name of the imported project and finally click Finish. Like for exporting, the menu sequence and layout are part of Eclipse.

The importation is refused if the name of the imported project (not the name of the file), is the same as the name of an existing local project. The moral of the story is that when exporting a project to a partner you better modify its name in case your partner has already got a project with that same name (maybe a previous version of the exported project). Changing the name of a project is explained in the next section.

Changing the Name of a Project

The procedure for changing the name of a project is a bit heavy at the present time. Here is what you have to do. Select the project whose name you want to modify. Enter the Eclipse "Resource" perspective (in Window > Open Perspective > Other...). A "Navigator" window will appear in which the project names are listed (and your project still selected). Right click with the mouse and, in the coming menu, click Rename. Modify the name and press enter. Return then to the original perspective. The name of your project has been modified accordingly.

Creating a Component

In this section, we learn how to create a component (context or machine). In order to create a component in a project, you have to first select the project and then click the
Create a new component
button as shown below:

You may now choose the type of the component (machine or context) and give it a name as indicated:

Click Finish to eventually create the component. The new component will appear in the Project Explorer window.

Removing a Component

In order to remove a component, press the right mouse button. In the coming menu, click Delete. This component is removed from the Project Explorer window.