Difference between pages "UML-B Integration and Improvements" and "Rodin Platform 3.5 Release Notes"

Revision as of 09:55, 8 September 2020

1 What's New in Rodin 3.5?
- 1.1 Changes for plug-in developers
2 Installing
- 2.1 Downloading
- 2.2 Upgrading from a previous version of Rodin 3.x
3 Requirements - Compatibility
4 External plug-ins
5 Fixed Bugs and Implemented Features
6 Known Issues
- 6.1 Rodin is not notarized
- 6.2 macOS in dark mode
7 Disclaimer
8 About

What's New in Rodin 3.5?

Rodin 3.5 brings several bug fixes, and upgrades the underlying Eclipse to 2020-06.

Please note that we no longer provide 32-bit binary versions of the Rodin platform, since they are almost not downloaded anymore (as per the statistics on SourceForge), everyone is now running a 64-bit OS. Nonetheless, if needed, it is still possible for you to build 32-bit binaries from the source (see Building Rodin Headless, you may also ask for support).

Changes for plug-in developers

Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.

There is no API change within Rodin Core.

TODO Several variants in the same machine

Installing

Downloading

Download Rodin 3.5 now !

Upgrading from a previous version of Rodin 3.x

TODO CHECK IS THIS IS TRUE

The only way to upgrade is to download the new platform. You may then point it to your usual workspace(s). This restriction is due to the Eclipse switch.

For those who are annoyed to install their Rodin plug-ins once more by downloading from the update site, it might be worth installing them directly from your older Rodin installation:

run the new Rodin
File > Import... > Install/From Existing Installation
Point to your older Rodin installation
Select the features you want to install
Proceed with the Next button, the following is just as a usual install

Requirements - Compatibility

Configurations supported (and for which binaries are provided)
- Linux 64-bit
- Windows 64-bit
- Mac OS X 64-bit

You need to have a 64-bit Java JRE (8 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32-bit JRE.

To enhance your proving experience, the eclipse font settings (size, aspect...) are available from the preferences (General > Appearance > Colors and Fonts > Rodin). These settings allow you to modify the properties set on the Event-B Keyboard Text Font which is used in many views of the Proving UI. However, to enjoy these functionalities, you need to install the Brave Sans Mono font on your system. You can download this font from the link here.

Linux 64-bit:

package 'libc6-amd64:i386' must be installed, in particular in order to run external prover binaries

depending on the distribution, you could instead need these packages: lib32z1 lib32ncurses5 lib32bz2-1.0

Windows 64-bit:

Atelier B provers work more slowly; it can cause ML to not automatically discharge some sequents that it discharges on windows 32-bit, due to its timeout. A workaround is to download a custom profile: DefaultAuto_ML800, then Window > Preferences > Event-B > Sequent Prover > Auto/Post Tactic > Profiles (tab) > Import..., point to the downloaded file, 'Select All' profiles (there are 2), OK. Then in 'Auto/Post Tactic' tab, select 'Default Auto Tactic Profile (ML 800)' profile for auto-tactics. It is the same as the 'Default Auto Tactic Profile', except ML has a longer timeout (800 ms). You can of course change this timeout by editing the 'ML (800)' profile.

We have not noticed this problem for Linux 64-bit, nor for other platforms; however if you do, the same workaround applies.

External plug-ins

Rodin Update Site

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

	Plug-in name	Version	Status	MCV*	Release Date	Contact	Additional info
	SMT Solvers	1.5.0	available		14th January 2022	Laurent Voisin	Automatic prover using SMT solvers
	Relevance Filter	1.1.1	available	?.x.x			Improves chance of automatic proof by selecting relevant hypotheses
	B2Latex export	0.7.0	available	2.5.x	27th May 2015	Laurent Voisin	generates a Latex documentation of the Event-B
	Rose editor	1.7.0	available	3.x.x	4 Nov 2018	umlb	Tree-structured editor for Event-B EMF that handles extensions without modification. Mainly useful for Plug-in developers.
CODA	CODA Component Diagrams	6.0.1	available	3.x.x	?	umlb	Component diagrams with timed channels. (Not compatible with latest UML-B. Will be up-issued on Soton update site.)
CODA	CODA Simulator for Component Diagrams	3.0.1	available	3.x.x	?	umlb	Component based simulation. (Not compatible with latest UML-B. Will be up-issued on Soton update site.)
	Project Diagram	1.0.1	available	3.x.x	1st Feb. 2015	umlb	Machine - Context relationship diagram. (Not compatible with latest UML-B. Will be up-issued on Soton update site.)
	UML-B	2.3.0	available	3.x.x	18th Oct. 2014	umlb	Original UML-B modelling environment
	Shared Event Composition	1.7.1	not checked		5th July 2017	umlb	Compatible with Rodin 3.x.x
	Decomposition	1.3.1	not checked		4th July 2017	umlb	Compatible with Rodin 3.x.x
	Refactory	1.3.0	not checked	3.x.x	6th May 2014	umlb	Compatible with Rodin 3.0.x.
	Theory Plug-in	4.0.4	available		1st April 2022	Guillaume Verdier
	Code Generation	0.2.5	not checked		29th Aug. 2013	umlb	For Java, Ada, and OpenMP C code
	Isabelle for Rodin		not checked	2.x.x
	Pattern	0.9.0	not checked	3.x.x	13th March 2015	Thai Son Hoang
	Qualitative Probability	0.2.3	not working	3.x.x	9th October 2015	Thai Son Hoang	Needs updating to be compatible with changes in Rodin 3.5
	Generic Instantiation (Soton)	1.0.1	not checked		05th March 2013	Asieh
	Records	2.0.0	not checked	2.x.x	16th Oct. 2010	umlb	no longer supported - use CamilleX instead
	Teamwork	1.2.0	not checked	3.2.x	5th Sept. 2016	umlb	No longer supported - use CamilleX instead. Provides a synchronised copy of Machines and Contexts for committing into a repository.
	UML-B Statemachine Animation	1.3.0	not checked	3.x.x	18th Oct. 2014	umlb	no longer supported - use new UML-B from Soton update site instead
	iUML-B plugins		not checked	3.x.x		umlb	New versions are now available on the Soton Update Site.

Atelier B Update Site

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

	Plug-in name	Version	Status	MCV*	Release Date	Contact	Additional info
	Atelier B provers	2.3.0	available	3.3.0	2 Dec 2020

ProB Update Site

Available from http://www.stups.hhu.de/prob_updates_rodin3

Plug-in name	Version	Status	MCV*	Release Date	Additional info
ProB	3.0.10	available	3.5.0	4 Sep 2020	The ProB animator and model checker
ProB (Dis)Prover	3.0.9	available	3.5.0	4 Sep 2020	The ProB counter-example finder and prover
ProB Symbolic constants support	3.0.9	available	3.5.0	4 Sep 2020

Southampton Releases Update Site

Available from http://eventb-soton.github.io/updateSite/releases

Plug-in name	Version	Status	MCV*	Release Date	Contact	Additional info
CamilleX	2.0.2	new release	3.4.x	21 Jan 2021	Thai Son Hoang	CamilleX provides text editors for Event-B models and support modelling mechanisms such as machine inclusion.
UML-B Class Diagrams	3.0.0	new release	3.x.x	11 Sept 2020	umlb	UML-B Class diagrams translate into Event-B Machines.
UML-B State-machines	4.0.1	new release	3.x.x	13 Aug 2020	umlb	UML-B State-machines translate into Event-B Machines.
UML-B State-machine Animation	3.0.0	new release	3.x.x	13 Aug 2020	umlb	Animate UML-B State-machines. Compatible with UML-B statemachines 4.x.x and ProB 3.0.x.
Scenario Checker	0.0.0	new release	3.4.x	31 July 2020	umlb	Validation tool for recording and replaying scenarios

The following framework plug-ins are also provided on the Southampton Releases Update Site. These plugins are installed automatically when required and are not usually installed explicitly by users.

Plug-in name	Version	Status	MCV*	Release Date	Contact	Additional info
Event-B EMF framework	6.1.0	new release	3.x.x	4 July 2020	umlb	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 extensions	6.1.0	new release	3.x.x	4 July 2020	umlb	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.
UML-B diagrams	8.0.1	new release	3.2.x	13 Aug 2020	umlb	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.
ProB Support	0.0.0	new release	3.4.x	28 July 2020	umlb	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.

Fixed Bugs and Implemented Features

Bugs

TODO
777 Missing refresh in Rodin Editor for event convergence status

Feature Requests

TODO
None

Known Issues

See known bugs on SourceForge.

Rodin is not notarized

TODO

macOS in dark mode

TODO

Disclaimer

Since Rodin is continuously maintained, several unsoundness bugs which have been encountered were investigated and fixed. However, despite the total commitment of our teams to ensure the soundness of the platform, some unexpected and unknown soundness issues could remain. We would be grateful if you would report these issues to the development mailing list.

About

TODO Rodin Platform with git commit: 6980ca1
User Release date : 2018/03/07.

@@ Line 1: / Line 1: @@
-=== UML-B Integration with Event-B===
+{{TOCright}}
-[[UML-B]] provides a 'UML-like' graphical front end for Event-B. It adds support for class-oriented and state machine modelling but also provides visualisation of existing Event-B modelling concepts. UML-B is similar to UML but is a new notation with its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B tools so that when a drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element.  However, many features of UML-B are a replication of corresponding Event-B features. For example, the project diagram in UML-B, uses the concepts of machines and contexts and their relationships (refines, sees and extends). The project diagram would be just as applicable to an Event-B project that did not use any UML like modelling concepts. Similarly, while modelling in UML-B class diagrams, model elements are introduced to a machine that are directly equivalent to their Event-B counterparts. Greater integration would allow UML-B diagrams to be interspersed with Event-B model elements in a flexible mixed modelling interface. This has not been possible due to the differing underlying technologies used for Event-B (bespoke data repository) and UML-B (EMF).
+== What's New in Rodin 3.5? ==
-The integration between UML-B and Event-B will be improved by introducing an [[EMF_framework_for_Event-B|EMF framework for Event-B]]. This will allow UML-B to be re-implemented as an extension to Event-B. Work has begun on this framework and resulting integrated tools will become available during 2009.
+Rodin 3.5 brings several bug fixes, and upgrades the underlying Eclipse to 2020-06.
-===Improvements to the existing version of UML-B===
+Please note that we no longer provide 32-bit binary versions of the Rodin platform, since they are almost not downloaded anymore (as per the statistics on SourceForge), everyone is now running a 64-bit OS. Nonetheless, if needed, it is still possible for you to build 32-bit binaries from the source (see [[Building Rodin Headless]], you may also ask for [https://sourceforge.net/projects/rodin-b-sharp/support support]).
-While this new UML-B is being developed, improvements to the existing version of UML-B are ongoing. A new release of UML-B (0.5.0)) contains significant improvements, most notably the addition of support for refinement of statemachines. New features include:
-* Support for refinement of state machines in UML-B. This release 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. This addition is described in more detail in [[SaidButlerSnook09.pdf|Said, Butler and Snook]]
+=== Changes for plug-in developers ===
-* 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.
+Rodin 3.5 is built on top of Eclipse 4.16 (2020-06), which requires Java 8, just as the previous versions.
-* 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 was formerly 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.
+There is no API change within Rodin Core.
-* The properties view has been improved with the addition of a tab for 'model'. This tab allows direct access to the underlying EMF model element so that its properties can be viewed and changed.
+TODO Several variants in the same machine
-* Some improvements have been made to the UML-B perspective layout to reflect changes to the Event-B one. The task and problem views have been removed and the 'Rodin Problem' view has been added instead.
+== Installing ==
+=== Downloading ===
+[http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.5/ Download Rodin 3.5 now !]
+=== Upgrading from a previous version of Rodin 3.x ===
+TODO CHECK IS THIS IS TRUE
+The only way to upgrade is to download the new platform.
+You may then point it to your usual workspace(s).
+This restriction is due to the Eclipse switch.
+For those who are annoyed to install their Rodin plug-ins once more by downloading from the update site, it might be worth installing them directly from your older Rodin installation:
+* run the new Rodin
+* File > Import... > Install/From Existing Installation
+* Point to your older Rodin installation
+* Select the features you want to install
+* Proceed with the Next button, the following is just as a usual install
+== Requirements - Compatibility ==
+* Configurations supported (and for which binaries are provided)
+** Linux 64-bit
+** Windows 64-bit
+** Mac OS X 64-bit
+* You need to have a 64-bit Java JRE (8 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32-bit JRE.
+* To enhance your proving experience, the eclipse font settings (size, aspect...) are available from the preferences (General > Appearance > Colors and Fonts > Rodin). These settings allow you to modify the properties set on the Event-B Keyboard Text Font which is used in many views of the Proving UI. However, to enjoy these functionalities, you need to install the Brave Sans Mono font on your system. You can download this font from the link [http://sourceforge.net/projects/rodin-b-sharp/files/Font_%20Brave%20Sans%20Mono/0.12/ here].
+* Linux 64-bit:
+: package 'libc6-amd64:i386' must be installed, in particular in order to run external prover binaries
+: depending on the distribution, you could instead need these packages: lib32z1 lib32ncurses5 lib32bz2-1.0
+* Windows 64-bit:
+: Atelier B provers work more slowly; it can cause ML to not automatically discharge some sequents that it discharges on windows 32-bit, due to its timeout. A workaround is to download a custom profile: [http://sourceforge.net/projects/rodin-b-sharp/files/DefaultAuto_ML800 DefaultAuto_ML800], then Window > Preferences > Event-B > Sequent Prover > Auto/Post Tactic > Profiles (tab) > Import..., point to the downloaded file, 'Select All' profiles (there are 2), OK. Then in 'Auto/Post Tactic' tab, select 'Default Auto Tactic Profile (ML 800)' profile for auto-tactics. It is the same as the 'Default Auto Tactic Profile', except ML has a longer timeout (800 ms). You can of course change this timeout by editing the 'ML (800)' profile.
+: We have not noticed this problem for Linux 64-bit, nor for other platforms; however if you do, the same workaround applies.
+== External plug-ins ==
+{{:Rodin_Platform_3.5.0_External_Plug-ins}}
+== Fixed Bugs and Implemented Features ==
+Bugs
+ TODO
+Missing refresh in Rodin Editor for event convergence status
+Feature Requests
+ TODO
+ None
+== Known Issues ==
+See [http://sourceforge.net/p/rodin-b-sharp/bugs known bugs on SourceForge].
+=== Rodin is not notarized ===
+TODO
+=== macOS in dark mode ===
+TODO
+== Disclaimer ==
+Since Rodin is continuously maintained, several unsoundness bugs which have been encountered were investigated and fixed. However, despite the total commitment of our teams to ensure the soundness of the platform, some unexpected and unknown soundness issues could remain. We would be grateful if you would report these issues to the [mailto:rodin-b-sharp-devel@lists.sourceforge.net development mailing list].
+== About ==
+TODO
+Rodin Platform with git commit: 6980ca1<br/>
+User Release date : 2018/03/07.
+[[Category:Rodin Platform Release Notes]]