AnimB start - Revision history

imported>Mathieu: display bug ?

2009-09-16T14:59:21Z

display bug ?

← Older revision		Revision as of 14:59, 16 September 2009
Line 8:		Line 8:
	* the first one is implicitly given by the axioms. This is the case for enumerated set.		* 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.~~<br>~~For example '''{a, b, de, g}''' declares 4 new identifiers ('''a''', '''b''', '''de''', '''g''') that could be used to set constant value~~<br>~~		* 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''')		* the third is a sugar form of the previous one. <br>For example '''{a1,..,a25}''' declares 25 new identifiers ('''a1''', '''a2''', ...,'''a25''')

Line 17:		Line 18:
	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.		Then "new animation wizard" is open.
	[[Image:rightclick.png\|305px\|center]]~~<br>~~		[[Image:rightclick.png\|305px\|center]]


	==New animation wizard==		==New animation wizard==
Line 26:		Line 28:
	*The combo list "Last model" fixes the more abstract model use to build the animation.		*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.		*The field "Max int value" and "Min int value" fix the value used to choose an integer.
	~~<br>~~

	'''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.		'''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.

Line 44:		Line 47:

	You can use this feature to animate one model.		You can use this feature to animate one model.
	[[Image:wizard.png\|438:px\|center]]~~<br>~~		[[Image:wizard.png\|438:px\|center]]


	== The animation editor==		== The animation editor==
Line 50:		Line 54:
	* a page for each model		* a page for each model
	* a page for each context seen by a model		* a page for each context seen by a model
	~~<br>~~
	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 :~~<br>~~
			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]]		[[Image:Editor1.png\|978:px\|center]]
	=== Model page ===		=== Model page ===
Line 65:		Line 71:
	=== Component tabs ===		=== Component tabs ===
	Each animated machines and its contexts are described in a specific tab.		Each animated machines and its contexts are described in a specific tab.
	The following screenshot describes a context tab.~~<br>~~		The following screenshot describes a context tab.

	[[Image:constantTab.png\|639\|center]]		[[Image:constantTab.png\|639\|center]]

imported>Christophe at 20:29, 6 July 2009

2009-07-06T20:29:09Z

@@ Line 81: / Line 81: @@
 * [[Image:GuardClosedEx.png]] when the event is closed
 * [[Image:GuardOpenEx.png]] when the event is open
 [[Category:User documentation]]
 [[Category:AnimB]]

imported>Christophe: /* Setting the constant values */

2009-07-06T20:28:26Z

Setting the constant values

← Older revision		Revision as of 20:28, 6 July 2009
Line 5:		Line 5:
	* the second one give a B expression		* the second one give a B expression
	===Setting set value===		===Setting set value===
	Three possible is ~~avalaible~~.		Three possible is available.
	* the first one is implicitly given by the axioms. This is the case for enumerated set.		* the first one is implicitly given by the axioms. This is the case for enumerated set.

Line 13:		Line 13:
	===Setting constant value===		===Setting constant value===
	A constant value is given by a B expression. A value declared in a set value could be used.		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.

imported>Christophe: /* Setting set value */

2009-07-06T20:22:42Z

Setting set value

← Older revision		Revision as of 20:22, 6 July 2009
Line 9:		Line 9:

	* the second one is given by a enumerated set with identifier which are not used for the constant names.<br>For example '''{a, b, de, g}''' declares 4 new identifiers ('''a''', '''b''', '''de''', '''g''') that could be used to set constant value<br>		* the second one is given by a enumerated set with identifier which are not used for the constant names.<br>For example '''{a, b, de, g}''' declares 4 new identifiers ('''a''', '''b''', '''de''', '''g''') that could be used to set constant value<br>
	* the third is a sugar form of the previous one. <br>For example '''{a1,..,a25}''' declares 25 new identifiers ('''a1''', '''a2''', ...,'''a25'''}		* 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===		===Setting constant value===

imported>Christophe: /* Setting set value */

2009-07-06T20:21:51Z

Setting set value

← Older revision		Revision as of 20:21, 6 July 2009
Line 8:		Line 8:
	* the first one is implicitly given by the axioms. This is the case for enumerated set.		* 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.<br>~~Example: the following~~ declares 4 new identifiers ('''a''', '''b''', '''de''', '''g''') that could be used to set constant value ~~{a, b, de, g}~~		* the second one is given by a enumerated set with identifier which are not used for the constant names.<br>For example '''{a, b, de, g}''' declares 4 new identifiers ('''a''', '''b''', '''de''', '''g''') that could be used to set constant value<br>
	* the third is a sugar form of the previous one. For example ...		* 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===		===Setting constant value===
	A constant value is given by a B expression. A value declared in a set value could be used.		A constant value is given by a B expression. A value declared in a set value could be used.

imported>Christophe at 20:19, 6 July 2009

2009-07-06T20:19:29Z

← Older revision		Revision as of 20:19, 6 July 2009
Line 6:		Line 6:
	===Setting set value===		===Setting set value===
	Three possible is avalaible.		Three possible is avalaible.
	* the first one is implicitly given by the axioms. This is the case for enumerated set.~~<br>Example: the following declares 4 new identifiers that could be used to set constant value {a, b, de, g}~~		* 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.		* the second one is given by a enumerated set with identifier which are not used for the constant names.<br>Example: the following declares 4 new identifiers ('''a''', '''b''', '''de''', '''g''') that could be used to set constant value {a, b, de, g}
	* the third is a sugar form of the previous one. For example ...		* the third is a sugar form of the previous one. For example ...
	===Setting constant value===		===Setting constant value===

imported>Christophe at 20:17, 6 July 2009

2009-07-06T20:17:54Z

← Older revision		Revision as of 20:17, 6 July 2009
Line 6:		Line 6:
	===Setting set value===		===Setting set value===
	Three possible is avalaible.		Three possible is avalaible.
	* the first one is implicitly given by the axioms. This is the case for enumerated set.		* the first one is implicitly given by the axioms. This is the case for enumerated set.<br>Example: the following declares 4 new identifiers that could be used to set constant value {a, b, de, g}

	* the second one is given by a enumerated set with identifier which are not used for the constant names.		* the second one is given by a enumerated set with identifier which are not used for the constant names.

imported>Christophe at 20:15, 6 July 2009

2009-07-06T20:15:53Z

← Older revision		Revision as of 20:15, 6 July 2009
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 avalaible.
			* 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.
			* the third is a sugar form of the previous one. For example ...
			===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.

imported>Christophe: /* The animation editor */

2009-07-05T20:53:05Z

The animation editor

← Older revision		Revision as of 20:53, 5 July 2009
Line 37:		Line 37:
	<br>		<br>
	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 :<br>		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 :<br>
	[[Image:~~Editor~~.png\|~~638~~:px\|center]]		[[Image:Editor1.png\|978:px\|center]]
	=== Model page ===		=== Model page ===
	The model page is split in two parts:		The model page is split in two parts:

imported>Christophe: /* The animation editor */

2009-07-05T20:48:09Z

The animation editor

← Older revision		Revision as of 20:48, 5 July 2009
Line 37:		Line 37:
	<br>		<br>
	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 :<br>		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 :<br>
	[[Image:~~editor~~.png\|638:px\|center]]		[[Image:Editor.png\|638:px\|center]]
	=== Model page ===		=== Model page ===
	The model page is split in two parts:		The model page is split in two parts: