Difference between pages "Extending the Rodin Structured Editor (How to extend Rodin Tutorial)" and "Rodin Developer Support"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Jrloria
 
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= }}
+
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
  
−
=== In this part ===
 
−
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 ===
+
== Rodin Developer FAQ ==
−
To structure a bit our development, we will separate the UI from the business layer.<br>
 
−
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>
 
−
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.
 
  
−
=== Step 2 ===
+
see [[Developer FAQ]].
−
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 ===
+
== Architecture of the Rodin Platform ==
−
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) {
+
=== Rodin Platform Core ===
−
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
+
* [[Database]]
−
.getBooleanAttrType(QualProbPlugin.PLUGIN_ID + ".probabilistic");
 
  
−
where <tt>IAttributeType.Boolean</tt> defines that our probabilistic attribute is actually coded as a boolean. We will implement the probabilistic attribute as followed:
+
* [[Builder]]
−
: 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'''
+
* [[Rodin Index Design]]
  
−
:Now let's fill the methods required to implement <tt>IAttributeManipulation</tt> :
+
* [[Indexing System]]
−
: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>
+
* [[Undo Redo]]
−
1. Create a new ''attributeRelation'' extension from the <tt>org.eventb.ui.editorItems</tt> extension point.<br>
 
−
2. Enter <tt>org.eventb.core.event</tt> as ''elementTypeId'' in the attribute relation. This means that events will hold an attribute.<br>
 
−
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>).
 
  
−
=== Step 4 ===
+
* [[File Root Separation]]
−
Finally, let's add the Bound element to Event-B machines.<br>
 
−
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.
 
  
−
We will then:
+
=== Event-B User Interface ===
−
# Register the Bound element as an UI element (e.g. a new type of element in the UI).
 
−
# 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':
+
The Event-B User Interface of the Roding Platform has two major components that are concerned with either [[Modelling User Interface|modelling]] in Event-B or [[Proving User Interface|proving]] properties of models.
−
:- In typeId, specify the ID of the extension Bound in our business plug-in (here <tt>fr.systerel.rodinextension.sample.bound</tt>).
 
−
:- 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:
+
* [[Modelling User Interface]]
−
:- 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:
+
* [[Proving User Interface]]
−
:- 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:
+
Apart from these are more minor components.
−
:- Repeat addition of an ''attributeReference'' to the above ''attributeRelation'' but specifying <tt>org.eventb.ui.expression</tt> as descriptionID.
 
  
−
You can now launch a Rodin product with our plug-ins imported and see the result:
+
* [[Proof Purger Design|Proof Purger]] allows to delete unused proofs.
  
−
[[Image:Extend_Rodin_Tuto_1_8_Used_ExtensionsExtended_UI.png]]
+
* [[Proof Skeleton Design]] is a view that displays skeletons of existing proofs
  
−
Congratulations! You are now able to edit the elements you added in Rodin Database.
+
* [[Auto-Completion Design]] proposes a list of names to the user editing a model
  
−
{{Navigation|Previous= [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Extending the database]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
+
=== Event-B Component Library ===
  
−
[[Category:Developer documentation|*Index]]
+
Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a [[Static Checker|static checker]]. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The [[Proof Obligation Generator|proof obligation generator]] uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the [[Proof Manager|proof manager]] attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the [[Proving User Interface|proving user interface]]).
−
[[Category:Rodin Platform|*Index]]
+
 
−
[[Category:Tutorial|*Index]]
+
* [[Abstract Syntax Tree]]
 +
 
 +
* [[Static Checker]]
 +
 
 +
* [[Proof Obligation Generator]]
 +
 
 +
* [[Proof Manager]]
 +
 
 +
* [[Proof Simplification]]
 +
 
 +
== Extending Rodin ==
 +
 
 +
* [[Developer Documentation]]
 +
 
 +
* [[Plug-in Tutorial]]
 +
 
 +
* [[Extending the Rodin Database]]
 +
 
 +
* [[Extending the project explorer]]
 +
 
 +
* [[Extending the Structure Editor]]
 +
 
 +
* [[Extending the Pretty Print Page]]
 +
 
 +
* [[Extending the Proof Manager]]
 +
 
 +
* [[Extending the Index Manager]]
 +
 
 +
* [[Extending the Static Checker]]
 +
 
 +
* [[Index Query]]
 +
 
 +
== Useful Hints ==
 +
 
 +
=== Version Control ===
 +
 
 +
All sources of the core Rodin platform (and of some plug-ins) are managed under version control in SourceForge.  The repository currently used is Subversion and can be accessed using URL [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp].
 +
 
 +
=== Building against a version of Rodin ===
 +
 
 +
To develop extensions to the Rodin platform your code build needs access to a consistent (version-wise) set of Rodin platform plug-ins. (Don't just check out the latest versions from 'Head' because it may be under development and in an inconsistent state). An easy way to set up your workspace is to import the Rodin platform source code from SVN into your workspace using the 'Releng' plug-in. See [http://wiki.event-b.org/index.php/FAQ#Installing_the_sources_from_Subversion_in_Eclipse Installing the sources from Subversion in Eclipse] for further instructions.
 +
 
 +
Alternatively, you can set your plugin development target platform to any Rodin installation you have installed (Eclipse-Preferences-Plug-in Development-Target Platform). This is useful as a final test that everything will work once installed into Rodin but because it uses a 'built' platform, you don't get access to the Rodin source code (e.g. for de-bugging).
 +
 
 +
=== Testing ===
 +
 
 +
=== Debugging ===
 +
 
 +
=== Publishing ===
 +
 
 +
A Plug-in developed for the Rodin Platform will normally consist of a collection of eclipse 'plugin' projects and a single eclipse 'feature' project. The feature project contains branding information such as logo's icons and licensing details. It is also used to identify your Plug-in so that users can install it. To build your Plug-in use an eclipse 'site' project. This will build the jar files for your plugin projects and a jar for your feature. See eclipse documentation for more details.
 +
 
 +
Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform).
 +
 
 +
First upload your jar files onto the Sourceforge uploads area and then create a new release in the FRS (Admin-file releases). Note that you should include a zip of the complete source projects to comply with Sourceforge rules. You must not repeat files that have not changed. Sourceforge does not allow you to upload multiple copies of the same jar file. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release.
 +
See here for details:- http://alexandria.wiki.sourceforge.net/File+Release+System+-+Offering+Files+for+Download
 +
 
 +
Finally, the update site must be updated to redirect the update requests to the files on the FRS.
 +
(Currently this is done by Colin Snook on request - see Rodin developers page for contact details).
 +
 
 +
[[Details for Maintaining Main Rodin Update Site]]
 +
 
 +
 
 +
[[Category:Developer documentation]]
 +
[[Category:Rodin Platform]]

Revision as of 07:53, 2 June 2010

The Developer Support provides resources for developing plug-ins for the Rodin Platform.


Rodin Developer FAQ

see Developer FAQ.

Architecture of the Rodin Platform

Rodin Platform Core

Event-B User Interface

The Event-B User Interface of the Roding Platform has two major components that are concerned with either modelling in Event-B or proving properties of models.

Apart from these are more minor components.

Event-B Component Library

Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an abstract syntax tree. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a static checker. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The proof obligation generator uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the proof manager attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the proving user interface).

Extending Rodin

Useful Hints

Version Control

All sources of the core Rodin platform (and of some plug-ins) are managed under version control in SourceForge. The repository currently used is Subversion and can be accessed using URL https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp.

Building against a version of Rodin

To develop extensions to the Rodin platform your code build needs access to a consistent (version-wise) set of Rodin platform plug-ins. (Don't just check out the latest versions from 'Head' because it may be under development and in an inconsistent state). An easy way to set up your workspace is to import the Rodin platform source code from SVN into your workspace using the 'Releng' plug-in. See Installing the sources from Subversion in Eclipse for further instructions.

Alternatively, you can set your plugin development target platform to any Rodin installation you have installed (Eclipse-Preferences-Plug-in Development-Target Platform). This is useful as a final test that everything will work once installed into Rodin but because it uses a 'built' platform, you don't get access to the Rodin source code (e.g. for de-bugging).

Testing

Debugging

Publishing

A Plug-in developed for the Rodin Platform will normally consist of a collection of eclipse 'plugin' projects and a single eclipse 'feature' project. The feature project contains branding information such as logo's icons and licensing details. It is also used to identify your Plug-in so that users can install it. To build your Plug-in use an eclipse 'site' project. This will build the jar files for your plugin projects and a jar for your feature. See eclipse documentation for more details.

Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform).

First upload your jar files onto the Sourceforge uploads area and then create a new release in the FRS (Admin-file releases). Note that you should include a zip of the complete source projects to comply with Sourceforge rules. You must not repeat files that have not changed. Sourceforge does not allow you to upload multiple copies of the same jar file. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release. See here for details:- http://alexandria.wiki.sourceforge.net/File+Release+System+-+Offering+Files+for+Download

Finally, the update site must be updated to redirect the update requests to the files on the FRS. (Currently this is done by Colin Snook on request - see Rodin developers page for contact details).

Details for Maintaining Main Rodin Update Site

Retrieved from ‘https://wiki.event-b.org/index.php?title=Extending_the_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)&oldid=7067’