AnimB start

From Event-B
Revision as of 21:10, 8 July 2008 by imported>Christophe (→‎String integer value)
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Start an animation

To start an animation, select a machine in "Project explorer" or in "Obligation Explorer" then click right and select "Animate" action.


New animation wizard

The "new animation wizard" is open.
This wizard allows to :

  • set an animation name,
  • choose constant valuation.

The animation name is used to shared animation between application client. You can use the default value.

438:px
438:px


The animation editor

The following screenshot describes the animation editor: ceneter

Event guard state

The state of an event guard is described by the following icons:

  • guardclosed.png the guard of the event is closed and can't be executed.
  • guardopen.png the guard of the event is open and the event can be executed.
  • unexecutable.png the guard can't be checked (constant value needed, well defined error, ...).

Component tabs

Each animated machines and here contexts are described in a specific tab. The following screenshot describes a context tab.

639
639


Variables table

The variable table or constant table describes the state of a machine or context.
The last changes are red underline.

Execute an event

To execute an event:

  • click on the corresponding event in the event table or
  • click on the "random execution" button : in this case the animator chooses randomly an open event and executes it.

The last executed event is described by a gold arrow:

  • when the event is closed
  • when the event is open

Manage constante values

The animator need constant value to animate a model. Be aware that no check is done by the animator so you can set any value.

Record constant value set

In the "Synthesis" tab of a context you can record a constant value set. The following button creates a constant value set.

Apply the constant value set

Once an animation start, you must set constant values:

  • selecting a recorded values set with the corresponding combo
  • editing manually the constant values in the tab

To set new value to the constant click on the "Apply" button.

String integer value

A string is considered as an integer. You can use string integer for carrier-set or constant belonging a carrier-set. The following screenshot describes a constant value set in the "Synthesis" vue with string value: