Difference between pages "ADVANCE D3.2 Improvement of automated proof" and "Rodin Editor"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
 
imported>Tommy
 
Line 1: Line 1:
−
= Overview =
+
{{TOCright}}
−
In an Event-B development, more than 60% of the time is spent on proofs. That explains why all users are naturally keen for the proofs to be as automatic as possible and why the automated prover enhancement was a continuous task since the birth of the Rodin platform.
+
Return to [[Rodin Plug-ins]]
−
Enhancing the automated prover can be achieved by core platform refactorings and additions to it, such as the addition of integrated reasoners and tactics, but also by the integration of some external reasoning ability such as external provers (e.g., SMT solvers).<br>
 
−
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 Solver Integration plug-in allowing to use the SMT solvers within Rodin as 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 =
+
[[Image:RodinEditor_basicView1.png|400px|left|a basic view of the Rodin Editor on a context]]
−
The proportion of automatically discharged proof obligations heavily depends on Auto-Tactic configuration. Sometimes, the automatic prover fails because the tactics are applied in an unappropriate order. Since Rodin 2.4,  a new tactic combinator 'Attempt after Lasso' is available in the tactic profile editor as well as an import/export feature. Indeed, a user that elaborates a good profile for a certain proof pattern is now able to share or backup this profile thus increasing the number of automatic proofs for a given proof pattern.
 
  
−
Two main reasons mainly motivated the integration of SMT solvers into the Rodin platform. Firstly, to allow Rodin to benefit from the known capacity of such solvers in the field of arithmetics. Secondly, to extract some useful information from the proofs that these solvers produce such as unsatisfiable cores, in order to significantly decrease the proving time of a modified model. The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory.
+
The Rodin Editor is an editor, based on the same principles as the historical structured Event-B Editor. This latter editor shown its weakness while editing large models. Moreover, it was impossible to show some information, which are needed when one edits an Event-B model (such as the inherited elements which were formerly displayed only in the pretty print view). This is to solve all these issues that the Rodin Editor was created.
  
−
= Available Documentation =
+
This editor aims to be clean, in order to read easily models, but new comers may find it less easy to use. Please read the '''Principles''' section to get the necessary background to understand how this editor works. Furthermore, the text base of this editor aims to bring with it all the navigation and edition ease provided by text editor.
−
A page<ref>http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic</ref> concerning tactic profiles is available in the user manual.<br>
+
<br style="clear: both" />
−
A page<ref>http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in</ref> is dedicated to the SMT Solver integration plug-in on the Event-B wiki.
 
  
−
= Planning =
+
Please have a look also at the [[Rodin Editor User Guide]].
−
Enhancement to automated proof will continue during the ADVANCE project. This will be mainly achieved by the implementation of the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, and by the addition of new ones.
+
=== Current version ===
 +
The current version for <b>Rodin 2.3</b> is 0.5.1 released on Monday 3 October 2011. This version is similar to v.0.5.0 but made compatible with Rodin 2.3<br>
 +
The current version for <b>Rodin 2.2.x</b> is 0.5.0 released on Wednesday 13 July 2011. This version is not compatible with Rodin 2.3<br>
 +
''<span style="color:#FF4500">IMPORTANT : we identified a source of concurrency in the current version (0.5.0) of the plug-in.</span>''<br>
 +
<span style="color:#FF4500">'''To avoid any trouble, please do not generate files while having some Rodin Editor open, and edit only one model per project at once.'''</span>
  
−
Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE. In particular, the translation to SMT-LIB will be completed by adding some support for mathematical extensions.
+
=== Principles ===
 +
'''The component contents are displayed as text.''' Once you component opened with the Rodin Editor, its contents are printed as text inside the Rodin Editor. However, as said, the Rodin Editor is not a text editor, and even if the component you edit is streamlined to basic text, what you edit is stored in an underlying database. That's the reason why you can not type text at any place at any moment. (i.e. there is no parsing of text file: what you see is a text component based form editor).
  
−
Finally, connecting other provers (such as Super Zenon and iProver) to the platform will be investigated.
+
'''There are two types of edition possible.''' Because Rodin manipulates Event-B elements and their attributes, the Rodin Editor provides two ways to modify Event-B models:
 +
* you can navigate through the model contents and do things on the Event-B elements (e.g. add/remove/move/etc.) with the right-click actions or the keyboard shortcuts, depending on where is your cursor, or what you selected,
 +
* you can edit the Event-B element's attributes by entering the "edition" mode provided by the overlay editor. This is detailed here-after.
  
−
= References =
+
'''An overlay editor displays over the text to edit element's attributes''' The basic idea is: ''"when I want to edit some contents, I should open the overlay editor that will allow me to modify its value"''.
−
<references/>
 
  
−
[[Category:ADVANCE D3.2 Deliverable]]
+
'''Everything happens where I click, or where my text caret is.''' The caret position, also set when the user left-clicks in the editor, is the base for component modifications:
 +
* if you click an editable attribute, the overlay editor opens on it and you are able to modify the attribute. The same action is possible if you press "Backspace" if the caret is on an editable attribute,
 +
* if you click on non editable places of the editor, you just move the text caret to the pointed position.
 +
 
 +
'''Implicit elements are displayed in grayed colors.''' The elements that are implicit at the current level of edition are not editable, and displayed in grayed colors. (See the figure below)
 +
[[Image:RodinEditor_basicView4.png|400px|center]]
 +
 
 +
=== A basic overview ===
 +
The Rodin Editor might not be the 'preferred' editor that Rodin uses to open your Event-B models.<br>
 +
Thus, to open a component (e.g. a machine, a context, etc.), '''right-click''' on it and select '''Open with''' > '''Rodin Editor'''.<br>
 +
The context component is then opened with the Rodin Editor.<br>
 +
 
 +
[[Image:RodinEditor_basicView2.png|600px]]
 +
 
 +
On the figure above, you see the context component.<br>
 +
* The user is editing the axiom ''axm8'' and we see that the text is black and the background is grayed. This is the actually the overlay editor, that is open to edit the predicate contained by the axiom ''axm8''.
 +
* There are buttons in the left ruler to fold some elements.
 +
* The comments are preceeded by the character ' › ' to indicate where to click for edition.
 +
* The other attributes are inlined as grayed text.
 +
** Note that : some attributes have type boolean, thus change value on click, and some attributes are choice attributes thus display a list of clickable values (see the image below) on click.
 +
 
 +
[[Image:RodinEditor_basicView3.png|center]]
 +
 
 +
For more details, please go to the [[Rodin_Editor_User_Guide| Rodin Editor User Guide]].
 +
 
 +
[[Category:Plugin]]
 +
[[Category:User documentation]]

Revision as of 14:09, 3 October 2011

Return to Rodin Plug-ins

a basic view of the Rodin Editor on a context

The Rodin Editor is an editor, based on the same principles as the historical structured Event-B Editor. This latter editor shown its weakness while editing large models. Moreover, it was impossible to show some information, which are needed when one edits an Event-B model (such as the inherited elements which were formerly displayed only in the pretty print view). This is to solve all these issues that the Rodin Editor was created.

This editor aims to be clean, in order to read easily models, but new comers may find it less easy to use. Please read the Principles section to get the necessary background to understand how this editor works. Furthermore, the text base of this editor aims to bring with it all the navigation and edition ease provided by text editor.

Please have a look also at the Rodin Editor User Guide.

Current version

The current version for Rodin 2.3 is 0.5.1 released on Monday 3 October 2011. This version is similar to v.0.5.0 but made compatible with Rodin 2.3
The current version for Rodin 2.2.x is 0.5.0 released on Wednesday 13 July 2011. This version is not compatible with Rodin 2.3
IMPORTANT : we identified a source of concurrency in the current version (0.5.0) of the plug-in.
To avoid any trouble, please do not generate files while having some Rodin Editor open, and edit only one model per project at once.

Principles

The component contents are displayed as text. Once you component opened with the Rodin Editor, its contents are printed as text inside the Rodin Editor. However, as said, the Rodin Editor is not a text editor, and even if the component you edit is streamlined to basic text, what you edit is stored in an underlying database. That's the reason why you can not type text at any place at any moment. (i.e. there is no parsing of text file: what you see is a text component based form editor).

There are two types of edition possible. Because Rodin manipulates Event-B elements and their attributes, the Rodin Editor provides two ways to modify Event-B models:

  • you can navigate through the model contents and do things on the Event-B elements (e.g. add/remove/move/etc.) with the right-click actions or the keyboard shortcuts, depending on where is your cursor, or what you selected,
  • you can edit the Event-B element's attributes by entering the "edition" mode provided by the overlay editor. This is detailed here-after.

An overlay editor displays over the text to edit element's attributes The basic idea is: "when I want to edit some contents, I should open the overlay editor that will allow me to modify its value".

Everything happens where I click, or where my text caret is. The caret position, also set when the user left-clicks in the editor, is the base for component modifications:

  • if you click an editable attribute, the overlay editor opens on it and you are able to modify the attribute. The same action is possible if you press "Backspace" if the caret is on an editable attribute,
  • if you click on non editable places of the editor, you just move the text caret to the pointed position.

Implicit elements are displayed in grayed colors. The elements that are implicit at the current level of edition are not editable, and displayed in grayed colors. (See the figure below)

RodinEditor basicView4.png

A basic overview

The Rodin Editor might not be the 'preferred' editor that Rodin uses to open your Event-B models.
Thus, to open a component (e.g. a machine, a context, etc.), right-click on it and select Open with > Rodin Editor.
The context component is then opened with the Rodin Editor.

RodinEditor basicView2.png

On the figure above, you see the context component.

  • The user is editing the axiom axm8 and we see that the text is black and the background is grayed. This is the actually the overlay editor, that is open to edit the predicate contained by the axiom axm8.
  • There are buttons in the left ruler to fold some elements.
  • The comments are preceeded by the character ' › ' to indicate where to click for edition.
  • The other attributes are inlined as grayed text.
    • Note that : some attributes have type boolean, thus change value on click, and some attributes are choice attributes thus display a list of clickable values (see the image below) on click.
RodinEditor basicView3.png

For more details, please go to the Rodin Editor User Guide.

Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.2_Improvement_of_automated_proof&oldid=7114’