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