B Tools - Brama

Presentation

Brama is a tool used to animate B models on the Rodin platform. Brama’s objective is two-fold:

To allow the formal model’s designer to ensure that his model is executed in accordance with the system it is supposed to represent.
To provide this model with a graphic representation and animate this representation in accordance with the state of the formal model. The graphic representation must be in Flash format and requires the use of a separate tool for its elaboration (Flash MX, for example).

How to Install Brama ?

Instructions...

How to Use Brama ?

Brama can be used in two distinct ways:

Animation of a B model in an Eclipse environment:

Display of events that can be initiated,
Display of the model’s variables and their value,
Initiation of an event that changes the value of a variable.

Animation of a B model with a flash animation:

Association of graphic flash animations with a change in status or the initiation of a B event,
Change in the value of a variable or initiation of an event further to a user action at the flash animation level.

Animation of a B model in an Eclipse environment

The animation of a B model requires:

A statically verified model (no error messagecan appear in the “Problems” view), composed of a machine and potentially one or more refinements.
The valuation of the constants declared in the contexts.

The valuation of the constants requires the attribution of values to every constant, including the items in the sets listed. There are two ways to perform this valuation:

By using B2RODIN when importing the textual B models:

By entering the value of the constants in the context editor within the Rodin platform:

Animation of a B model with a flash animation :

Once the B model is satisfactory (it has been fully proven and its animation has demonstrated that the model behaves like its related system), you can create a graphic representation of this system and animate it synchronously with the underlying B Rodin model.

Brama does not create this animation. It is up to the modeler to create the representation of the model depending on the part of the model he wants to display. However, Brama provides the elements required to connect your flash animation and model B.

For more details, see the online help tool.

History of the Versions

0.0.15:

Correction of a bug preventing the operations of schedulers under MacOS
Addition of a button to sort variables in the animator.
Addition of an “animate” button for *.mch and *.ref files. This command converts B files into rodin files and launches the animator on the converted file.

0.0.14:

Significant improvement in performance