Generic Event-B EMF extensions

Refinement

AVAILABLE IN NEXT RELEASE OF ac.soton.eventb.emf.core.extension.feature

The Rodin platform provides an extension point for contributing behaviour to the 'Refine' action. For Serialised Event-B EMF extensions, an abstract, reflective refinement contributor class is provided to simplify the task of making a refinement.

The class is ac.soton.eventb.emf.core.extension.navigator.refiner$AbstractExtensionRefiner which implements IRefinementParticipant. The class should be extended by a client plug-in and the clients class should be registered as a Refinement Participant using the relevant Rodin extension point The client class must implement the method getExtensionID() to return the relevant Extension ID string that identifies such extensions. The client class may override populateReferenceMap(Map<>) to add the EReference Features that need to be dealt with, defining which ones are back references to the corresponding abstract element.

The generic refiner class works as follows:

• All serialised extensions of the given Extension ID in the Rodin resource are loaded
• Each one is deep cloned using the Ecore copier utility
• The contents of the extension are then searched for elements that own one of the client supplied EReferences.
• For each reference, the reference is either set to reference the corresponding source abstract element or copied so that it corresponds to the abstract reference

Generator

AVAILABLE IN NEXT RELEASE OF ac.soton.eventb.emf.core.extension.feature

A framework to support the implementation of generators is provided. The framework is designed to support the generation of standard Event-B models from higher-level model extensions that are based on the Event-B EMF modelling extensions framework.

The Generator framework provides:

• A toolbar button to initiate the generation
• Generic code to remove previously generated elements
• Generic code to organise the incorporation of newly generated elements
• Utilities to aid the creation of new elements
• An abstract basis for client defined rules
• An extension point for clients to declare generators and generation rules

The client rules return generation descriptors (rather than modifying the target model directly). The framework takes care of updating the model (within the clients Transactional Editing Domain) provided the generation completes successfully. This ensures that the model is not left in an inconsistent state should the generation fail. The generation descriptors allow the client to specify where the new element should be contained and a priority which will be used to influence the placement of the new element within the containment ordering.

To define a particular generator a client should:

• Define an extension of org.eclipse.ui.handlers to enable the generate command when the activePartID is their Editor (see Defining a generator handler)
• Define an extension of ac.soton.eventb.emf.diagrams.generator.rule to make the generator framework aware of your generator and its rule classes.
• Implement your rule classes

Implementing Rule Classes

Rule classes must implement IRule. It is recommended the rule classes extend ac.soton.eventb.emf.diagrams.generator#AbstractRule which provides some concise constants for the commonly needed containments and defines some default behaviour (always enabled and the target EventB component is the source component).

The rule's fire method must return a list of GenerationDescriptors. The Utility class, Make, provides a convenience method to help construct a GenerationDescriptor from the parent element, the containment feature, the new child and the priority indicator.

Priority may be from 10 to 0, where 10 indicates first in the containment and 0 last in the containment. [User elements in the same containment will be placed after position 5]. For example, a basic type invariant that doesn't depend on other variables might be placed at position 10 whereas a theorem or invariant included purely for proof purposes might be placed at position 0

A typical line from a rule class might look like this:

		ret.add(Make.descriptor(machine,invariants,Make.invariant("myInvariantName", "myVar >0","my comment"),10));

where, ret is the list to be returned and machine is the parent element containing the invariants to be added to.

Note that the rule will only be attempted for the type of source element defined in the extension point. However, this could be defined as an abstract base class to allow the rule to operate on several types of element. The rules enabled method can be used to restrict when it applies. More than one rule can be defined for the same kind of element allowing the generation to be decomposed in a maintainable way. Since the enablement of rules may depend on what has already been generated, the enabled method is passed the list of GenerationDescriptors created so far.