Difference between revisions of "Extending the Rodin Database"

Latest revision as of 15:43, 4 September 2013

There are different ways to extend the Rodin Database:

adding a new attribute.
adding a new element.

Since Rodin 3.0, when adding an element or an attribute type to the database, you also have to define the relationship it has with other elements types. For an attribute, it consists into defining which elements can carry it. For an element, it consists into defining which elements can parent it, and defining which elements can be considered as children of it.

Adding a New Attribute

Declaring its type

The extension point org.rodinp.core.attributeTypes allows to declare a new attribute. The element to add is attributeType.

In the example below, we assume that the extensions are developed within a plug-in project with name org.eventb.developer.examples

The following extension declares a new string attribute.

<extension
        point="org.rodinp.core.attributeTypes">
     <attributeType
           id="stringAttr"
           kind="string"
           name="%eventBStringAttribute">
     </attributeType>
 </extension>

The attribute has an ID (which should be always unique) which also contain the project name, i.e. org.eventb.developer.examples.stringAttr. This unique ID will be used for access the value corresponding to this attribute of an element later.

The name of the attribute is a string that could be externalised to be used for displaying to the users in the future.

There are five different attribute kinds: boolean, handle, integer, long, string.

Declaring its relationship with existing elements

Imagine we want our newly create attribute type stringAttr be an attribute for the "variable" elements of Event-B models. We have to declare the fact that "variable" elements "can carry" our type of attribute. The extension point org.rodinp.core.itemRelations allows to declare such a relation.

The following extension declares our new string attribute stringAttr as carried by "variable" elements.

<extension
        point="org.rodinp.core.itemRelations">
     <relationship parentTypeId="org.eventb.core.variable">
        <attributeType typeId="org.eventb.developer.examples.stringAttr">
        </attributeType>
     </relationship>
</extension>

Note that for a given parent element type identified by parentTypeId, one can set multiple attributeType which denotes they are all carried by this parent element.

Accessing (Programmatically) the Newly Created Attribute

After declaring the attribute with the ID and the kind of the attribute, we need to access the value corresponding to the attribute of any internal element.

Getting the corresponding Java attribute kind

Firstly, we need to get the corresponding Java attribute kind.

boolean: org.rodinp.core.IAttributeType.Boolean

handle: org.rodinp.core.IAttributeType.Handle

integer: org.rodinp.core.IAttributeType.Integer

long: org.rodinp.core.IAttributeType.Long

string: org.rodinp.core.IAttributeType.String

The following methods get the corresponding Java attribute kind, given an unique ID and the kind (as declared via the extension point).

org.rodinp.core.IAttributeType.Boolean RodinCore.getBoolAttrType(String ID)

org.rodinp.core.IAttributeType.Handle RodinCore.getHandleAttrType(String ID)

org.rodinp.core.IAttributeType.Integer RodinCore.getIntegerAttrType(String ID)

org.rodinp.core.IAttributeType.Long RodinCore.getLongAttrType(String ID)

org.rodinp.core.IAttributeType.String RodinCore.getStringAttrType(String ID)

Note: There is a general method for getting the Java attribute kind given an unique ID (without knowing in advance the kind as declared via the extension point).

org.rodinp.core.IAttributeType RodinCore.getAttrubuteType(String ID)

As an example with the previously declare attribute, we can use the following code to get the attribute type:

 org.rodinp.core.IAttributeType.String attrType = RodinCore.getStringAttrType("org.eventb.developer.examples");

Checking for existence of the attribute for an element

Given an internal element (i.e. IInternalElement), and given an attribute type (i.e. IAttributeType), method boolean IInternalElement.hasAttribute(IAttributeType) checks for the existence of this attribute for the input element.

Getting the value corresponding to the attribute of an element

Depending on the Java attribute kind, we have different methods for getting the value corresponding to the attribute of an internal element (i.e. IInternalElement).

boolean IInternalElement.getAttributeValue(IAttributeType.Boolean)

IRodinElement IInternalElement.getAttributeValue(IAttributeType.Handle)

int IInternalElement.getAttributeValue(IAttributeType.Integer)

long IInternalElement.getAttributeValue(IAttributeType.Long)

String IInternalElement.getAttributeValue(IAttributeType.String)

As an example, we can use the following code to set our previously declared attribute of an internal element (e.g. elem)

String attrValue = elem.getAttributeValue(attrType);

Setting the value corresponding to the attribute of an element

Depending on the Java attribute kind, we have different methods for setting the value corresponding to the attribute of an internal element (i.e. IInternalElement).

void IInternalElement.setAttributeValue(IAttributeType.Boolean, boolean, IProgressMonitor)

void IInternalElement.setAttributeValue(IAttributeType.Handle, IRodinElement, IProgressMonitor)

void IInternalElement.setAttributeValue(IAttributeType.Integer, int, IProgressMonitor)

void IInternalElement.setAttributeValue(IAttributeType.Long, long, IProgressMonitor)

void IInternalElement.setAttributeValue(IAttributeType.String, String, IProgressMonitor)

As an example, we can use the following code to set our previously declared attribute of an internal element (e.g. elem)

elem.setAttributeValue(attrType, "My new value", new NullProgressMonitor());

Adding a New Element

Declaring its type

The extension point org.rodinp.core.internalElementTypes allows to declare a new element. The element to add is internalElementType. The following extension declares a new element:

 <extension
        point="org.rodinp.core.internalElementTypes">
     <internalElementType
           id="myElement"
           class="package.MyClass"
           name="%eventBElement">
     </internalElementType>
 </extension>

An element has a unique ID, a name, and a class. This class shall be a subclass of org.eventb.core.basis.EventBElement, and it shall implement the following interfaces, depending on the attributes that will be associated to this newly created element:

If the element will be commented, this class shall implement ICommentedElement.
If the element will be labelled, this class shall implement ILabeledElement.
If the element will be identified, this class shall implement IIdentifierElement.
If the element will carry an expression, this class shall implement IExpressionElement.
If the element will carry a predicate, this class shall implement IPredicateElement.
If the element will carry an assignment, this class shall implement IAssignmentElement.
If the element will have a convergence, this class shall implement IConvergenceElement.

Declaring its relationship with existing elements

After having declared the new element type myElement, one has to define at which place this element can appear in the database.
Indeed, just registering the type will not allow any element of this type be part of a file in the database.

To declare relationships one has to contribute to the extension point org.rodinp.core.itemRelations.
Now suppose we want to register the elements of type myElement as children of machine files, like Event-B variables for example, then hereafter is the definition of such an item relation:

<extension
        point="org.rodinp.core.itemRelations">
     <relationship
           parentTypeId="org.eventb.core.machineFile">
        <childType
              typeId="org.eventb.developer.examples.myElement">
        </childType>
     </relationship>
</extension>

The plug-in id shall prefix the name of the element type contributed. Note that for a given parent element type identified by parentTypeId, one can set multiple childType elements which denotes they are all valid child types of the identified parent element.

@@ Line 1: / Line 1: @@
 There are different ways to extend the Rodin Database:
+* adding a new attribute.
 * adding a new element.
-* adding a new attribute.
+Since Rodin 3.0, when adding an element or an attribute type to the database, you also have to define the relationship it has with other elements types.
+For an attribute, it consists into defining which elements can carry it. For an element, it consists into defining which elements can parent it, and defining which elements can be considered as children of it.
-== Adding a New Element ==
+== Adding a New Attribute ==
+=== Declaring its type ===
-== Adding a New Attribute to Existing Elements ==
+The extension point <code>org.rodinp.core.attributeTypes</code> allows to declare a new attribute.  The element to add is <code>attributeType</code>.
-=== Declare a New Attribute ===
-The extension point <code>org.rodinp.core.attributeTypes</code> to declare a new attribute.
 In the example below, we assume that the extensions are developed within a plug-in project with name '''org.eventb.developer.examples'''
@@ Line 30: / Line 29: @@
 * There are five different attribute kinds: ''boolean'', ''handle'', ''integer'', ''long'', ''string''.
-=== Access (Programmatically) the Newly Created Attribute ===
+=== Declaring its relationship with existing elements ===
+Imagine we want our newly create attribute type <tt>stringAttr</tt> be an attribute for the "variable" elements of Event-B models. We have to declare the fact that "variable" elements "can carry" our type of attribute.
+The extension point <code>org.rodinp.core.itemRelations</code> allows to declare such a relation.
+The following extension declares our new string attribute <tt>stringAttr</tt> as carried by "variable" elements.
+ <extension
+         point="org.rodinp.core.itemRelations">
+      <relationship parentTypeId="org.eventb.core.variable">
+         <attributeType typeId="org.eventb.developer.examples.stringAttr">
+         </attributeType>
+      </relationship>
+ </extension>
+Note that for a given parent element type identified by <tt>parentTypeId</tt>, one can set multiple <tt>attributeType</tt> which denotes they are all carried by this parent element.
+=== Accessing (Programmatically) the Newly Created Attribute ===
 After declaring the attribute with the ID and the kind of the attribute, we need to access the value corresponding to the attribute of any internal element.
@@ Line 67: / Line 82: @@
    org.rodinp.core.IAttributeType.String attrType = RodinCore.getStringAttrType("org.eventb.developer.examples");
-==== Check for existence of the attribute ====
+==== Checking for existence of the attribute for an element ====
-Given an internal element (i.e. <code>IInternalElement</code>), and given an attribute type (i.e. <code>IAttributeType</code>), method <code>boolean hasAttribute(IAttributeType)</code> within <code>IInternalElement</code> checks for the existence of this attribute for the input element.
+Given an internal element (i.e. <code>IInternalElement</code>), and given an attribute type (i.e. <code>IAttributeType</code>), method <code>boolean IInternalElement.hasAttribute(IAttributeType)</code> checks for the existence of this attribute for the input element.
-==== Get the value corresponding to the attribute of an element ====
+==== Getting the value corresponding to the attribute of an element ====
 Depending on the Java attribute kind, we have different methods for getting the value corresponding to the attribute of an internal element (i.e. <code>IInternalElement</code>).
-* <code>boolean getAttributeValue(IAttributeType.Boolean)</code>
+* <code>boolean IInternalElement.getAttributeValue(IAttributeType.Boolean)</code>
-* <code>IRodinElement getAttributeValue(IAttributeType.Handle)</code>
+* <code>IRodinElement IInternalElement.getAttributeValue(IAttributeType.Handle)</code>
-* <code>int getAttributeValue(IAttributeType.Integer)</code>
+* <code>int IInternalElement.getAttributeValue(IAttributeType.Integer)</code>
-* <code>long getAttributeValue(IAttributeType.Long)</code>
+* <code>long IInternalElement.getAttributeValue(IAttributeType.Long)</code>
-* <code>String getAttributeValue(IAttributeType.String)</code>
+* <code>String IInternalElement.getAttributeValue(IAttributeType.String)</code>
+As an example, we can use the following code to set our previously declared attribute of an internal element (e.g. <code>elem</code>)
+ String attrValue = elem.getAttributeValue(attrType);
+==== Setting the value corresponding to the attribute of an element ====
+Depending on the Java attribute kind, we have different methods for setting the value corresponding to the attribute of an internal element (i.e. <code>IInternalElement</code>).
+* <code>void IInternalElement.setAttributeValue(IAttributeType.Boolean, boolean, IProgressMonitor)</code>
+* <code>void IInternalElement.setAttributeValue(IAttributeType.Handle, IRodinElement, IProgressMonitor)</code>
+* <code>void IInternalElement.setAttributeValue(IAttributeType.Integer, int, IProgressMonitor)</code>
+* <code>void IInternalElement.setAttributeValue(IAttributeType.Long, long, IProgressMonitor)</code>
+* <code>void IInternalElement.setAttributeValue(IAttributeType.String, String, IProgressMonitor)</code>
+As an example, we can use the following code to set our previously declared attribute of an internal element (e.g. <code>elem</code>)
+ elem.setAttributeValue(attrType, "My new value", new NullProgressMonitor());
+== Adding a New Element ==
+=== Declaring its type ===
+The extension point <code>org.rodinp.core.internalElementTypes</code> allows to declare a new element.  The element to add is <code>internalElementType</code>.
+The following extension declares a new element:
+  <extension
+         point="org.rodinp.core.internalElementTypes">
+      <internalElementType
+            id="myElement"
+            class="package.MyClass"
+            name="%eventBElement">
+      </internalElementType>
+  </extension>
+An element has a unique ID, a name, and a class. This class shall be a subclass of <tt>org.eventb.core.basis.EventBElement</tt>, and it shall implement the following interfaces, depending on the attributes that will be associated to this newly created element:
+* If the element will be commented, this class shall implement <tt>ICommentedElement</tt>.
+* If the element will be labelled, this class shall implement <tt>ILabeledElement</tt>.
+* If the element will be identified, this class shall implement <tt>IIdentifierElement</tt>.
+* If the element will carry an expression, this class shall implement <tt>IExpressionElement</tt>.
+* If the element will carry a predicate, this class shall implement <tt>IPredicateElement</tt>.
+* If the element will carry an assignment, this class shall implement <tt>IAssignmentElement</tt>.
+* If the element will have a convergence, this class shall implement <tt>IConvergenceElement</tt>.
+=== Declaring its relationship with existing elements ===
+After having declared the new element type <tt>myElement</tt>, one has to define at which place this element can appear in the database.<br />
+Indeed, just registering the type will not allow any element of this type be part of a file in the database.
+To declare relationships one has to contribute to the extension point <code>org.rodinp.core.itemRelations</code>. <br />
+Now suppose we want to register the elements of type <tt>myElement</tt> as children of machine files, like Event-B variables for example, then hereafter is the definition of such an item relation:
+ <extension
+         point="org.rodinp.core.itemRelations">
+      <relationship
+            parentTypeId="org.eventb.core.machineFile">
+         <childType
+               typeId="org.eventb.developer.examples.myElement">
+         </childType>
+      </relationship>
+ </extension>
+The plug-in id shall prefix the name of the element type contributed.
+Note that for a given parent element type identified by <tt>parentTypeId</tt>, one can set multiple <tt>childType</tt> elements which denotes they are all valid child types of the identified parent element.
-==== Set the value corresponding to the attribute of an element ====
+[[Category:Developer documentation]]

Difference between revisions of "Extending the Rodin Database"

Latest revision as of 15:43, 4 September 2013

Contents

Adding a New Attribute

Declaring its type

Declaring its relationship with existing elements

Accessing (Programmatically) the Newly Created Attribute

Getting the corresponding Java attribute kind

Checking for existence of the attribute for an element

Getting the value corresponding to the attribute of an element

Setting the value corresponding to the attribute of an element

Adding a New Element

Declaring its type

Declaring its relationship with existing elements

Navigation menu

Page actions

Page actions

Personal tools

Navigation

contribute

Search

Tools