Difference between pages "ADVANCE D3.2 Language extension" and "AnimB limitations"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Im06r
 
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...)
 
Line 1: Line 1:
−
== Overview ==
+
When you try to animate a non-trivial model, it might happen that you get an
−
Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions).  
+
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.
  
−
The Theory plugin provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. The theory component is used to hold mathematical extensions (datatypes, operators with direct definitions, operators with recursive definitions and operators with axiomatic definitions), and proof extensions (polymorphic theorems, rewrite and inference rules). Theories are developed in the workspace (akin to models), and are subject to static checking and proof obligation generation. Proof obligations generated from theories ensure any contributed extensions do not compromise the soundness of the existing infrastructure for modelling and proof. In essence, the Theory plugin provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.
+
==Finding the Source of the Problem==
  
−
== Motivations / Decisions ==
+
AnimB sends error messages to the "Console" (Window -> Show View -> Other -> General -> Console).
−
{{TODO|Fill this paragraph.}}
+
This error messages might help you to find out the places of your model that you have to change.
  
−
== Available Documentation ==
+
==How To Write Your Event-B Models==
−
{{TODO|Fill this paragraph.}}
 
  
−
== Planning ==
+
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.
−
Issam Maamria will not be part of Advance after July 31, 2012.
 
  
−
== References ==
+
* AnimB (currently) does not read invariants, theorems, the variant, or axioms. So changing any of them will not solve problems with the animator.
−
<references/>
+
* 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.
  
−
[[Category:ADVANCE D3.2 Deliverable]]
+
==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 09:21, 2 October 2008

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 (\pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij, \rel, \trel, \srel, \strel).
  • 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:
  1. \forall x\qdot x \in PERSON \limp x \in \dom(mother)
  2. \exists x\qdot x \in PERSON \land x \in \ran(mother)

Do not write:

  1. \forall x\qdot x \in \dom(mother)
  2. \exists x\qdot x \in \ran(mother)
  • 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.
Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.2_Language_extension&oldid=737’