Difference between revisions of "Extending the Rodin database (How to extend Rodin Tutorial)"

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Pascal
Line 1: Line 1:
{{Navigation|Previous= [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Extend the database]]|Next=[[Extend_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)|Extend the structured editor]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]]}}
+
{{Navigation|Previous= [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Extending the database]]|Next=[[Extend_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)|Extending the structured editor]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]]}}
  
 
=== In this part ===
 
=== In this part ===
Line 11: Line 11:
  
 
=== Step 1 ===
 
=== Step 1 ===
When one wants to use extension points provided by a plugin, one has to add a dependency to this plugin.
+
When one wants to use extension points provided by a plug-in, one has to add a dependency to this plug-in.
We will use 2 extension points to extend the database, so we need to add a dependency to the plugin <tt>org.rodinp.core</tt> which defines them.
+
We will use 2 extension points to extend the database, so we need to add a dependency to the plug-in <tt>org.rodinp.core</tt> which defines them.
Moreover, as we want to manipulate event-b elements, we will manipulate interfaces and public classes provided by the event-B plugin.
+
Moreover, as we want to manipulate event-b elements, we will manipulate interfaces and public classes provided by the event-B plug-in.
We will then add a dependency to the plugin <tt>org.eventb.core</tt>
+
We will then add a dependency to the plug-in <tt>org.eventb.core</tt>
To do this, open the MANIFEST.MF file in the forlder META-INF of our plugin to get the following:
+
To do this, open the MANIFEST.MF file in the folder META-INF of our plug-in to get the following:
  
 
[[Image:Extend_Rodin_Tuto_1_5_Manifest_dependencies.png|500px]]
 
[[Image:Extend_Rodin_Tuto_1_5_Manifest_dependencies.png|500px]]
Line 21: Line 21:
 
1. Click on the "Dependencies" Tab, <br>
 
1. Click on the "Dependencies" Tab, <br>
 
2. Click on the Add button.<br>
 
2. Click on the Add button.<br>
A dialog appears, start to enter <tt>org.rodinp.core</tt> and select this plugin, press "OK" to add it to the dependencies.<br>
+
A dialog appears, start to enter <tt>org.rodinp.core</tt> and select this plug-in, press "OK" to add it to the dependencies.<br>
 
The dependency to <tt>org.rodinp.core</tt> has been added.
 
The dependency to <tt>org.rodinp.core</tt> has been added.
 
Re-do the above operations to add <tt>org.eventb.core</tt>.
 
Re-do the above operations to add <tt>org.eventb.core</tt>.
  
You should now have the following dependencies added to the plugin :
+
You should now have the following dependencies added to the plug-in :
  
 
[[Image:Extend_Rodin_Tuto_1_5_Added_Dependencies.png|200px]]
 
[[Image:Extend_Rodin_Tuto_1_5_Added_Dependencies.png|200px]]
Line 88: Line 88:
 
=== Step 5 ===
 
=== Step 5 ===
 
We now opened the class ''Bound.java'' and see that we need to implement the method <tt>getElementType()</tt> inherited from the superclass.<br>
 
We now opened the class ''Bound.java'' and see that we need to implement the method <tt>getElementType()</tt> inherited from the superclass.<br>
As the type of element might be needed from outside, and is common to all Bound element, we will create a constanst in a new interface IBound that we have to create.<br>
+
As the type of element might be needed from outside, and is common to all Bound element, we will create a constant in a new interface <tt>IBound</tt> that we have to create.<br>
 
Enter in the method body the following code :
 
Enter in the method body the following code :
 
  return IBound.ELEMENT_TYPE;
 
  return IBound.ELEMENT_TYPE;
Line 94: Line 94:
 
[[Image:Extend_Rodin_Tuto_1_7_Create_Interface_Menu.png|400px]]
 
[[Image:Extend_Rodin_Tuto_1_7_Create_Interface_Menu.png|400px]]
  
Then use the quick assist (while you go over IBound underlined in red), to create the interface IBound.
+
Then use the quick assist (while you go over <tt>IBound</tt> underlined in red), to create the interface <tt>IBound</tt>.
 
The following wizard appears :
 
The following wizard appears :
 
   
 
   
 
[[Image:Extend_Rodin_Tuto_1_7_Create_Interface_Wizard.png|400px]]
 
[[Image:Extend_Rodin_Tuto_1_7_Create_Interface_Wizard.png|400px]]
  
Use here the "Extended Interfaces" field to specify that the element '''Bound''' should be commented (thus shall implement ICommentedElement) and will carry an expression (thus shall implement IExpressionElement) for the value of the bound.  
+
Use here the "Extended Interfaces" field to specify that the element '''Bound''' should be commented (thus shall implement <tt>ICommentedElement</tt>) and will carry an expression (thus shall implement <tt>IExpressionElement</tt>) for the value of the bound.  
  
 
  public interface IBound extends ICommentedElement, IExpressionElement {
 
  public interface IBound extends ICommentedElement, IExpressionElement {
Line 111: Line 111:
 
[[Image:Extend_Rodin_Tuto_1_7_Used_Extensions.png]]
 
[[Image:Extend_Rodin_Tuto_1_7_Used_Extensions.png]]
  
and you should have the following contents in your plugin :
+
and you should have the following contents in your plug-in :
  
 
[[Image:Extend_Rodin_Tuto_1_7_ProjectExplorer2.png.png]]
 
[[Image:Extend_Rodin_Tuto_1_7_ProjectExplorer2.png.png]]
  
The sources of the plugin at this point can be downloaded here : // FIXME attach sources here.
+
The sources of the plug-in at this point can be downloaded here: // FIXME attach sources here.
  
 
=== In Brief ===
 
=== In Brief ===
  
We saw how to use Eclipse to add extension points that will be used in our plugin and created our extensions using some helpful Eclipse automatic actions (wizard, content assist...).
+
We saw how to use Eclipse to add extension points that will be used in our plug-in and created our extensions using some helpful Eclipse automatic actions (wizard, content assist...).
 
As we had a detailed view (captures) of all the actions further needed, the next parts of this tutorial will focus only on the extensions.
 
As we had a detailed view (captures) of all the actions further needed, the next parts of this tutorial will focus only on the extensions.
 
   
 
   

Revision as of 14:21, 20 August 2010

In this part

We will explain how to add a new attribute to events elements and add a new element in the database. Here are the steps we will detail:

  1. Add dependencies to the plug-ins providing the extension services and interfaces we want to use.
  2. Add the extension points we will use, and define our extensions.
  3. Implement required classes to specify newly added elements.
  4. Create an interface using Eclipse content assist.

For more information about the database extension, please refer to: Extending the Rodin Database

Step 1

When one wants to use extension points provided by a plug-in, one has to add a dependency to this plug-in. We will use 2 extension points to extend the database, so we need to add a dependency to the plug-in org.rodinp.core which defines them. Moreover, as we want to manipulate event-b elements, we will manipulate interfaces and public classes provided by the event-B plug-in. We will then add a dependency to the plug-in org.eventb.core To do this, open the MANIFEST.MF file in the folder META-INF of our plug-in to get the following:

Extend Rodin Tuto 1 5 Manifest dependencies.png

1. Click on the "Dependencies" Tab,
2. Click on the Add button.
A dialog appears, start to enter org.rodinp.core and select this plug-in, press "OK" to add it to the dependencies.
The dependency to org.rodinp.core has been added. Re-do the above operations to add org.eventb.core.

You should now have the following dependencies added to the plug-in :

Extend Rodin Tuto 1 5 Added Dependencies.png

Step 2

We will add now the Extensions Points that we want to use, and define extensions using them.

Extend Rodin Tuto 1 6 Add Extension Point.png

1. Click on the "Extensions" Tab,
2. and click on the "Add" button.

Extend Rodin Tuto 1 6 Extension Point Selection.png

As we will start by extending the database by adding the attribute "probabilistic", we will create an extension for org.rodinp.core.attributeTypes extension point. Hence, we need to add this extension point first before creating an extension with it. To do so... on the wizard that appeared (see picture above):
1. start to type the extension point name org.rodinp.core.attributeTypes, to reveal it in the list of available extension points,
2. select it in the list, and click on "Finish" to add it.

The extension point org.rodinp.core.attributeTypes now appears in the list on the "Extensions" page of the MANIFEST.MF of our plugin.

Step 3

We will now add the attribute "probabilistic" in the database, creating an extension for org.rodinp.core.attributeTypes. Right click on the extension point, select New > attributeType as in the picture below :

Extend Rodin Tuto 1 7 Add Attibute Extension.png

A new extension attributeType has been added. We will edit it to add our "probabilistic" attribute.
As an event can be probabilistic or not, we set the kind of this attribute to boolean. Give a unique ID to this attribute (here probabilistic) and a name (here Event-B Probabilistic Attribute). You should now have something similar to what appears in the picture below :

Extend Rodin Tuto 1 7 Add Attibute Extension2.png

Step 4

We will now add a new element "Bound" to set the upper bound of the probabilistic variant.
Repeat the step 2, to add the extension point : org.rodinp.core.internalElementTypes.
Create an extension to specify our new element "Bound" using the right click as previously.
You shall now specify the details for this new extension element :

Extend Rodin Tuto 1 7 Bound Extension.png

As in the picture above :
1. give the element a unique ID (here bound)
2. give a name to this element (here Event-B Bound Element)
3. now things differ, as this extension point (org.rodinp.core.internalElementTypes) requires us to provide a class describing the element.
Click on the "class*:" link to open a wizard that will help us to create this class.

The following wizard appears :

Extend Rodin Tuto 1 7 Bound Extension New Java Class Bound.png

1. First specify a package where you want this class to be stored. As we want to organise a bit the project, we will say that all elements that we add will be part of a new package called fr.systerel.rodinextension.sample.basis,
2. Give the name of the class : "Bound",
3. We see that the superclass of this element is org.rodinp.core.basis.InternalElement but we know that we will implement an element specific to Event-B, so we put here org.eventb.core.basis.EventBElement,
4. You can optionnaly add comments automatically to the created class, if you set them in "Preferences > Java > Code Style > Code Templates",
5. Click on "Finish" to create the class.

The class Bound.java has now been created. We can open it and review its contents that we anyway shall modify now.

Step 5

We now opened the class Bound.java and see that we need to implement the method getElementType() inherited from the superclass.
As the type of element might be needed from outside, and is common to all Bound element, we will create a constant in a new interface IBound that we have to create.
Enter in the method body the following code :

return IBound.ELEMENT_TYPE;

Extend Rodin Tuto 1 7 Create Interface Menu.png

Then use the quick assist (while you go over IBound underlined in red), to create the interface IBound. The following wizard appears :

Extend Rodin Tuto 1 7 Create Interface Wizard.png

Use here the "Extended Interfaces" field to specify that the element Bound should be commented (thus shall implement ICommentedElement) and will carry an expression (thus shall implement IExpressionElement) for the value of the bound.

public interface IBound extends ICommentedElement, IExpressionElement {
	IInternalElementType<IBound> ELEMENT_TYPE = RodinCore
			.getInternalElementType(QualProbPlugin.PLUGIN_ID + ".bound");
}

Modify the class Bound.java to add implements IBound.
At this point of the development, you should have the following extensions :

Extend Rodin Tuto 1 7 Used Extensions.png

and you should have the following contents in your plug-in :

Extend Rodin Tuto 1 7 ProjectExplorer2.png.png

The sources of the plug-in at this point can be downloaded here: // FIXME attach sources here.

In Brief

We saw how to use Eclipse to add extension points that will be used in our plug-in and created our extensions using some helpful Eclipse automatic actions (wizard, content assist...). As we had a detailed view (captures) of all the actions further needed, the next parts of this tutorial will focus only on the extensions.