AnimB start: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Christophe
imported>Christophe
Line 23: Line 23:
The following screenshot describes the animation editor for an animation of the models brp_3 and brp_2 which refer the contexts brp_ctx3, brp_ctx_2 and brp_ctx_1 :<br>
The following screenshot describes the animation editor for an animation of the models brp_3 and brp_2 which refer the contexts brp_ctx3, brp_ctx_2 and brp_ctx_1 :<br>
[[Image:editor.png|638:px|center]]
[[Image:editor.png|638:px|center]]
=== Model page ===
The model page is split in two parts:
*the first part contains the list of the event of the corresponding model
*the second part describes in a table the list of the variables and the list of the seen constants and there values.
=== Event guard state ===
=== Event guard state ===
The state of an event guard is described by the following icons:
The state of an event guard is described by the following icons:

Revision as of 20:19, 10 March 2009

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.
The field "Animation name" is required and give a name to the created animation.

  • The combo list "Last model" fixes the more abstract model use to build the animation.
  • The animation name is used to shared animation between application client. You can use the default value.

In the following example, an animation called anim_name will be created.

  • brp_3 is the more concrete model
  • brp_2 is the more abstract model

You can use the feature to animate one model.

438:px
438:px


click on Next to choose the constants valuation or on Finish to run the animation.

The animation editor

The animation editor contains :

  • a page for each model
  • a page for each context seen by a model


The following screenshot describes the animation editor for an animation of the models brp_3 and brp_2 which refer the contexts brp_ctx3, brp_ctx_2 and brp_ctx_1 :

638:px
638:px

Model page

The model page is split in two parts:

  • the first part contains the list of the event of the corresponding model
  • the second part describes in a table the list of the variables and the list of the seen constants and there values.

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 its 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 variable changes by the lest event execution are typeset in red.

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 by either:

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

After editing the values, you to need to click on the "Apply" button for them to be taken into account.

String integer value

A string is considered as an integer. So, in order to ease the understanding of the animation behaviour, you can use meaningful strings instead of integers for carrier-sets or constants belonging to a carrier-set.

The following screenshot describes a constant value set in the "Synthesis" view with string value: