Difference between pages "D45 Scalability" and "Extending the Rodin Database"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Tommy
 
Line 1: Line 1:
= Overview =
+
There are different ways to extend the Rodin Database:
* '''Improved Performance''' According to the refocus mentionned in the [[D45_General_Platform_Maintenance#Motivations| General Platform Maintenance]] chapter, much of the reworking efforts performed on the core plateform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed in a separate chapter.
+
* adding a new attribute.
* '''Design pattern management / Generic Instantiation''' {{TODO}} An overview of the contribution about the design pattern management / Generic Instantiation (Thai Son Hoang)
+
* adding a new element.
* '''Edition''' It appeard along DEPLOY, the models defined by pilots becoming industrial sized due to the level of complexity reached, that the edition became a central concern.  
 
:*The legacy structured editor based on a form edition specific achitecture reach its limits in responsivness and hence in usability when being constrained to display a huge amount of graphical elements. Industrial partners found this issue significant regarding the adoption of the rodin platform in industry and that is why providing a new editor that would solve them has been a main task during this last year of the DEPLOY project.
 
:*Camille textual editor had to tackle challenges related to ressources mapping and management for projects of industrial size mentionned above or even the design of extension capabilities, that became a major concern since the grammar could be extended with theories.
 
  
= Motivations =
+
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.
  
== Improved Performance ==
+
== Adding a New Attribute ==
It appeared that the various DEPLOY partners encountered several major issues while editing large models. Some were related to the core code of the Rodin platform, causing crashes, loss of data, corruption in models. Some other were related to the UI causing platform hanging, and sometimes leading to its freezing which required sometimes to kill the Rodin process, thus also leading to potential loss of data and corruption in models. Hence, it appeared necessary to solve such issues before the end of DEPLOY.
+
=== Declaring its type ===
  
== Design Pattern Management / Generic Instantiation  ==
+
The extension point <code>org.rodinp.core.attributeTypes</code> allows to declare a new attribute. The element to add is <code>attributeType</code>.
{{TODO}} ''To be completed by Thai Son Hoang''
 
== Edition ==
 
* The motivations behind the creation of the new textual structured editor mainly concern performance but not only. From the growing size of complexity reached in models inducing a growing of their physical size lead the platform to its limits. Two major kinds of failures were faced when developing such models:
 
:* failures occuring on windows platforms, the mostly used system, when reaching the operating system limit number of graphical elements in memory allowed to be displayed at once. This bug used to crash the Rodin platform, and it appeared necessary to control the number of graphical elements needed to display the model elements. Architectures sparing these graphical elements should be thus favoured.
 
:* failures due to the high consumption of memory by the heavy graphical elements used by the forms of legacy editor.
 
:Moreover, it appeared important to visualize some elements that are not part of the current level of modelling, but are linked to it, for exemple, the actions in an abastract event, or its guards. Such elements are called the "inherited" elements, or "implicit children". The legacy structured editor being directly interfaced with the underlying Event-B models in database, it was difficult and tricky to modify it in order to display inherited elements. This was one more argument to go for a new editor based on a intermediary representation of the models.
 
:Another motivation to go for another editor was to get a more modest and ergonomic way to visualize and edit the models. The models being presented through styled text pretty printing and the edition thightly derived from a textual edition.
 
  
* The motivations about Camille evolution {{TODO}} Ingo Weigelt.
+
In the example below, we assume that the extensions are developed within a plug-in project with name '''org.eventb.developer.examples'''
  
= Choices / Decisions =
+
The following extension declares a new string attribute.
== Improved Performance ==
+
<extension
SYSTEREL lead a two phase investigation to have a better idea of the work to be done. Each phase being followed by some refactoring of the code. Out of the early investigation, a cause and effect relationship has been found between perfomance loss and the various reported bugs, such as "platform hanging" bugs or even "no more handle" bugs related to the high consumption of graphical elements on Windows platforms. Indeed, it appeared that solving the performance issues sometimes solved induced bugs as well which made the scalability improvement tasks emcompass the maintenance goals.<br>
+
        point="org.rodinp.core.attributeTypes">
Later, a deeper investigation was performed, to indentify and tackle the remaining performance issues. Profiling and code review were the two techniques used. The profiling strategy allowed to get a better localisation of the performance loss in both UI and core code while the code review helped to understand the intrinsic misuses or drawbacks of particular components and/or architectures.
+
      <attributeType
A good example, was the Event-B built-in editor based on form editors with a high use of greedy graphical components. Such architecture appeard to be weak when it was needed to display industrial size models. This affected the modelling experience with some long, and really annoying to the user, reaction lags. To solve such issue, it has been chosen to refactor the editors using a textual representation which was a light-weight graphical alternative to lower the number of needed components.
+
            id="stringAttr"
 +
            kind="string"
 +
            name="%eventBStringAttribute">
 +
      </attributeType>
 +
  </extension>
  
== Design Pattern Management / Generic Instantiation  ==
+
* The attribute has an ID (which should be always unique) which also contain the project name, i.e. <code>org.eventb.developer.examples.stringAttr</code>. This unique ID will be used for access the value corresponding to this attribute of an element later.  
{{TODO}} ''To be completed by Thai Son Hoang''
 
== Edition ==
 
* Rodin Editor
 
As previously said, the legacy editor drawbacks mainly come from its greedy components and structure. However, a structured way to edit the models (based on a database storage) seams still particularly appropriate. This mainly explains why a new structured editor, the Rodin Editor, has been build to keep a structured edition of the model contents on the basis of the improvements made to the Proving UI. In fact, the textual component, the SWT StyledText, used in this latter UI element significantly improved the modelling experience. Hence, every element modelled in the Rodin editor is described as text. Not only this lightened the presentation, but also side stepped the use of a significant amount of greedy graphical components. Although using this technique makes models look like plain text, it is just a sort of pretty printing and they remain edited and stored by the database. The edition is then possible through the use of a unique additional graphical component that overlays the presentation of the element to edit. This drastically reduces the memory consumption as well as the number of needed graphical components because at most two of them are needed!<br>
 
The first public version (0.5.0) of the Rodin Editor as been released on the 13/07/2011 as a plug-in of the Rodin platform. This decision has been made in order to let the plug-in in incubation.
 
  
* Camille
+
* The name of the attribute is a string that could be externalised to be used for displaying to the users in the future.
{{TODO}} Ingo Weigelt
 
  
= Available Documentation =
+
* There are five different attribute kinds: ''boolean'', ''handle'', ''integer'', ''long'', ''string''.
* {{TODO}} Links for Improved Performance
 
* {{TODO}} Links for Design Pattern Management / Generic Instantiation
 
* {{TODO}} Links for Edition
 
:* Rodin Editor
 
  
:* Camille
+
=== 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.
  
= Status =
+
The following extension declares our new string attribute <tt>stringAttr</tt> as carried by "variable" elements.
== Improved Performance ==
 
The refactoring made on both core code and UI code allowed to gain up to 25 times speed-up on the UI, and almost a 2 times speed-up in the core code, making the platform usable in an industrial sized context.<br>
 
  
== Design Pattern Management / Generic Instantiation  ==
+
<extension
{{TODO}} ''To be completed by Thai Son Hoang''
+
        point="org.rodinp.core.itemRelations">
== Edition ==
+
      <relationship parentTypeId="org.eventb.core.variable">
{{TODO}} ''To be completed by Thomas Muller, Ingo Weigelt''
+
        <attributeType typeId="org.eventb.core.variable">
 +
        </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.
  
= References =
+
=== Accessing (Programmatically) the Newly Created Attribute ===
<references/>
 
  
[[Category:D45 Deliverable]]
+
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).
 +
 
 +
* <code>org.rodinp.core.IAttributeType.Boolean RodinCore.getBoolAttrType(String ID)</code>
 +
 +
* <code>org.rodinp.core.IAttributeType.Handle RodinCore.getHandleAttrType(String ID)</code>
 +
 
 +
* <code>org.rodinp.core.IAttributeType.Integer RodinCore.getIntegerAttrType(String ID)</code>
 +
 
 +
* <code>org.rodinp.core.IAttributeType.Long RodinCore.getLongAttrType(String ID)</code>
 +
 
 +
* <code>org.rodinp.core.IAttributeType.String RodinCore.getStringAttrType(String ID)</code>
 +
 
 +
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).
 +
 
 +
* <code>org.rodinp.core.IAttributeType RodinCore.getAttrubuteType(String ID)</code>
 +
 
 +
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. <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.
 +
 
 +
==== 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 IInternalElement.getAttributeValue(IAttributeType.Boolean)</code>
 +
 
 +
* <code>IRodinElement IInternalElement.getAttributeValue(IAttributeType.Handle)</code>
 +
 
 +
* <code>int IInternalElement.getAttributeValue(IAttributeType.Integer)</code>
 +
 
 +
* <code>long IInternalElement.getAttributeValue(IAttributeType.Long)</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.xxxx.myElement">
 +
        </childType>
 +
      </relationship>
 +
</extension>
 +
[[Category:Developer documentation]]

Revision as of 15:38, 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.core.variable">
        </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.xxxx.myElement">
        </childType>
     </relationship>
</extension>