AnimB start: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Christophe |
imported>Christophe |
||
| 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 | The state of an event guard is described by the following icons: | ||
* [[Image:guardclosed.png|guardclosed.png]] the guard of the event is closed and can't be executed. | * [[Image:guardclosed.png|guardclosed.png]] the guard of the event is closed and can't be executed. | ||
* [[Image:guardopen.png|guardopen.png]] the guard of the event is open and the event can be executed. | * [[Image:guardopen.png|guardopen.png]] the guard of the event is open and the event can be executed. | ||
* [[Image:unexecutable.png|unexecutable.png]] the guard can't be checked (constant value needed, well defined error, ...). | * [[Image:unexecutable.png|unexecutable.png]] the guard can't be checked (constant value needed, well defined error, ...). | ||
=== Component tabs === | === Component tabs === | ||
Each animated machines and here contexts are described in a specific tab. | Each animated machines and here contexts are described in a specific tab. | ||
Revision as of 20:19, 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 following 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, ...).
Component tabs
Each animated machines and here contexts are described in a specific tab.
The following screenshot describes a context tab.
Variables table
The variable table or constant table describes the state of a machine or context.
The last change 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 choose randomly an open event and execute it.
