Difference between pages "Extending the Rodin Structured Editor (How to extend Rodin Tutorial)" and "Generic Instantiation Plug-in User Guide"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Asiehsalehi
 
Line 1: Line 1:
{{Navigation|Previous= [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Extend the database]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
+
== Introduction ==
 +
The Generic Instantiation (GI) Feature plug-in allows to instantiate and reuse generic developments in other formal developments..
  
=== In this part ===
+
See the [http://wiki.event-b.org/index.php/Generic_Instantiation Generic Instantiation] page for technical details.
We will use the extension points provided by the plug-in <tt>org.eventb.ui</tt> to add our Probabilistic Attribute on events and the Bound Element to the Structured Editor.
 
  
=== Step 1 ===
+
== Installing and Updating ==
To structure a bit our development, we will separate the UI from the business layer.<br>
+
=== Setup ===
1. Create a new plug-in (here <tt>fr.systerel.rodinextension.sample.ui</tt>, and this time, select "This plug-in will make contributions to the UI" as it will be indeed the case here.<br>
+
The following steps will guide you through the setup process:
2. Add our business plug-in (<tt>fr.systerel.rodinextension.sample</tt>) to the dependencies as well as <tt>org.eventb.ui</tt> that provides the extensions points we want to use.
+
# Download Rodin for your platform.
 +
# Extract the downloaded zip file.
 +
# Start Rodin from the folder where you extracted the zip file in the previous step.
 +
# Install the Generic Instantiation Feature plug-in:
 +
## In the menu choose ''Help'' -> ''Install New Software...''
 +
## In the ''Work with'' dropdown list, choose the location URL: Rodin
 +
## Select the ''Generic Instantiation Feature'' feature under the ''Utilities'' category, then click the check box
 +
## Click ''Next'', after some time, the ''Install Details'' page appears
 +
## Click ''Next'' and accept the license
 +
## Click ''Finish''
 +
## A ''Security Warning'' window may appear: click ''OK''
 +
# Restart Rodin as suggested.
  
=== Step 2 ===
+
[[Image:GI_Install.jpg|center]]
1. Add the extension point <tt>org.eventb.ui.editorItems</tt>.<br>
 
At this point, we will start to add our extensions to the structured editor.<br>
 
  
=== Step 3 ===
+
Now you are ready to use the Generic Instantiation Feature plug-in.
First, let's add the probabilistic attribute to Event-B events.<br>
 
The probabilistic attribute can have two values : 'standard' (by default) and 'probabilistic'. Thus we need to create a 'choiceAttribute' extension.
 
Create a new 'choice attribute' extension:<br>
 
1. Give a unique ID to identify this attribute in the UI plug-in (such as <tt>fr.systerel.rodinextension.sample.ui.probabilistic</tt>).<br>
 
2. In typeID, give the ID reference of the probabilistic attribute in our business plug-in (here <tt>fr.systerel.rodinextension.sample.probabilistic</tt>).<br>
 
3. Set the ''required'' attribute to <tt>true</tt> as we want this attribute to appear by default in the structured editor when editing events.<br>
 
4. Create a class (using Eclipse assist, see [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Step4]]) to manipulate this attribute; this class should implements the interface <tt>org.eventb.ui.IAttributeManipulation</tt>.
 
'''//FIXME:This class should be implemented the following:'''
 
:Before doing any manipulation of the given <tt>IRodinElement</tt>, we have to cast this element as an <tt>IInternalElement</tt> (interface from <tt>org.rodinp.core</tt> providing access to element attributes. As we know that the element that will carry the probabilistic attribute is of type <tt>IEvent</tt>, and as <tt>IEvent</tt> implements the interface <tt>IInternalElement</tt>, let's create the following method.
 
  
  private IEvent asEvent(IRodinElement element) {
 
assert element instanceof IEvent;
 
return (IEvent) element;
 
}
 
:We also have to add the ID of the probabilistic attribute as a constant, as we will need it at various places in this class. We then add the following code:
 
  
  public static IAttributeType.Boolean PROB_ATTRIBUTE = RodinCore
+
=== Update ===
.getBooleanAttrType(QualProbPlugin.PLUGIN_ID + ".probabilistic");
+
The following steps will guide you through the update process:
 +
# In Rodin open the preferences (''Window'' -> ''Preferences'' or for Mac: ''Rodin'' -> ''Preferences'')
 +
# Find ''Install/Update'' -> ''Automatic Updates''
 +
# Select ''Automatically find new updates and notify me''
  
where <tt>IAttributeType.Boolean</tt> defines that our probabilistic attribute is actually coded as a boolean. We will implement the probabilistic attribute as followed:
+
As soon as Rodin finds a new update it will ask you if you would like to install it.
: if the event is probabilistic, the probabilistic attribute is set to <tt>true</tt>,
 
: otherwise, the event is standard (e.g. non probabilistic) so the probabilistic attribute is set to <tt>false</tt>.
 
  
There are several Types for attributes. See here from more details. '''//FIXME insert a link to IAttributeType doc'''
+
=== Release Notes ===
 +
See the [http://wiki.event-b.org/index.php/Generic_Instantiation_Release_History Generic Instantiation Feature Release History].
  
:Now let's fill the methods required to implement <tt>IAttributeManipulation</tt> :
+
== Instantiating ==
:1. <tt>getPossibleValues(IRodinElement element, IProgressMonitor monitor)</tt> should return an array of two constant values : 'standard' and 'probabilistic'.<br>
 
:2. <tt>getValue(IRodinElement element, IProgressMonitor monitor)</tt> should 'convert' the given element as an event (using <tt>asEvent</tt>) and return the value (retrieved by <tt>IInternalElement.getAttributeValue(PROB_ATTRIBUTE)</tt> corresponding to the state of the probabilistic attribute.(e.g. should return 'probabilistic' if the attribute has value <tt>true</tt>, <tt>false</tt> otherwise.<br>
 
:3. <tt>hasValue(IRodinElement element, IProgressMonitor monitor)</tt> should check if the given element converted as an event has a probabilistic attribute using the method <tt>IInternalElement.hasAttribute(PROB_ATTRIBUTE)</tt>.<br>
 
:4. <tt>removeAttribute(IRodinElement element, IProgressMonitor monitor)</tt> should convert the given element as an event, and use <tt>IInternalElement.removeAttribute(PROB_ATTRIBUTE, monitor)</tt>.<br>
 
:5. <tt>setDefaultValue(IRodinElement element, IProgressMonitor monitor)</tt> should convert the given element as an event, and do <tt>IInternalElement.setAttributeValue(PROB_ATTRIBUTE,</tt> '''false'''<tt>, monitor);</tt> as the default value for the probabilistic attribute is '''false'''.<br>
 
:6. finally, <tt>setValue(IRodinElement element, String value, IProgressMonitor monitor)</tt> should check that the given value correspond to the "probabilistic" string constant, and set the value of the element (previously converted as an event) to <tt>true</tt> if it is the case, or set the value to <tt>false</tt> otherwise.
 
  
Now we will add this attribute to events. To do so, we need to create an attribute relation that will link our probabilistic attribute to events. Return to the MANIFEST.MF extensions page.<br>
+
The example followed here to demonstrate the GI plug-in is from [[Image:Supporting_Reuse_of_Event-B_Developments_through_Generic_Instantiation.pdf | Supporting Reuseof Event-B Developments through Generic Instantiation]]
1. Create a new ''attributeRelation'' extension from the <tt>org.eventb.ui.editorItems</tt> extension point.<br>
+
=== Running the Instantiate Action ===
2. Enter <tt>org.eventb.core.event</tt> as ''elementTypeId'' in the attribute relation. This means that events will hold an attribute.<br>
+
The <tt>Instantiate</tt> action launches the instantiation wizard, which will perform the generic instantiation according to the preferences. It is available:
3. From this extension specify that the attribute held by events (among others) will be our probabilistic attribute by adding an ''attributeReference'' with the ID of our UI extension for the probabilistic attribute (here <tt>fr.systerel.rodinextension.sample.ui.probabilistic</tt>).
+
{|
 +
|-
 +
|1. Either from the toolbar of the Event-B explorer.  
 +
|2. Or from the contextual menu, when right-clicking on a machine.
 +
|-
 +
| valign="top" | [[Image:Ins_Explorer.jpg|center]]
 +
| valign="top" | [[Image:Ins_Contextual.jpg|center]]
 +
|}
  
=== Step 4 ===
+
=== Selecting the Pattern Machine and Problem Machine ===
Finally, let's add the Bound element to Event-B machines.<br>
+
* Pattern machine is the machine to be instantiated and reuse.
This step differs from the previous, as our element Bound is a new element (e.g. not an attribute). We want it to appear at top level in the structured editor, in the same way that are elements such as invariants, events, etc.
+
* Problem machine (optional) is the machine to be refined by the instantiating machine. In other words, the instantiating machine is a refinement of the problem machine.
  
We will then:  
+
[[Image:GI_Wizard.jpg|center]]
# Register the Bound element as an UI element (e.g. a new type of element).
 
# Set this element to be a 'child' of machine elements (e.g. Bound will belong to machine files).
 
# Set up a link to edit expressions of the Bound element in the UI. (Bound element carry one expression [they extend <tt>IExpressionElement</tt>]).
 
# Set up a link to edit comments of the Bound element in the UI. (Bound element carry one comment [they extend <tt>ICommentedElement</tt>]).
 
  
1. To register the Bound element in the UI, create an extension 'element':
+
=== Replacing Sets and Constants ===
:- In typeId, specify the ID of the extension Bound in our business plug-in (here <tt>fr.systerel.rodinextension.sample.bound</tt>).
+
All sets and constants from the pattern context must be replaced by the available sets and constants in the context seen by instantiating machine.
:- In imagePath, you can specify the icon to be displayed next to the element (we created here a folder 'icons' containing an default icon).
 
:- In prefix, type 'BOUND', this value will appear as the header of bound elements in the structured editor.
 
:- In 'defaultColumn' field, put the value '0' as to make the Bound element appear at top level in the outline of machines.
 
  
2. To set Bound element to be a child element of a machine:
+
[[Image:Replace_Set_Constant.jpg|center]]
:- Create an extension 'childRelation' using the extension point <tt>org.eventb.ui.editorItems</tt>.<br>
 
:- In ''parentTypeId'' field of this extension, enter "<tt>org.eventb.core.machineFile</tt>" to refer to machine files.<br>
 
:- Create a sub element for the child relation extension<br>
 
:- and refer to the ID of the bound in our business class (here <tt>fr.systerel.rodinextension.sample.bound</tt>).<br>
 
:- Put a priority of '65' to display Bound elements after ''variants'' but before ''events''. (Have a look at the ''childRelation'' for <tt>org.eventb.core.machineFile</tt> type in extension <tt>org.eventb.ui.editorItems</tt> of the package <tt>org.eventb.ui</tt> to view the priorities of other elements displayed in the structured editor).
 
  
3. To set up a link to edit the expression of a Bound element:
+
=== Renaming Variables and Events ===
:- Create an extension ''attributeRelation'' for our elementTypeId <tt>fr.systerel.rodinextension.sample.bound</tt>.
 
:- Add one ''attributeReference'' to <tt>org.eventb.ui.expression</tt> (descriptionID).
 
  
4. To set up a link to edit the comment of a Bound element:
+
[[Image:Rename_Var_Eve.jpg|center]]
:- Repeat addition of an ''attributeReference'' to the above ''attributeRelation'' but specifying <tt>org.eventb.ui.expression</tt> as descriptionID.
+
Variables and events (also event parameters) can be renamed.
 
 
You can now launch a Rodin product with our plug-ins imported and see the result:
 
 
 
[[Image:Extend_Rodin_Tuto_1_8_Used_ExtensionsExtended_UI.png]]
 
 
 
Congratulations! You are now able to edit the elements you added in Rodin Database.
 
 
 
{{Navigation|Previous= [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Extending the database]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
 
 
 
[[Category:Developer documentation|*Index]]
 
[[Category:Rodin Platform|*Index]]
 
[[Category:Tutorial|*Index]]
 

Revision as of 15:53, 17 December 2012

Introduction

The Generic Instantiation (GI) Feature plug-in allows to instantiate and reuse generic developments in other formal developments..

See the Generic Instantiation page for technical details.

Installing and Updating

Setup

The following steps will guide you through the setup process:

  1. Download Rodin for your platform.
  2. Extract the downloaded zip file.
  3. Start Rodin from the folder where you extracted the zip file in the previous step.
  4. Install the Generic Instantiation Feature plug-in:
    1. In the menu choose Help -> Install New Software...
    2. In the Work with dropdown list, choose the location URL: Rodin
    3. Select the Generic Instantiation Feature feature under the Utilities category, then click the check box
    4. Click Next, after some time, the Install Details page appears
    5. Click Next and accept the license
    6. Click Finish
    7. A Security Warning window may appear: click OK
  5. Restart Rodin as suggested.
GI Install.jpg

Now you are ready to use the Generic Instantiation Feature plug-in.


Update

The following steps will guide you through the update process:

  1. In Rodin open the preferences (Window -> Preferences or for Mac: Rodin -> Preferences)
  2. Find Install/Update -> Automatic Updates
  3. Select Automatically find new updates and notify me

As soon as Rodin finds a new update it will ask you if you would like to install it.

Release Notes

See the Generic Instantiation Feature Release History.

Instantiating

The example followed here to demonstrate the GI plug-in is from File:Supporting Reuse of Event-B Developments through Generic Instantiation.pdf

Running the Instantiate Action

The Instantiate action launches the instantiation wizard, which will perform the generic instantiation according to the preferences. It is available:

1. Either from the toolbar of the Event-B explorer. 2. Or from the contextual menu, when right-clicking on a machine.
Ins Explorer.jpg
Ins Contextual.jpg

Selecting the Pattern Machine and Problem Machine

  • Pattern machine is the machine to be instantiated and reuse.
  • Problem machine (optional) is the machine to be refined by the instantiating machine. In other words, the instantiating machine is a refinement of the problem machine.
GI Wizard.jpg

Replacing Sets and Constants

All sets and constants from the pattern context must be replaced by the available sets and constants in the context seen by instantiating machine.

Replace Set Constant.jpg

Renaming Variables and Events

Rename Var Eve.jpg

Variables and events (also event parameters) can be renamed.