AnimB start
From Event-B
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.
The animation editor
The following screenshot describes the animation editor:
Event guard state
The state of an event guard is described by the foolowing icons:
the guard of the event is closed and can't be executed.
the guard of the event is open and the event can be executed.
the guard can't be checked (constant value needed, well defined error, ...).
