Extending Refinement Actions

Purpose

The GUI of Rodin 2.1 provides two actions for creating a new component from an existing one. These actions are available as entries in the context menu of event-B components in the Event-B Explorer:

• $\sqsubseteq$ Refine for machines
• $\sqsubseteq$ Extend for contexts

In release 2.1, these actions are hard-coded in the event-B UI plug-in. They copy some of the elements of the selected component into the new component and massage the latter so that it statically checks and does not produce any proof obligation.

The purpose of this development is to allow external plug-ins to contribute to these actions.

Analysis

The implementation of the two actions in Rodin 2.1 is very similar. Both proceed along the following steps:

1. Retrieve the name of the selected component from Eclipse UI.
2. Open a pop-up window asking for the name of the new component (and check its validity).
3. Run a workspace job for populating the new component with parts of the old one, plus additional tricks.
4. Save the new component to disk.
5. Open the event-B editor for the new component.

In order to make these actions extensible, we need to open the following points to external contributions:

1. Name of the action in the context menu (e.g., Refine, Extend).
2. Title and message of the pop-up window for entering the new component name.
3. Name validator for the new component (currently, only the absence of a machine or context with the same name is checked).
4. Contribution to the construction of the new component.

The first three items must be contributed only once per file type. For the last item, we want that several plug-in can contribute (e.g., each on different aspects). To ensure repeatability, we need that plug-ins define an order of execution among the contributions. This could be derived from dependency declarations where plug-ins would declare that a contribution must occur before or after another contribution. In case of a loop in the dependencies, an internal error would be reported to the user (with details of the loop in the workspace log).

API Change

The proposed change is two-fold. Firstly, it allows plug-ins to contribute similar refinement actions on other components than machine and refinements. Secondly, it allows plug-ins to contribute to the construction of the new concrete component.

TODO: Finish API description