Introduction (How to extend Rodin Tutorial)
In this tutorial, we will focus on the extension of the Rodin platform by adding plug-ins. This mechanism inherits from Eclipse extension mechanism (see paragraph about Extension points and Extensions below).
As we will discuss here about the provided Rodin extensibility possibilities, reading this tutorial implies that you have basic knowledge in Event-B, and are familiar with Java programming language.
Extension Points and Extensions
Rodin uses Eclipse extensibility mechanism. This mechanism is based on the notions of "extension points" and "extensions".
A plug-in that wants to offer functionalities (e.g. extension services) defines an extension point. An extension point is a sort of contract given to other plug-ins, to use (e.g. extend) those provided extension services. This contract is expressed in XML. A concrete example of extension service is offered by the plug-in org.rodinp.core to register new elements in Rodin database.
Moreover, a plug-in defining an extension point will manage all contributions (that we call extensions), through its lifecycle. In the case of Rodin Database, all extensions of the database (added elements, added attributes, etc.) are managed by the plug-in org.rodinp.core.
To extend Rodin, we are in the situation where plug-ins (callers) want to use the extension services offered by one plug-in (e.g. the callee that defines an extension point).
Thus, we will define a caller (a new plug-in) that accepts one or more contracts with the Rodin platform. To accept such contract, a caller has to specify its dependency to the callee, and define one (resp. many) extensions, which conforms to an (resp. corresponding) imported extension point. The terms of the contract are often given through required interfaces, which defines a protocol to use the provided extension services. In other words, the results of the computation performed in caller's code need to conform to an interface defined by the callee (the extension service provider). Sometimes, the callee defines additional interfaces to give the callers a view on the managed contributions.
In this tutorial, we will define new callers and use the contracts offered by the Rodin platform.
For more information about extension points, please refer to this article: Getting started with Eclipse plug-ins: understanding extension points. Reading this tutorial implies that you have basic knowledge about eclipse extension mechanism, and programming in Java.
Extension Points provided by Eclipse
Eclipse defines extension points that allow plug-ins to contribute behaviours to existing views and editors or to provide implementations for new views and editors (See Basic workbench extension points using actions):
- org.eclipse.ui.views
- org.eclipse.ui.viewActions
- org.eclipse.ui.editors
- org.eclipse.ui.editorActions
- org.eclipse.ui.popupMenus
- org.eclipse.ui.actionSets
Some other extension points are useful to contribute to the GUI:
- org.eclipse.ui.preferencePages, which allows to define preference pages (See Preferences in the Eclipse Workbench UI).
- org.eclipse.ui.navigator.navigatorContent and org.eclipse.ui.navigator.viewer, which allows to get a basic navigator to appear with custom content. This extension point will be used in details in the section " Extending the Rodin Event-B Explorer" of this tutorial.
Finally, a plug-in may contribute help files by using the org.eclipse.help.toc extension point. These files may be written by hand or automatically generated from Wiki pages, as explained here.
Explanations and Outline
This tutorial is problem solving oriented. Hence, all contributions to the platform via plug-in additions will address needs implied by the issues we aim to solve, or functionalities we want to add.
It is mainly based on one concrete example of step-by-step plug-in development. This example will add Probabilistic Termination and Qualitative Reasoning in Rodin. For more informations about the Probabilistic Termination and Qualitative Reasoning, please refer to the paper of Emre Yilmaz and Thai Son Hoang : Development of Rabin's Choice Coordination Algorithm in Event-B in Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010)
See the corresponding paper here : http://e-collection.ethbib.ethz.ch/eserv/eth:1677/eth-1677-01.pdf
Other small examples are used in parallel to review all extensions abilities.
