AnimB start: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Christophe
imported>Christophe
No edit summary
Line 38: Line 38:
* [[Image:GuardClosedEx.png]] when the event is closed
* [[Image:GuardClosedEx.png]] when the event is closed
* [[Image:GuardOpenEx.png]] when the event is open
* [[Image:GuardOpenEx.png]] 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 [[Image:applied.png]] 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.

Revision as of 21:04, 8 July 2008

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.