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.