Home l Brama Tool l Download l Our Demonstrations l Documentation l Links l Contact  

Download Brama

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