AnimB start: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Christophe No edit summary |
imported>Christophe No edit summary |
||
| Line 15: | Line 15: | ||
[[Image:editor.png|638:px|ceneter]] | [[Image:editor.png|638:px|ceneter]] | ||
=== Event guard state === | === Event guard state === | ||
The state of an event guard is described by the foolowing icons: | |||
* [[guardclosed.png|guardclosed.png]] the guard of the event is closed and can't be executed. | |||
* [[guardopen.png|guardopen.png]] the guard of the event is open and the event can be executed. | |||
* [[unexecutable.png|unexecutable.png]] the guard can't be checked (constant value needed, well defined error, ...). | |||
=== Component tabs === | === Component tabs === | ||
=== Variables table === | === Variables table === | ||
Revision as of 20:01, 7 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.
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:
- 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, ...).
