AnimB limitations: Difference between revisions
From Event-B
Jump to navigationJump to search
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... |
imported>Christophe No edit summary |
||
| (2 intermediate revisions by 2 users not shown) | |||
| 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 | * 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 | * 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]] | |||
Latest revision as of 08:56, 27 September 2010
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 (
). - 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:
Do not write:
- AnimB cannot deal with integer parameters and quantified integer variables, unless AnimB finds out that they range over a finite number of integers.
