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

TODO: the notion of refinement seems too specific to be put in database plug-in org.rodinp.core; use a more general vocabulary, talking about "creating a new component from an existing one"

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
  • context menu text
  • title (new component window)
  • message (new component window)

Interfaces

IRefinementParticipant

public interface IRefinementParticipant {
	
	void process(IInternalElement root);
	
}

New API

in org.rodinp.core.RodinCore.java:

/**
 * Refines the given root. In case the refinement fails, an error is logged
 * and null is returned.
 * The given source root is not modified by this operation.
 * In the context of this plug-in, the notion of refinement is to be
 * understood as an operation that creates a new component from an existing
 * one, without any constraint about the results.
 * 
 * @param sourceRoot
 *            the root to refine
 * @return refined root or null
 */
public static IInternalElement refine(IInternalElement sourceRoot) {
	return new RefinementProcessor(sourceRoot).refine();
}

File Name Validation

It looks preferable to externalize file name validation, making it independent from refinement.

A new extension point fileNameValidators is proposed

in org.rodinp.core

(Validator)+

• Validator
  • id
  • class, implements IFileNameValidator

public interface IFileNameValidator {

	/**
	 * @param name
	 *            proposed name
	 * @param project
	 *            the project where the file will be created
	 * @return null if the name is valid, else a description of the problem
	 */
	String isValid(String name, IRodinProject project);
	
}