Difference between revisions of "AnimB start"

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 foolowing icons:
+
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.

Rightclick.png


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


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


Variables table

The variable table or constant table describes the state of a machine or context.
The last change are red underline.

LastChange.png

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.