Difference between pages "D23 General Platform Maintenance" and "Rodin Platform 2.1 Release Notes"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
 
imported>Tommy
 
Line 1: Line 1:
−
= Overview =
+
{{TOCright}}
−
The purpose of the platform corrective and evolutive maintenance is to address bugs and feature requests reported either by mail or through the appropriate trackers on SourceForge.
 
  
−
The noticeable new features in the main platform for the past year are listed below:
+
== What's New in Rodin 2.1? ==
−
* Mathematical Language V2 (releases 1.0 and upper)
+
* General Interface
−
: The new version of the mathematical language is supported.
+
**Improved general platform performance.
−
: See [http://wiki.event-b.org/index.php/Event-B_Mathematical_Language Event-B Mathematical Language].
+
**Preferences for the automatic tactics changed.
−
* Theorems everywhere (releases 1.0 and upper)
+
:::It is now possible to define profiles (e.g. ordered lists) of tactics to be used in post or automatic tactics at both workspace and/or project level. A mechanism is also provided in order to export and share these profiles.
−
: It is possible to mix theorems and regular predicates in axioms, invariants and guards.
+
:::See [[Preferences_for_the_automatic_tactics | Preferences for the automatic tactics]]
−
* Auto-completion (releases 1.0 and upper)
 
−
: When entering a predicate or expression in the Event-B machine / context editor, it is possible to type <tt>C-Space</tt> to see a list of possible identifiers that could be entered at the cursor position.
 
−
* Entering mathematical symbols (releases 1.1 and upper)
 
−
: The Rodin platform provides many more ways to enter mathematical symbols:
 
−
: - either type the ASCII shortcut (as in previous releases),
 
−
: - or type the LaTeX command (as defined in style <tt>bsymb</tt>),
 
−
: - or click in the ''Symbol Table'' view which displays the symbols graphically,
 
−
: - or directly enter the Unicode value of the symbol (for advanced users).
 
−
: See [http://wiki.event-b.org/index.php/Rodin_Keyboard Rodin Keyboard].
 
  
−
See the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Release Notes] and the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation SourceForge] databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
+
* Modelling
  
−
= Motivations =
+
* Proving
−
The main evolutions of the Rodin platform are driven by the description of work for the DEPLOY project and the requirements expressed by industrial WP1 to WP4 partners or by advanced users during the lifecycle of the project.
+
:'''New automatic rewriting rules'''. Over 150 automatic rewriting rules have been added, making it easier to discharge proof obligations.
 +
:See: [[All_Rewrite_Rules]]
  
−
Beyond that, any user registered on SourceForge may record any encountered bug on the Rodin platform or request a new feature, using the dedicated [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation trackers]. Depending on the category, the bug / feature is assigned to the WP9 partner who is in charge of processing it:
+
== Requirements ==
−
{{SimpleHeader}}
+
{{TODO | COPY REQUIREMENTS FROM PREVIOUS PAGES / VERIFY}}<br>
−
|-
+
{{TODO | Inform here of some specific system requirements (version of Java, etc).}}
−
! scope=col | Category || Partner
 
−
|-
 
−
|AnimB || Christophe METAYER
 
−
|-
 
−
|B2LaTeX || University of Southampton
 
−
|-
 
−
|Decomposition || Systerel
 
−
|-
 
−
|Event-B core || Systerel
 
−
|-
 
−
|Event-B interface || Systerel
 
−
|-
 
−
|Event-B POG || Systerel
 
−
|-
 
−
|Event-B provers || Systerel
 
−
|-
 
−
|Event-B static checker || Systerel
 
−
|-
 
−
|PRO-B || Dusseldorf
 
−
|-
 
−
|Renaming || University of Southampton
 
−
|-
 
−
|Requirements || Dusseldorf
 
−
|-
 
−
|Rodin platform || Systerel
 
−
|-
 
−
|Text editor || Dusseldorf
 
−
|-
 
−
|U2B || Southampton
 
−
|}
 
  
−
The priorities are discussed during the WP9 meetings (bi-weekly management conference call, WP9 face-to-face meetings during DEPLOY workshops).
+
== External plug-ins ==
 +
{{:Rodin_Platform_2.1_External_Plug-ins}}
  
−
= Choices / Decisions =
+
== Downloading ==
−
The WP9 partners have agreed on a release policy (see the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Rodin Platform Releases] wiki page). In particular:
+
{{TODO | Add here a link to download the platform.}}
−
* A new version of the Rodin platform is released every 3 months.
 
−
* The code is frozen during the 2 weeks preceding each release.
 
−
* The Eclipse versioning policy is enforced (See [http://wiki.eclipse.org/index.php/Version_Numbering Version Numbering]).
 
−
* A wiki page is dedicated to each release.
 
  
−
The main advantages, for both developers and end-users, are summarized below:
+
== Fixed Bugs ==
−
* Information. The wiki page dedicated to each release provides instant information on the new features and improvements, which may be discussed if necessary.
+
{{TODO | Add here a list of the fixed bugs.}}
−
* Validation. The period of code freeze is more especially devoted to bug fixes, and the frequency of the stable releases is ensured.
 
−
* Integration. A synchronization between the optional plug-ins and other plug-ins is now possible.
 
  
−
= Available Documentation =
+
== Known Issues ==
−
The following pages give useful information about the Rodin platform releases:
+
{{TODO | COPY KNOWN ISSUES FROM PREVIOUS PAGES / VERIFY}}<br>
−
* Release notes.
+
{{TODO | Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.2).}}
−
: See [http://wiki.event-b.org/index.php/Rodin_Platform_Releases Rodin Platform Releases].
 
−
: More details are provided in the notes distributed with each release (eg. [http://sourceforge.net/project/shownotes.php?release_id=693928]).
 
−
* Bugs.
 
−
: See [http://sourceforge.net/tracker/?atid=651669&group_id=108850].
 
−
* Feature requests.
 
−
: See [http://sourceforge.net/tracker/?group_id=108850&atid=651672].
 
  
−
= Planning =
+
== About ==
−
The [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Rodin Platform Releases] wiki page lists in particular the upcoming releases and give the scheduled release dates.
+
Rodin Platform up to rxxxx <br>
 +
Developer Release date : dd/mm/yyyy.<br>
 +
User Release date : 28/01/2011.<br>
  
−
Special efforts will be made on the following topics, which are requested by all users in an industrial context:
+
[[Category:Rodin Platform Release Notes]]
−
* Mathematical Extensions.
 
−
: Currently, the operators and basic predicates of the Event-B mathematical language supported by the Rodin platform are fixed. The purpose is to extend the platform to support user-defined data types and associated operators, including inductive data types. Users will then be able to define operators of polymorphic type as well as parameterised predicate definitions.
 
−
 
 
−
* Team-based Development.
 
−
: The purpose is to perform simultaneous developments.
 
−
: The [http://wiki.event-b.org/index.php/D23_Decomposition Decomposition plug-in] gives an answer to this requirement by allowing to cut a model in sub-models which may be handled independently. In the same manner, the [http://wiki.event-b.org/index.php/EMF_Compare_Editor_installation EMF Compare Editor] enables the comparison of machines and contexts: it is a first step to be able to use the Rodin platform in a team environment by putting a code repository (e.g., Subversion) underneath it.
 
−
: In order to understand the problem properly, some usage scenarios for [http://wiki.event-b.org/index.php/Scenarios_for_Team-based_Development team-based development] and for [http://wiki.event-b.org/index.php/Scenarios_for_Merging_Proofs merging proofs] have already been written. Moreover, a page has been initiated to remember the main requirements (see [http://wiki.event-b.org/index.php/Teamwork_Requirements Teamwork Requirements]). These pages provide a basis for brainstorming and further developments on the topic.
 
−
 
 
−
* Documentation.
 
−
: The purpose is to continuously increase the available documentation on the Wiki. It may contains requirements, pre-studies (states of the art, proposals, discussions), technical details (specifications), teaching materials (tutorials), user's guides, etc. The intended audience may be the developers or the end-users.
 
−
 
 
−
[[Category:D23 Deliverable]]
 

Revision as of 14:03, 10 January 2011

What's New in Rodin 2.1?

  • General Interface
    • Improved general platform performance.
    • Preferences for the automatic tactics changed.
It is now possible to define profiles (e.g. ordered lists) of tactics to be used in post or automatic tactics at both workspace and/or project level. A mechanism is also provided in order to export and share these profiles.
See Preferences for the automatic tactics
  • Modelling
  • Proving
New automatic rewriting rules. Over 150 automatic rewriting rules have been added, making it easier to discharge proof obligations.
See: All_Rewrite_Rules

Requirements

TODO: COPY REQUIREMENTS FROM PREVIOUS PAGES / VERIFY
TODO: Inform here of some specific system requirements (version of Java, etc).

External plug-ins

Rodin Update Site

Plug-in name Version Status MCV* Release Date Contact Additional info
Umlb32.gif UML-B 2.2.0 available 9th Feb. 2011 email
UML-B Statemachine Animation 1.1.0 available 15th Feb. 2011 email Compatible with UML-B 2.2 and ProB 2.1.
Event-B EMF framework 3.2.1 available Users should not need to install this framework. It will be installed automatically by other plug-ins as required.
Export to Isabelle available 2.x.x email
Rose.gif Rose 1.1.0 available email
Records 1.0.1 available email This release includes EMF and Refactory support for records.
Teamwork not available
Shared Event Composition 1.3.1 available 9th Mar. 2011 email
Refactory 1.1.0 available 11th Feb. 2011 email
DecompositionPlug-in logo.png Decomposition 1.2.0 available 11th Feb. 2011 email
Project diagram icon s.png Project Diagram 1.0.0 available email
Relevance Filter 1.0.0 available 2.x.x email
Theory Plug-in v0.6 available 4th Jan. 2011 email
Code Generation Feature 0.1.5 available 17th May 2011 email

B Method Update Site

Plug-in name Version Status MCV* Release Date Contact Additional info
Atelier-B provers 1.2.2 available 17th Feb. 2011

Other Updates Sites

Plug-in name Version Status MCV* Release Date Contact Additional info
AnimB.png AnimB not available Christophe Métayer Use the update site http://www.animb.org/updatesite
Camille available Use the Camille update site. http://www.stups.uni-duesseldorf.de/camille_updates
Mlogo big.png Modularisation available 2.x.x email Use the update site http://www.iliasov.org/modplugin
Group refinement available 2.x.x email Use the update site http://iliasov.org/refplugin
Flows/Use case extension available 2.x.x email Use the update site http://iliasov.org/usecase
Prob eventb wiki logo.png ProB available 8th Feb. 2011 Use the ProB update site. http://www.stups.uni-duesseldorf.de/prob_updates
The Plug-in includes BMotion Studio
ProR logo.png ProR available 20th Jan. 2012 Michael Jastram ProR support working with requirements. For traceability to Event-B, the Rodin Integration is required.
Update site: http://update.pror.org
Project web site: http://eclipse.org/rmf
ProR logo.png Rodin Integration for ProR not available 28th Feb. 2012 Michael Jastram We are currently working on a revised ProR-Rodin-Integration.

*MCV stands for the Rodin's Maximum Compatible Version

Known plug-in incompatibilities

It unfortunately 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

Downloading

TODO: Add here a link to download the platform.

Fixed Bugs

TODO: Add here a list of the fixed bugs.

Known Issues

TODO: COPY KNOWN ISSUES FROM PREVIOUS PAGES / VERIFY
TODO: Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.2).

About

Rodin Platform up to rxxxx
Developer Release date : dd/mm/yyyy.
User Release date : 28/01/2011.

Retrieved from ‘https://wiki.event-b.org/index.php?title=D23_General_Platform_Maintenance&oldid=7609’