Difference between pages "ADVANCE D3.2 Improvement of automated proof" and "AnimB Javascript Tutorial"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Christophe
 
Line 1: Line 1:
−
== Overview ==
+
This page discribes how to build a graphical animation for a event-b model.
−
The automated prover enhancement was a continuous task since the birth of the Rodin platform. It could be achieved by core platform internal refactorings and enhancements, but also by adding some external reasoning ability such as external provers.<br>
+
These animations are built following the pattern MVC (Model/View/Controller).
−
From the core platform point of view, and within the ten first month of ADVANCE, it consisted into two tasks: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. The user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations. The user can furthermore share and backup these defined tactics using the provided import/export mechanism.<br>
 
−
From an external point of view, the SMT Solvers plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. It is maintained in the time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.
 
  
−
== Motivations / Decisions ==
+
The view part is done by a browser and a HTML page.
−
Since Rodin 2.4,  a new tactic combinator 'Attempt after Lasso' is available in auto tactic profile editor and the import/export of profiles has been made possible. Indeed, a user that elaborates a good profile for a certain kind of proof pattern can thus share this profile thus increasing the number of automatic proofs.
+
The model part is given by a running animation in the Rodin plateform through AnimB and a event-b model.
 +
The controller is ensured by a piece of javascript code running in the browser.
  
−
Two main reasons mainly motivate the integration of SMT solvers into the Rodin platform. Firstly, to allow Rodin to benefit from the know capacity of such solvers in the field of arithmetics. Secondly, to extract some useful informations from the proofs that these solvers produce such as unsatisfiable cores, in order to significantly decrease the proving time of a modified model.
+
= The installation =
 +
In your Event-B project, create a directory called "animation".  
 +
Then dowload the two following files in this directory:
 +
* [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/AnimB/org.animb.jscomponent/animation/AnimB.js AnimB.js] the AnimB javascript component
 +
* [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/AnimB/org.animb.jscomponent/animation/index.html index.html] a basic HTML file. This file could be used to create your own animation.
  
−
== Available Documentation ==
+
= Create your own animation =
−
{{TODO|Fill this paragraph.}}
 
  
−
== Planning ==
+
First you must set the three variables describing your project.
−
{{TODO|Fill this paragraph.}}
+
* project this variable must be to set with the Rodin project name
−
 
+
* model this variable must be to set with the model used to build the animation
−
== References ==
 
−
<references/>
 
−
 
 
−
[[Category:ADVANCE D3.2 Deliverable]]
 

Revision as of 12:37, 10 October 2010

This page discribes how to build a graphical animation for a event-b model. These animations are built following the pattern MVC (Model/View/Controller).

The view part is done by a browser and a HTML page. The model part is given by a running animation in the Rodin plateform through AnimB and a event-b model. The controller is ensured by a piece of javascript code running in the browser.

The installation

In your Event-B project, create a directory called "animation". Then dowload the two following files in this directory:

  • AnimB.js the AnimB javascript component
  • index.html a basic HTML file. This file could be used to create your own animation.

Create your own animation

First you must set the three variables describing your project.

  • project this variable must be to set with the Rodin project name
  • model this variable must be to set with the model used to build the animation
Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.2_Improvement_of_automated_proof&oldid=717’