Difference between pages "Current Developments" and "Rodin Developer Support"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Mathieu
 
imported>Laurent
(→‎Debugging: add pointers to Eclipse resources.)
 
Line 1: Line 1:
{{TOCright}}
+
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
This page sum up the known developments that are being done around or for the [[Rodin Platform]]. ''Please contributes informations about your own development to keep the community informed''
 
  
== Deploy Tasks ==
 
The following tasks were planned at some stage of the [[Deploy]] project.
 
=== Core Platform ===
 
==== New Mathematical Language ====
 
==== Rodin Index Manager ====
 
[[Systerel]] is in charge of this task.
 
{{details|Rodin Index Design|Rodin index design}}
 
  
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.
+
== Rodin Developer FAQ ==
  
==== Text Editor ====
+
see [[Developer FAQ]].
[[Düsseldorf]] has a prototype text-based editor for Event-B (courtesy of [[User:Fabian|Fabian]]). As of end of sempteber 2008, it still needs more work to fully integrate into Rodin.
 
  
[[Newcastle]] has another text editor based on EMF.  Among other things, it defines an EMF model of Event-B machines and contexts. At some point, the editor code is to be split into two plugins - an EMF adapater to rodin and the editor itself. Source code is currently available from [http://iliasov.org/editor-source.zip].
+
== Architecture of the Rodin Platform ==
  
=== Plug-ins ===
+
=== Rodin Platform Core ===
==== Requirement Management Plug-in ====
 
[[User:Jastram|Michael]] at [[Düsseldorf]] is in charge of the [[:Category:Requirement Plugin|Requirements Management Plug-in]].
 
  
{{See also|ReqsManagement|Requirements Tutorial|l1=Requirements Management Plug-in}}
+
* [[Database]]
  
This plug-in allows:
+
* [[Builder]]
* Requirements to be edited in a set of documents (independently from Rodin)
 
* Requirements to be viewed within Rodin
 
* Individual Requirements to be linked to individual Event-B-Entities
 
* A basic completion test to be performed
 
  
==== UML-B Plug-in ====
+
* [[Rodin Index Design]]
[[Southampton]] is in charge of [[UML-B]] plug-in.
 
  
* Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.
+
* [[Indexing System]]
  
*Allow user to allocate the name of the 'implicit contextual instance' used in a class. Events and Transitions owned by a class are implicitly acting upon an instance of the class which has formerly been denoted by the reserved word 'self'. This modification allows the modeller to override 'self' (which is now the default name) with any other identifier. This feature is needed to avoid name clashes when synchronising transitions into a single event. It also allows events to be moved between different classes (or outside of all classes) during refinement without creating name clashes.
+
* [[Undo Redo]]
  
* Better support for state machine refinement in UML-B. This revision to UML-B allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines.
+
* [[File Root Separation]]
  
==== ProB Plug-in ====
+
=== Event-B User Interface ===
[[Düsseldorf]] is in charge of [[ProB]].
 
<!-- {{details|ProB current developments|ProB current developments}} -->
 
  
===== Work already performed =====
+
The Event-B User Interface of the Roding Platform has two major components that are concerned with either [http://handbook.event-b.org/current/html/event_b_perspective.html modelling] in Event-B or [http://handbook.event-b.org/current/html/proving_perspective.html proving] properties of models.
  
We have now ported ProB to work directly on the Rodin AST. Animation is working and the user can now set a limited number of preferences.
+
* [http://handbook.event-b.org/current/html/event_b_perspective.html Modelling User Interface]
The model checking feature is now also accessible.
 
It is also possible to create CSP and classical B specification files. These files can be edited with BE4 and animated/model checked with ProB.
 
On the classical B side we have moved to a new, more robust parser (which is now capable of parsing some of the more complicated AtelierB
 
specifications from Siemens).
 
  
On the developer side, we have moved to a continuous integration infrastructure using CruiseControl. Rodin is also building from CVS in that infrastructure.
+
* [http://handbook.event-b.org/current/html/proving_perspective.html Proving User Interface]
  
===== Ongoing and future developments=====
+
Apart from these are more minor components.
  
We are currently developing a new, better user interface.
+
* [[Proof Purger Design|Proof Purger]] allows to delete unused proofs.  
We also plan to support multi-level animation with checking of the gluing invariant.
 
  
We have prototypes for several extensions working, but they need to be fully tested and integrated into the plugin:
+
* [[Proof Skeleton Design]] is a view that displays skeletons of existing proofs
* an inspector that allows the user to inspect complex predicates (such as invariants or guards) as well as expressions in a tree-like manner
 
* a graphical animator based on SWT that allows the user to design his/her own animations easily within the tool
 
* a 2D viewer to inspect the state space of the specification
 
  
==== B2Latex Plug-in ====
+
* [[Auto-Completion Design]] proposes a list of names to the user editing a model
[[Southampton]] is in charge of [[B2Latex]].
 
  
Kriangsak Damchoom will update the plug-in to add [[Event Extension|extensions of events]].
+
=== Event-B Component Library ===
  
==== Parallel Composition Plug-in ====
+
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 [http://handbook.event-b.org/current/html/proving_perspective.html proving user interface]).
[[Southampton]] is in charge of the [[Parallel Composition using Event-B]] .
 
  
The intention of the plug-in is to allow the parallel composition of events using Event-B syntax. The composition uses a value-passing style (shared event composition), where parameters can be shared/merged.
+
* [[Abstract Syntax Tree]]
  
This plug-in allows:
+
* [[Static Checker]]
* Selection of machines that will be part of the composition (''Includes'' Section)
 
* Possible selection of an abstract machine (''Refines'' Section)
 
* Possible inclusion of invariants that relate the included machines (''Invariant'' Section and use of the monotonicity )
 
* Invariants of included machines are conjoined.
 
* Selection of events that will be merged. The event(s) must come from different machines. At the moment, events with parameters with same name are merged. If it is a refinement composition, it is possible to choose the abstract event that is being refined.
 
* Initialisation event is the parallel composition of all the included machines' initialisations.
 
* For a composed event, the guards are conjoined and the all the actions are composed in parallel.
 
  
Currently, after the conclusion of the composition machine, a new machine can be generated, resulting from the properties defined on the composition file. This allows proofs to be generated as well as a visualisation of the composition machine file. In the future, the intention is to make the validation directly on the composition machine file directly where proofs would be generated ( and discharged) - the new machine generation would be optional. An event-b model for the validation/generation of proofs in currently being developed. Another functionality which should be quite useful for the composition (but not restricted to that) is '''renaming''':
+
* [[Proof Obligation Generator]]
  
* while composing, two machines may have variables with the same name for instance (which is not allowed for this type of composition). In order to solve this problem, one would have to rename one of the variables in order to avoid the clash, which would mean change the original machine. A possible solution for that would be to rename the variable but just on composition machine file, keeping the original machine intact. A renaming framework designed and developed by Stefan Hallerstede and Sonja Holl exists currently although still on a testing phase. The framework was developed to be used in a general fashion (not constrained to event-b syntax). The idea is to extend the development of this framework and apply to Event-B syntax (current development).
+
* [[Proof Manager]]
  
There is a prototype for the composition plug-in available, but only works for Rodin 0.8.2. A release for the Rodin 0.9 should be made available soon.
+
* [[Proof Simplification]]
  
==== Refactoring Framework Plug-in ====
+
== Extending Rodin ==
[[Southampton]] is in charge of the [[Refactoring Framework]].
 
  
The intention of the plug-in is to allow the renaming/refactoring of elements on a file (and possible related files). Although created to be used in a general way, the idea is to embed this framework on the Rodin platform, using Event-B syntax. This plug-in was initially designed and developed by Stefan Hallerstede and Sonja Holl.
+
* [[Developer Documentation]]
  
This plug-in allows:
+
* [[Plug-in Tutorial]]
* Defining extensions that can be used to select related files.
 
* Defining extensions that can be used to rename elements based on the type of file.
 
* Renaming of elements on a file and possible occurrences on related files.
 
* Generating of a report of possible problems (clashes) that can occur while renaming.
 
  
== Exploratory Tasks ==
+
* [[Extending the Rodin Database]]
=== One Single View ===
 
[[Maria]] is in charge of this exploratory work during is internship.
 
{{details|Single View Design|Single View Design}}
 
The goal of this project is to present everything in a single view in Rodin. So the user won't have to switch perspectives.
 
  
 +
* [[Extending the project explorer]]
  
 +
* [[Extending the Structure Editor]]
  
== Others ==
+
* [[Extending the Pretty Print Page]]
  
=== AnimB ===
+
* [[Extending the Proof Manager]]
[[Christophe]] devotes some of its spare time for this plug-in.
 
{{details|AnimB Current Developments|AnimB Current Developments}}
 
The current developments around the [[AnimB]] plug-in encompass the following topics:
 
;Live animation update
 
:where the modification of the animated event-B model is instantaneously taken into account by the animator, without the need to restart the animation.
 
;Collecting history
 
:The history of the animation will be collected.
 
  
=== Team-Based Development ===
+
* [[Extending the Index Manager]]
  
; Usage Scenarios
+
* [[Extending the Static Checker]]
: In order to understand the problem properly, [http://www.stups.uni-duesseldorf.de/ Düsseldorf] created a number of usage [[Scenarios for Team-based Development]].
+
 
: A page as also been opened for [[Scenarios for Merging Proofs|merging proofs scenarios]].
+
* [[Index Query]]
[[Category:Work in progress]]
+
 
 +
== 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/Developer_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 ===
 +
 
 +
There is nothing special to the Rodin platform as concerns debugging. This is just like debugging any Eclipse plug-in. See for instance [http://eclipse.org/resources/?sort=date&category=Debugging Eclipse Debugging Resources].
 +
 
 +
=== 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).
 +
 
 +
Create a new release folder in the FRS (On Sourceforge Rodin project website - Admin-file releases) noting the naming conventions (e.g. Plugin_<mypluginName>). Now you can upload your jar files using the controls on the releases webpage). Note that you should include a zip of the complete source projects to comply with Sourceforge rules.
 +
You should not repeat files that have not changed. 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.
 +
# From the sourceforge SVN repository, check out the project org.rodinp.updateSite.
 +
# Edit the  file site.xml to add your feature and plug-in archive paths ([[Details for Maintaining Main Rodin Update Site]])
 +
# Test the changes by performing the install into a Rodin installation, via the local update site in your workspace.
 +
# Commit the changes back into SVN
 +
# Upload the new version of the update site onto the Rodin webspace ([[Details for Uploading Main Rodin Update Site]]).  
 +
 
 +
 
 +
=== Upgrading and maintain ===
 +
 
 +
Please note that you should always keep an existing version of your plug-in for the antepenultimate version of Rodin when you want to perform some clean-up of your update site.
 +
Indeed, not all the users switch to the latest version of Rodin by the time of its release, and certainly would like to use your plug-ins anyway.
 +
 
 +
[[Category:Developer documentation]]
 +
[[Category:Rodin Platform]]

Revision as of 11:28, 28 October 2011

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

There is nothing special to the Rodin platform as concerns debugging. This is just like debugging any Eclipse plug-in. See for instance Eclipse Debugging Resources.

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).

Create a new release folder in the FRS (On Sourceforge Rodin project website - Admin-file releases) noting the naming conventions (e.g. Plugin_<mypluginName>). Now you can upload your jar files using the controls on the releases webpage). Note that you should include a zip of the complete source projects to comply with Sourceforge rules. You should not repeat files that have not changed. 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.

  1. From the sourceforge SVN repository, check out the project org.rodinp.updateSite.
  2. Edit the file site.xml to add your feature and plug-in archive paths (Details for Maintaining Main Rodin Update Site)
  3. Test the changes by performing the install into a Rodin installation, via the local update site in your workspace.
  4. Commit the changes back into SVN
  5. Upload the new version of the update site onto the Rodin webspace (Details for Uploading Main Rodin Update Site).


Upgrading and maintain

Please note that you should always keep an existing version of your plug-in for the antepenultimate version of Rodin when you want to perform some clean-up of your update site. Indeed, not all the users switch to the latest version of Rodin by the time of its release, and certainly would like to use your plug-ins anyway.