Difference between pages "AnimB limitations" and "AnimB roadmap"

From Event-B
(Difference between pages)
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
(New page: The following array describes the features which will be developed. {| border="1" cellpadding="20" cellspacing="0" !feature !description |- |History saving |The history saving allows the u...)
 
Line 1: Line 1:
When you try to animate a non-trivial model, it might happen that you get an
+
The following array describes the features which will be developed.
internal error.
+
{| border="1" cellpadding="20" cellspacing="0"
It might also happen that some events are gray, which means that the animator is unable
+
!feature
to evaluate their guards.
+
!description
Below we list some guidelines of how to prevent such problems. This page will be continuously updated.
+
|-
 
+
|History saving
==Finding the Source of the Problem==
+
|The history saving allows the user to save and replay a saved history
 
+
|-
AnimB sends error messages to the "Console" (Window -> Show View -> Other -> General -> Console).
+
|Predicate evaluator
This error messages might help you to find out the places of your model that you have to change.
+
|Actually the predicate evaluator don't use type information to infer a set that allow iteration of variable.
 
+
|-
==How To Write Your Event-B Models==
+
|Sorter on event table column
 
+
|The events, constants and variables are listed using the editing order given by the Rodin database. This new feature could allow the user to manage the order of events, constants and variables.
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 <b>any</b> machine and <b>any</b> context.
+
|-
 
+
|Extension of predicate evaluator
* AnimB (currently) does not read invariants, theorems, the variant, or axioms. So changing any of them will not solve problems with the animator.
+
|Actually, the predicate evaluator don't allow the variable quantification with function sets (injection, bijection, ...)
* 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 <b>m_anim</b> that refines the machine <b>m</b> you want to animate. The new machine <b>m_anim</b> should have the same events as <b>m</b>.
 
* Change <b>m_anim</b> such that it does not refine <b>m</b> 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 <b>m</b>, add type information for parameters and quantified variables.
 

Revision as of 21:11, 3 March 2009

The following array describes the features which will be developed.

feature description
History saving The history saving allows the user to save and replay a saved history
Predicate evaluator Actually the predicate evaluator don't use type information to infer a set that allow iteration of variable.
Sorter on event table column The events, constants and variables are listed using the editing order given by the Rodin database. This new feature could allow the user to manage the order of events, constants and variables.
Extension of predicate evaluator Actually, the predicate evaluator don't allow the variable quantification with function sets (injection, bijection, ...)