Updated:

Rodin information

For most recent information on Rodin including most recent release:

http://wiki.event-b.org/index.php/Main_Page

Rodin is implemented on Eclipse and can be installed on Mac OS X, Windows, and Linux.

Installing Rodin

1. follow instructions on Rodin website;
2. make sure you install:

   AtelierB provers

   : basic provers;

   AnimB

   : a very nice animator;

   Other advice may follow.

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.

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