AnimB start: Difference between revisions
imported>Christophe |
imported>Mathieu m display bug ? |
||
(33 intermediate revisions by 2 users not shown) | |||
Line 1: | Line 1: | ||
==Setting the constant values== | |||
The user must give a value for each constants. A constant value is set in the context editor. To add a new constant value add to button [[Image:plus.png]]. | |||
Each line is composed of two fields: | |||
* the first one give the constant or set name | |||
* the second one give a B expression | |||
===Setting set value=== | |||
Three possible is available. | |||
* the first one is implicitly given by the axioms. This is the case for enumerated set. | |||
* the second one is given by a enumerated set with identifier which are not used for the constant names. | |||
:For example '''{a, b, de, g}''' declares 4 new identifiers ('''a''', '''b''', '''de''', '''g''') that could be used to set constant value | |||
* the third is a sugar form of the previous one. <br>For example '''{a1,..,a25}''' declares 25 new identifiers ('''a1''', '''a2''', ...,'''a25''') | |||
===Setting constant value=== | |||
A constant value is given by a B expression. A value declared in a set value could be used. | |||
==Start an animation== | ==Start an animation== | ||
To start an animation, select a machine in "Project explorer" or in "Obligation Explorer" then click right and select "Animate" action. | To start an animation, select a machine in "Project explorer" or in "Obligation Explorer" then click right and select "Animate" action. | ||
Then "new animation wizard" is open. | |||
[[Image:rightclick.png|305px|center]] | |||
==New animation wizard== | ==New animation wizard== | ||
The " | ===Generality=== | ||
The "Run AnimB" wizard allows to start an animation of a event-b model. | |||
* set | The wizard is composed of two field: | ||
*"Animation name" field allows to set the name of the animation. The animation name identifies an animation and could be used to shared animation between application clients. You can use the default value. | |||
The animation name | *The combo list "Last model" fixes the more abstract model use to build the animation. | ||
[[Image:wizard.png|438:px|center]] | *The field "Max int value" and "Min int value" fix the value used to choose an integer. | ||
'''Note''': If you choose a name already used for an open animation, then you will obtain a second editor but the two editors will display the same animation. | |||
===Example=== | |||
Suppose a refinement column composed of 5 models: | |||
* brp_0 | |||
* brp_1 | |||
* brp_2 | |||
* brp_3 | |||
and you run the wizard under the "brp_2" model. | |||
The following picture display the settings to run a animation called "brp_name". The animation will execute the two following model. | |||
* brp_1, the more concrete model | |||
* brp_2, the more abstract used for the animation | |||
You can use this feature to animate one model. | |||
[[Image:wizard.png|438:px|center]] | |||
== The animation editor== | == The animation editor== | ||
The following screenshot describes the animation editor: | The animation editor contains : | ||
[[Image: | * a page for each model | ||
* a page for each context seen by a model | |||
The following screenshot describes the animation editor for an animation of the models brp_3 and brp_2 which refer the contexts brp_ctx3, brp_ctx_2 and brp_ctx_1 : | |||
[[Image:Editor1.png|978:px|center]] | |||
=== Model page === | |||
The model page is split in two parts: | |||
*the first part contains the list of the event of the corresponding model | |||
*the second part describes in a table the list of the variables and the list of the seen constants and there values. | |||
=== Event guard state === | === Event guard state === | ||
The state of an event guard is described by the following icons: | The state of an event guard is described by the following icons: | ||
Line 21: | Line 70: | ||
=== Component tabs === | === Component tabs === | ||
Each animated machines and | Each animated machines and its contexts are described in a specific tab. | ||
The following screenshot describes a context tab. | The following screenshot describes a context tab. | ||
[[Image:constantTab.png|639|center]] | [[Image:constantTab.png|639|center]] | ||
=== Variables table === | |||
The variable table or constant table describes the state of a machine or context. | |||
The variables change by the last event execution are typeset in red. | |||
The | |||
[[Image:lastChange.png|640px|center]] | [[Image:lastChange.png|640px|center]] | ||
Line 39: | Line 89: | ||
* [[Image:GuardOpenEx.png]] when the event is open | * [[Image:GuardOpenEx.png]] when the event is open | ||
[[Category:User documentation]] | |||
[[Category:AnimB]] | |||
[[ |
Latest revision as of 14:59, 16 September 2009
Setting the constant values
The user must give a value for each constants. A constant value is set in the context editor. To add a new constant value add to button . Each line is composed of two fields:
- the first one give the constant or set name
- the second one give a B expression
Setting set value
Three possible is available.
- the first one is implicitly given by the axioms. This is the case for enumerated set.
- the second one is given by a enumerated set with identifier which are not used for the constant names.
- For example {a, b, de, g} declares 4 new identifiers (a, b, de, g) that could be used to set constant value
- the third is a sugar form of the previous one.
For example {a1,..,a25} declares 25 new identifiers (a1, a2, ...,a25)
Setting constant value
A constant value is given by a B expression. A value declared in a set value could be used.
Start an animation
To start an animation, select a machine in "Project explorer" or in "Obligation Explorer" then click right and select "Animate" action. Then "new animation wizard" is open.
New animation wizard
Generality
The "Run AnimB" wizard allows to start an animation of a event-b model. The wizard is composed of two field:
- "Animation name" field allows to set the name of the animation. The animation name identifies an animation and could be used to shared animation between application clients. You can use the default value.
- The combo list "Last model" fixes the more abstract model use to build the animation.
- The field "Max int value" and "Min int value" fix the value used to choose an integer.
Note: If you choose a name already used for an open animation, then you will obtain a second editor but the two editors will display the same animation.
Example
Suppose a refinement column composed of 5 models:
- brp_0
- brp_1
- brp_2
- brp_3
and you run the wizard under the "brp_2" model. The following picture display the settings to run a animation called "brp_name". The animation will execute the two following model.
- brp_1, the more concrete model
- brp_2, the more abstract used for the animation
You can use this feature to animate one model.
The animation editor
The animation editor contains :
- a page for each model
- a page for each context seen by a model
The following screenshot describes the animation editor for an animation of the models brp_3 and brp_2 which refer the contexts brp_ctx3, brp_ctx_2 and brp_ctx_1 :
Model page
The model page is split in two parts:
- the first part contains the list of the event of the corresponding model
- the second part describes in a table the list of the variables and the list of the seen constants and there values.
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 its 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 variables change by the last event execution are typeset in red.
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: