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.

New APIs are divided between Core and UI, in order to make it possible to programmatically make a refinement.

Extension Points

For generality, the notion of refinement here is to be understood as an operation that makes a new component (the target) from an existing one (the source), without any constraint about the results.

Machine refinement and context extension are particular cases of refinement.

refinements

in org.rodinp.core

((Refinement | Participant | Order)+)

• Refinement
  • id
  • Root Element Type
• Participant
  • id
  • refinement id
  • class, implements IRefinementParticipant
• Order
  • First Participant id
  • Second Participant id

refinementUI

in org.eventb.ui

(UIMessages+)

• UIMessages
  • refinement id
  • label (contextual menu)
  • title (new component window)
  • message (new component window)

Interfaces

IRefinementParticipant

This interface is implemented by clients who want to participate in refinements.

public interface IRefinementParticipant {

/**
 * Modifies the given target root in order to make it (partially or
 * entirely) a refinement of the given source root. The source root is not
 * modified by this operation.
 * 
 * @param targetRoot
 *            the target root
 * @param sourceRoot
 *            the source of the refinement
 * @param monitor
 *            a progress monitor, or null
 * @throws RodinDBException
 *             if a database operation fails
 */
void process(IInternalElement targetRoot, IInternalElement sourceRoot,
		IProgressMonitor monitor) throws RodinDBException;

}

File Name Validation

File name validation will be treated apart, as a separate feature request, as it does not seem directly related to this topic.

How to extend an existing refinement

Say we want to participate in machine refinement, for instance because we introduced a new element type used in machines, that is not processed by standard refinement.

In this case, we already have:

• a refinement defined in org.eventb.core: org.eventb.core.machineRefinement for machine root element type
• a refinement participant implementing standard machine refinement: org.eventb.core.machineRefiner
• refinement UI for this refinement, contributed in org.eventb.ui

All we have to do is:

• contribute a new participant, implementing the refinement of elements of our new element type
• set an order, so that our new participant is called after the standard one

Setting an order may not be necessary, in case our contributed elements are disconnected from the rest of the machine (put at machine root).

An archive for this example is attached in feature request: FR3260797