Updated:

Installing Rodin

Rodin can be installed from the Event-B home page (http://www.event-b.org)

1. follow the Rodin Platform link in the navigation panel;
2. under Rodin Platform click on the download button;
3. choose the latest release and download the zip archive for your platform;
4. move the archive to where you want to put the Rodin executable and unzip it;
5. this will create a directory named “rodin” and within that directory will be an executable also named “rodin”, but with some executable suffix appropriate for your platform;
6. invoke rodin by executing the rodin executable.

Configuring Rodin

Workspace

When you run Rodin you will be requested to name a workspace. The work space is a directory in which you will store projects. You should give some careful thought to where you put the workspace.

Archive repository

Rodin is not going to ask for this until you want to create an archive of a project. The archive directory should be close to your workspace, but should not be in the workspace.

The initial screen

When you first run Rodin you will be given a welcome window. Having read that you should then simply delete it.

Updating and extending your Rodin application

Soon after installing Rodin you should install the Atelier B provers. Do this as follows:

1. Select Help/Software Updates.

   You will get a window in which you can view either Installed Software or Available Software.

   Notice the Revert Configuration button in the Installed Software view. You can use this to revert to an earlier configuration and it is recommended that you sequence the installation of new packages so that you can simply move back to an earlier configuration if you encounter problems.

   Many of the additional packages are written independently from the main Rodin development and maintenance group. Consequently, especially at release changes, incompatibility problems can occur.

2. Select Available Software. You should see the following item on the list
   • . Select this and expand and you should see
   • .
3. If you don’t see the AtelierB provers there, you could try adding the site using the url you see above. Don’t try going to that url, as you will be refused.
4. Once you have selected the site then select Install and the installation should proceed.

It is recommended that you also install:

AnimB:

a very nice animator;

Camille:

a text editor that is an alternative to Event-B editors that come already installed in Rodin.

Configuring the views and perspective

In Eclipse terminology, windows are called views as they give a views of some part of the model. Initially all the views are accessible via a little rectangular box in the bottom left of the whole view. There is a little vertical separator to the left of that box. You can push the bar to move the box to another position on the page.

If you click on that box you can see all the views to which you have access.

It is recommended that you install the following views:

Event-B explorer:

should be there by default;

Rodin problems:

reports on errors and warnings;

Statistics:

reports proof obligation statistics;

Goal:

goal for current PO;

Proof control:

interactive proof control;

Proof information:

information on current proof;

Once you have a satisfactory configuration you should save it as a perspective:

1. Select Window
2. Select Save perspective as ldots or Reset perspective

The Proof Control tools

The Proof Control view should have the following tools in the toolbar

If it doesn’t then you have something missing. If the lassoo or the scissors are missing this is probably due to the vertical bars shifting: you can move these bars and the tools should reappear.

Documentation

1. Rodin manual: dated, but still a lot of useful information
2. Documentation wiki