B Tools - B2RODIN

Presentation

B2RODIN makes it possible to import into the Rodin platform textual B models, developed with Atelier B of B4Free. A complete refinement column can be imported in a single step. B2RODIN undertakes generating the associated models and contexts.

How to Install B2RODIN ?

The installation of B2RODIN uses Eclipse’s "UpdateSite" function. In order to do that, it is necessary to:

In the Help / Software Updates menu, activate the "Find and Install" function;
Select "Search for a new feature to install;"
Click on the "New Remote Site" button;
In the dialogue box the appears, enter:

"b2rodin" in the "Name" field;
http://www.bmethod.com/update_site/b2rodin in the "URL" field

Click on the "Finish" button in order to install the b2rodin plugin.

The online help makes it possible to understand how to implement this tool.

How to Use B2RODIN ?

The B models to be imported must be compatible with the event-driven B, i.e. that the operations must be of the form:

It is necessary, in addition, to add to the textual B models information relative to the semantics of the event-driven B (see the online help of the tool regarding this for more details), by notably indicating how the events are refined: introduction of new events, combination of events, break-up of event.

Finally, it is possible to value the constants of the textual model so as to animate it with Brama.

In order to import a refinement column in a single time, it is necessary to indicate the last refinement of the column that one wants to import / B2RODIN thus undertakes importing in an iterative manner the abstractions from this refinement.

Version History

Version 1.0.7
Addition of a mode making it possible to not over-bracket the generated components. This mode is not activated by default, because it has not been tested very much.
In the case where no pragma include is given in the machine B, B2RODIN from now on translates all the events. The previous behaviour was to translate nothing.
Correction of a bug during the translation of bracketed expressions.
Correction of an installation problem under macros X: the b2rodin file was not rendered executable during the installation.