Difference between pages "Rodin Developer Support" and "Rodin Platform 3.0.0 External Plug-ins"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
 
imported>Son
 
Line 1: Line 1:
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
+
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>IMPORTANT<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- To set your plug-in state to available, please use : <span style="color:green">available</span> -->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>IMPORTANT<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
<!-- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>><<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-->
 +
==== Rodin Update Site ====
  
 +
http://rodin-b-sharp.sourceforge.net/updates
  
== Rodin Platform Overview ==
+
{{SimpleHeader}}
 +
|-
 +
! scope=col |  || Plug-in name || Version ||  Status || MCV* || Release Date || Contact || Additional info
 +
|-
 +
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Statemachines|Event-B State-machines]] || 2.1.0 ||  <span style="color:green"> available</span> || || 27th May 2014 || [mailto:cfs@ecs.soton.ac.uk email] || State-machines contained in Event-B Machines
 +
|-
 +
| [[Image:IUMLB_big.png|30px]] ||[[Event-B_Statemachines|Event-B State-machine Animation]] || 2.1.1 || <span style="color:green"> available</span> || || 27th May 2014 || [mailto:vs2@ecs.soton.ac.uk email] || Compatible with Event-B statemachines  2.1.x and ProB 3.0.x.
 +
|-
 +
| [[Image:Umlb32.gif|30px]] || [[UML-B|UML-B]] || 2.2.0 ||  <span style="color:#8B4513"> not checked</span> || || 9th Feb. 2011 || [mailto:cfs@ecs.soton.ac.uk email] || Original UML-B modelling environment
 +
|-
 +
| [[Image:Umlb32.gif|30px]] ||[[UML-B_-_Statemachine_Animation|UML-B Statemachine Animation]] || 1.1.0 || <span style="color:#8B4513"> not checked</span> || || 15th Feb. 2011 || [mailto:vs2@ecs.soton.ac.uk email] || Compatible with UML-B 2.2 and ProB 2.1.
 +
|-
 +
| ||[[EMF_framework_for_Event-B|Event-B EMF framework]] || 4.1.0 ||<span style="color:green"> available</span>|| || 27th May 2014  || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
 +
|-
 +
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for extensions]] || 3.1.0 ||<span style="color:green"> available</span>|| || 27th May 2014  || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers.  End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
 +
|-
 +
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for diagrams]] || 4.1.0 ||<span style="color:green"> available</span>|| || 27th May 2014  || [mailto:cfs@ecs.soton.ac.uk email] ||  Provided for plug-in developers.  End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
 +
|-
 +
| || [[Isabelle for Rodin]] || || <span style="color:#8B4513"> not checked</span> || 2.x.x || || ||
 +
|-
 +
| [[Image:Rose.gif|30px]]||[[Rose_(Structured)_Editor|Rose]] || 1.5.0 ||<span style="color:green"> available</span>|| || 27th May 2014 || [mailto:cfs@ecs.soton.ac.uk email] || Mainly useful for Plug-in developers. Tree-structured editor that handles extensions without modification
 +
|-
 +
| ||[[Records|Records]] ||  1.0.1 ||<span style="color:#8B4513"> not checked</span> || || 16th Oct. 2010 || [mailto:cfs@ecs.soton.ac.uk email] || No longer actively supported - please email if you wish to use this plugin
 +
|-
 +
| ||[[EMF_Compare_Editor_installation|Teamwork]] || 1.1.0 || <span style="color:#8B4513"> not checked</span> || || 15th Oct. 2010 || [mailto:cfs@ecs.soton.ac.uk email] || No longer actively supported - please email if you wish to use this plugin
 +
|-
 +
| ||[[Parallel_Composition_using_Event-B | Shared Event Composition]] || 1.6.1 || <span style="color:#8B4513"> not checked</span> || || 04th July 2013 || [mailto:asf08rr@ecs.soton.ac.uk email] || Compatible with Rodin 2.8.
 +
|-
 +
| ||[[Refactoring Framework | Refactory ]]|| 1.3.0 || <span style="color:green"> available</span>|| 3.x.x || 6th May 2014 || [mailto:asf08r@ecs.soton.ac.uk email] || Compatible with Rodin 3.0.
 +
|-
 +
| [[Image:DecompositionPlug-in_logo.png|30px]] || [[Decomposition Plug-in User Guide | Decomposition]] || 1.2.6 || <span style="color:#8B4513"> not checked</span>|| || 11th Dec 2012 || [mailto:asf08r@ecs.soton.ac.uk email] || Compatible with Rodin 2.8.
 +
|-
 +
| [[Image:Project diagram icon s.png|30px]]||[[Project_Diagram|Project Diagram]]|| 1.0.0 || <span style="color:#8B4513"> not checked</span> || || 15th Nov. 2010 || [mailto:vs2@ecs.soton.ac.uk email] || Machine - Context relationship diagram
 +
|-
 +
| || Relevance Filter || 1.1.1 || <span style="color:#8B4513"> not checked</span> || 2.x.x || || ||
 +
|-
 +
| || [[Theory Plug-in| Theory Plug-in]] ||v1.0 ||<span style="color:#8B4513"> not checked</span>|| 2.2 || 8th July 2011|| [mailto:im06r@ecs.soton.ac.uk email] || Compatible with Rodin 2.2 only.
 +
|-.x
 +
| || [[Code Generation Activity | Code Generation]] || 0.2.5 ||<span style="color:#8B4513"> not checked</span>||  || 29th Aug. 2013|| [mailto:ae2@ecs.soton.ac.uk email] || For Java, Ada, and OpenMP C code
 +
|-.x
 +
|-
 +
| || [[SMT_Plug-in | SMT Solvers ]] || 1.2.1 || <span style="color:green"> available</span> || 3.0 || 14th March 2014|| [mailto:laurent.voisin@systerel.fr Laurent Voisin]  ||
 +
|-
 +
| || [[Event-B Qualitative Probability User Guide | Qualitative Probability]] || 0.2.1 || <span style="color:#8B4513"> not checked</span> || 2.3.x || 23rd November 2011 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
 +
|-
 +
| || [[B2Latex | B2Latex export]] || 0.5.4 || <span style="color:green"> available</span> || 2.5.x || 16th April 2012 || [mailto:thomas.muller@systerel.fr email] ||
 +
|-
 +
| || [[Generic Instantiation Plug-in User Guide | Generic Instantiation (Soton)]] || 1.0.1 || <span style="color:#8B4513"> not checked</span> || || 05th March 2013 || [mailto:asf08r@ecs.soton.ac.uk email] ||
 +
|}
  
== Architecture of the Rodin Platform ==
+
==== B Method Update Site ====
  
=== Rodin Platform Core ===
+
http://methode-b.com/update_site/atelierb_provers
  
* [[Database]]
+
{{SimpleHeader}}
 +
|-
 +
! scope=col | ||Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
 +
|-
 +
| [[Image:atelierB.png]]||Atelier-B provers || 2.1.0 || <span style="color:green">available</span> || 3.x.x || 18th March 2014 || [mailto:contact@atelierb.eu email] || Read the instructions concerning 64-bit compatibility : [[Rodin_Platform_3.0_Release_Notes#Requirements_-_Compatibility | here ]]
 +
|}
  
* [[Builder]]
+
==== Other Update Sites ====
 +
{{SimpleHeader}}
 +
|-
 +
! scope=col | ||Plug-in name || Version || Status || MCV* || Release Date || Contact || Additional info
 +
|-
 +
| [[Image:AnimB.png|30px]] || [[AnimB]] ||  || <span style="color:#8B4513"> not checked</span>|| || || [mailto:christope.metayer@animb.org Christophe Métayer] || Use the update site <tt>http://www.animb.org/updatesite</tt>
 +
|-
 +
| ||[[Camille_Editor|Camille]] || 2.1.5 ||<span style="color:#8B4513"> not checked</span>|| 2.5.x || 27th July 2011 || [mailto:michael@jastram.de Michael Jastram] || Use the Camille update site. <tt>http://www.stups.uni-duesseldorf.de/camille_updates</tt><br><span style="color:#8B4513">Make sure to install the Event-B EMF Framework version 3.7.0 or greater.</span>
 +
|-
 +
| [[Image:Mlogo_big.png|30px]] || [[Modularisation_Plug-in|Modularisation]] ||  || <span style="color:#8B4513"> not checked</span>|| 2.x.x || || [mailto:alexei.iliasov@ncl.ac.uk email] || Use the update site <tt>http://www.iliasov.org/modplugin</tt>
 +
|-
 +
| || [[Generic Instantiation User Guide | Generic Instantiation]] || 1.1.0 || <span style="color:green">available</span> || 3.0.x || 1 August 2014 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] || Use the update site <tt>http://gen-inst.sourceforge.net/updates</tt>
 +
|-
 +
| ||[[Group_refinement_plugin|Group refinement]] ||  || <span style="color:#8B4513"> not checked</span>|| 2.x.x || || [mailto:alexei.iliasov@ncl.ac.uk email] || Use the update site <tt>http://iliasov.org/refplugin</tt>
 +
|-
 +
| ||[[Flows|Flows/Use case extension]] ||  || <span style="color:#8B4513"> not checked</span>|| 2.x.x || || [mailto:alexei.iliasov@ncl.ac.uk email] || Use the update site <tt>http://iliasov.org/usecase</tt>
 +
|-
 +
| [[Image:Prob_eventb_wiki_logo.png|30px]]||[http://www.stups.uni-duesseldorf.de/ProB ProB] || 3.0.1|| <span style="color:green">available</span> || 3.0.x || 18th March 2014 || [mailto:jens@bendisposto.de Jens Bendisposto] || Use the ProB update site.  <tt>http://www.stups.uni-duesseldorf.de/prob_updates_rodin3</tt><br>The Plug-in includes [http://www.stups.uni-duesseldorf.de/BMotionStudio BMotion Studio]<br>For older Rodin versions use <tt>http://www.stups.uni-duesseldorf.de/prob_updates</tt>
 +
|-
 +
| [[Image:ProR_logo.png|32px]] || [http://pror.org ProR] || 0.3.2 ||<span style="color:#8B4513"> not checked</span> || 2.6.x || 08/01/2012  || [mailto:michael@jastram.de Michael Jastram] || Update site: <tt>http://update.formalmind.com/rodin</tt><br>Project web site: <tt>http://eclipse.org/rmf</tt>
 +
|-
 +
| [[Image:MBT_for_Event-B_Logo_Medium.png]] ||[[MBT_plugin|MBT plugin]] || 2.0 || <span style="color:#8B4513"> not checked</span>|| 2.7.x || 5th of March 2012 || [mailto:alin.stefanescu@upit.ro Alin Stefanescu] || Use the update site <tt>http://fmi.upit.ro/mbt_plugin</tt>
 +
|-
 +
| ||[[Mode/FT Views]]|| 1.0.2 || <span style="color:#8B4513"> not checked</span>|| 2.4.x || 4th July 2011 || [mailto:ilya.lopatkin@ncl.ac.uk Ilya Lopatkin] || Update site: <tt>http://rodinmodeftview.sourceforge.net/</tt>
 +
|-
 +
| ||[[Transformation patterns]]|| 1.0 || <span style="color:#8B4513"> not checked</span>|| 2.x.x || 4th July 2011 || [mailto:ilya.lopatkin@ncl.ac.uk Ilya Lopatkin] || Update site: <tt>http://rodinmodeftview.sourceforge.net/</tt>
 +
|
 +
|-
 +
| [[Image:EHDL_Ver2.png|center|28px]] ||[[VHDL code generator]]|| 2.0.2 || <span style="color:#8B4513"> not checked</span>|| 2.x.x || 12th March 2012 || [mailto:Sergey.Ostroumov@abo.fi Sergey Ostroumov] || Update site: <tt>http://www.eventb-to-vhdl.tk/</tt>
 +
|}
 +
<nowiki>*MCV stands for the Rodin's Maximum Compatible Version</nowiki>
  
* [[Indexing System]]
+
==== Known plug-in incompatibilities ====
 +
It unfortunately might exists some incompatibilities between plug-ins. This list might be non exhaustive and is updated accorded to user experiences.
 +
If you encounter some conflict while installing or using plug-ins, please send a mail to the [mailto:rodin-b-sharp-user@lists.sourceforge.net Rodin User List] or feel free to complete the following table.
 +
{{SimpleHeader}}
 +
|-
 +
! scope=col |  Plug-in name || Incompatible with
 +
|-
 +
|}
  
=== Event-B User Interface ===
+
[[Category:Rodin Platform Release Notes]]
 
 
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.
 
 
 
* [[Modelling User Interface]]
 
 
 
* [[Proving User Interface]]
 
 
 
=== 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 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]]).
 
 
 
* [[Abstract Syntax Tree]]
 
 
 
* [[Static Checker]]
 
 
 
* [[Proof Obligation Generator]]
 
 
 
* [[Proof Manager]]
 
 
 
== Extending Rodin ==
 
 
 
* [[Getting Started]]
 
 
 
* [[Plug-in Tutorial]]
 
 
 
* [[Extending the project explorer]]
 
 
 
* [[Extending the Proof Manager]]
 
 
 
* [[Extending the Index Manager]]
 
 
 
* [[Index Requester]]
 
 
 
== Useful Hints ==
 
 
 
=== 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]]
 
 
 
== Rodin Developer FAQ ==
 
 
 
[[Category:Developer documentation]]
 
[[Category:Rodin Platform]]
 

Revision as of 01:14, 18 August 2014

Rodin Update Site

http://rodin-b-sharp.sourceforge.net/updates


Plug-in name Version Status MCV* Release Date Contact Additional info
IUMLB big.png Event-B State-machines 2.1.0 available 27th May 2014 email State-machines contained in Event-B Machines
IUMLB big.png Event-B State-machine Animation 2.1.1 available 27th May 2014 email Compatible with Event-B statemachines 2.1.x and ProB 3.0.x.
Umlb32.gif UML-B 2.2.0 not checked 9th Feb. 2011 email Original UML-B modelling environment
Umlb32.gif UML-B Statemachine Animation 1.1.0 not checked 15th Feb. 2011 email Compatible with UML-B 2.2 and ProB 2.1.
Event-B EMF framework 4.1.0 available 27th May 2014 email Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
Event-B EMF support for extensions 3.1.0 available 27th May 2014 email Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
Event-B EMF support for diagrams 4.1.0 available 27th May 2014 email Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
Isabelle for Rodin not checked 2.x.x
Rose.gif Rose 1.5.0 available 27th May 2014 email Mainly useful for Plug-in developers. Tree-structured editor that handles extensions without modification
Records 1.0.1 not checked 16th Oct. 2010 email No longer actively supported - please email if you wish to use this plugin
Teamwork 1.1.0 not checked 15th Oct. 2010 email No longer actively supported - please email if you wish to use this plugin
Shared Event Composition 1.6.1 not checked 04th July 2013 email Compatible with Rodin 2.8.
Refactory 1.3.0 available 3.x.x 6th May 2014 email Compatible with Rodin 3.0.
DecompositionPlug-in logo.png Decomposition 1.2.6 not checked 11th Dec 2012 email Compatible with Rodin 2.8.
Project diagram icon s.png Project Diagram 1.0.0 not checked 15th Nov. 2010 email Machine - Context relationship diagram
Relevance Filter 1.1.1 not checked 2.x.x
Theory Plug-in v1.0 not checked 2.2 8th July 2011 email Compatible with Rodin 2.2 only.
Code Generation 0.2.5 not checked 29th Aug. 2013 email For Java, Ada, and OpenMP C code
SMT Solvers 1.2.1 available 3.0 14th March 2014 Laurent Voisin
Qualitative Probability 0.2.1 not checked 2.3.x 23rd November 2011 Thai Son Hoang
B2Latex export 0.5.4 available 2.5.x 16th April 2012 email
Generic Instantiation (Soton) 1.0.1 not checked 05th March 2013 email

B Method Update Site

http://methode-b.com/update_site/atelierb_provers


Plug-in name Version Status MCV* Release Date Contact Additional info
AtelierB.png Atelier-B provers 2.1.0 available 3.x.x 18th March 2014 email Read the instructions concerning 64-bit compatibility : here

Other Update Sites

Plug-in name Version Status MCV* Release Date Contact Additional info
AnimB.png AnimB not checked Christophe Métayer Use the update site http://www.animb.org/updatesite
Camille 2.1.5 not checked 2.5.x 27th July 2011 Michael Jastram Use the Camille update site. http://www.stups.uni-duesseldorf.de/camille_updates
Make sure to install the Event-B EMF Framework version 3.7.0 or greater.
Mlogo big.png Modularisation not checked 2.x.x email Use the update site http://www.iliasov.org/modplugin
Generic Instantiation 1.1.0 available 3.0.x 1 August 2014 Thai Son Hoang Use the update site http://gen-inst.sourceforge.net/updates
Group refinement not checked 2.x.x email Use the update site http://iliasov.org/refplugin
Flows/Use case extension not checked 2.x.x email Use the update site http://iliasov.org/usecase
Prob eventb wiki logo.png ProB 3.0.1 available 3.0.x 18th March 2014 Jens Bendisposto Use the ProB update site. http://www.stups.uni-duesseldorf.de/prob_updates_rodin3
The Plug-in includes BMotion Studio
For older Rodin versions use http://www.stups.uni-duesseldorf.de/prob_updates
ProR logo.png ProR 0.3.2 not checked 2.6.x 08/01/2012 Michael Jastram Update site: http://update.formalmind.com/rodin
Project web site: http://eclipse.org/rmf
MBT for Event-B Logo Medium.png MBT plugin 2.0 not checked 2.7.x 5th of March 2012 Alin Stefanescu Use the update site http://fmi.upit.ro/mbt_plugin
Mode/FT Views 1.0.2 not checked 2.4.x 4th July 2011 Ilya Lopatkin Update site: http://rodinmodeftview.sourceforge.net/
Transformation patterns 1.0 not checked 2.x.x 4th July 2011 Ilya Lopatkin Update site: http://rodinmodeftview.sourceforge.net/
EHDL Ver2.png
VHDL code generator 2.0.2 not checked 2.x.x 12th March 2012 Sergey Ostroumov Update site: http://www.eventb-to-vhdl.tk/

*MCV stands for the Rodin's Maximum Compatible Version

Known plug-in incompatibilities

It unfortunately might exists some incompatibilities between plug-ins. This list might be non exhaustive and is updated accorded to user experiences. If you encounter some conflict while installing or using plug-ins, please send a mail to the Rodin User List or feel free to complete the following table.

Plug-in name Incompatible with