AnimB limitations - Revision history

imported>Christophe at 08:56, 27 September 2010

2010-09-27T08:56:23Z

@@ Line 25: / Line 25: @@
 * AnimB cannot deal with integer parameters and quantified integer variables, unless AnimB finds out that they range over a finite number of integers.
 [[Category:User documentation]]
 [[Category:AnimB]]

imported>Wohuai at 11:13, 20 November 2008

2008-11-20T11:13:00Z

← Older revision		Revision as of 11:13, 20 November 2008
Line 17:		Line 17:
	* Avoid all sorts of relational operators (<math>\pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij,		* Avoid all sorts of relational operators (<math>\pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij,
	\rel, \trel, \srel, \strel</math>).		\rel, \trel, \srel, \strel</math>).
	* AnimB is not good in inferring the types of ~~parameters and~~ quantified variables~~. For each event parameter you might need a guard stating the type of the parameter~~. For each quantified variable you have to state the type of the variable. Write:		* AnimB is not good in inferring the types of quantified variables. For each quantified variable you have to state the type of the variable. Write:
	# <math>\forall x\qdot x \in PERSON \limp x \in \dom(mother)</math>		# <math>\forall x\qdot x \in PERSON \limp x \in \dom(mother)</math>
	# <math>\exists x\qdot x \in PERSON \land x \in \ran(mother)</math>		# <math>\exists x\qdot x \in PERSON \land x \in \ran(mother)</math>
Line 23:		Line 23:
	# <math>\forall x\qdot x \in \dom(mother)</math>		# <math>\forall x\qdot x \in \dom(mother)</math>
	# <math>\exists x\qdot x \in \ran(mother)</math>		# <math>\exists x\qdot x \in \ran(mother)</math>
	* AnimB cannot ~~really~~ deal with integers.		* AnimB cannot deal with integer parameters and quantified integer variables, unless AnimB finds out that they range over a finite number of integers.

	==Avoid Simultaneous Animation of All Machines==		==Avoid Simultaneous Animation of All Machines==

imported>Mathieu: cat

2008-10-02T09:25:12Z

cat

← Older revision		Revision as of 09:25, 2 October 2008
Line 36:		Line 36:
	** Add trivial typing invariants to avoid error messages from the type checker.		** Add trivial typing invariants to avoid error messages from the type checker.
	* If you have not already done that in <b>m</b>, add type information for parameters and quantified variables.		* If you have not already done that in <b>m</b>, add type information for parameters and quantified variables.
			[[Category:User documentation]]
			[[Category:AnimB]]

imported>Wohuai: New page: When you try to animate a non-trivial model, it might happen that you get an internal error. It might also happen that some events are gray, which means that the animator is unable to eval...

2008-10-02T09:21:42Z

New page: When you try to animate a non-trivial model, it might happen that you get an internal error. It might also happen that some events are gray, which means that the animator is unable to eval...

New page

When you try to animate a non-trivial model, it might happen that you get an
internal error.
It might also happen that some events are gray, which means that the animator is unable
to evaluate their guards.
Below we list some guidelines of how to prevent such problems. This page will be continuously updated.

==Finding the Source of the Problem==

AnimB sends error messages to the "Console" (Window -> Show View -> Other -> General -> Console).
This error messages might help you to find out the places of your model that you have to change.

==How To Write Your Event-B Models==

AnimB cannot properly deal with every Event-B model. If you want to animate your model, you have to write it in a certain way. We give some guidelines, which you have to apply to any machine and any context.

* AnimB (currently) does not read invariants, theorems, the variant, or axioms. So changing any of them will not solve problems with the animator.
* Avoid all sorts of relational operators (<math>\pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij,
\rel, \trel, \srel, \strel</math>).
* AnimB is not good in inferring the types of parameters and quantified variables. For each event parameter you might need a guard stating the type of the parameter. For each quantified variable you have to state the type of the variable. Write:
# <math>\forall x\qdot x \in PERSON \limp x \in \dom(mother)</math>
# <math>\exists x\qdot x \in PERSON \land x \in \ran(mother)</math>
Do not write:
# <math>\forall x\qdot x \in \dom(mother)</math>
# <math>\exists x\qdot x \in \ran(mother)</math>
* AnimB cannot really deal with integers.

==Avoid Simultaneous Animation of All Machines==
The animator tries to animate all machines simultaneously, not only the
last one. If you do not want to adopt all your machines so that the animator can
handle them, you might apply the following steps:

* Create a new machine m_anim that refines the machine m you want to animate. The new machine m_anim should have the same events as m.
* Change m_anim such that it does not refine m anymore.
** Set the field "Abstract Machine" in "Dependencies" to "None".
** Remove all "Refines" clauses from all events.
** Add trivial typing invariants to avoid error messages from the type checker.
* If you have not already done that in m, add type information for parameters and quantified variables.