Difference between pages "Records Extension" and "Rodin Editor User Guide"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Colin
 
imported>Tommy
 
Line 1: Line 1:
This page is under development. It is intended to be a user oriented manual for using records in Event-B. This page should be read in conjunction with the  [[Structured_Types|Structured Types]] page which gives a more theoretical description of the origin of the Records extension.
+
== Introduction ==
  
==Introduction==
+
The Rodin Editor plug-in provides a structured editor to model in Event-B withing Rodin. This editor uses a textual representation, and edition is done through an overlay text editor and action depending on the caret position in the text.<br>
The Event-B mathematical language currently does not support a syntax for the direct definition of structured types such as records or class structures.
+
For more details about the principles of this editor,  see [[Rodin_Editor|the Rodin Editor Plug-in page]].<br>
The Records Extension introduces a new modelling construct to provide a notion of structured types in Event-B Contexts.
 
  
Currently, structured variables are not supported. Variables that are typed as an instance of a record type can be thought of as identifying a particular record value. Hence it is not possible to vary an individual field, the variable must be assigned a complete new record value instance. To vary an individual field this new record value instance can be selected to have the same field value for every other field.)
+
'''IMPORTANT FOR RODIN PLATFORMS BELOW RODIN 2.5''' :  ''we identified a source of concurrency issue in the current version (0.5.0) of the plug-in.''<br>
 +
'''The Rodin Editor is not maintained for these versions of Rodin  since Rodin 2.4. Please try to upgrade your plaform to the latest [[Rodin_Platform_Releases | version of Rodin available]].'''
 +
'''To avoid any trouble, please do not generate files while having some Rodin Editor open, and edit only one model per project at once.'''
  
==UI Extensions==
+
== Installation ==
The '''Event-B editor''' is extended to include two new top level clauses. These are '''Record Declarations''' and '''Record Extensions'''.
 
  
Records (or sub-records) are introduced in the Record Declarations clause. Records that are introduced here without a '''Supertypes''' clause are equivalent to carrier sets. Those that have a Supertypes clause are equivalent to constants that are a subset of the referenced (i.e. subtyped) record.
+
=== Setup ===
 +
Since Rodin 2.4, the Rodin Editor is part of the core platform (i.e. it is pre-installed and available out of the box).
 +
Once you've installed Rodin 2.4 or upper, you are ready to use the Rodin Editor plug-in.
  
Record Extensions may only add new fields to a record that has previously been declared in a Record Declaration. The extended record is referenced in an 'extends' clause.
+
=== Release Notes ===
 +
See [[Rodin_Editor_Release_History | Rodin Editor Release Notes]]
  
The '''Event-B navigator''' is extended to show a new node '''Records'''. Under this node are listed the records and records extensions in the Context.
 
Record Extensions are displayed as the name of the extended record appended with a + sign. Each record or record extension can be expanded to show the owned fields. (Note that this list is not cumulative, only the new fields are shown).
 
(Currently in the Navigator, the Records node is shown as the first item in the Context whereas eleswhere it appears between carrier sets and constants. This is due to a limitation in the Rodin tool extension facilities).
 
  
The '''Outline''' panel shows the records followed by record extensions as a plain list without the Records node. Again, the record or record extension can be expanded to show the fields.
+
== Editing ==
  
In all  cases, the '''icon''' used for a record reflects its equivalence. That is, if it does not have a supertypes clause, it is displayed with the same icon as a carrier set. otherwise it is displayed with the same icon as a constant.
+
This is a small exercice to get used to the principles of the new structured editor. It is based on the 'Celebrity' project of the tutorial. You can download the resulting project [http://sourceforge.net/projects/rodin-b-sharp/files/Doc_%20Tutorial/1.1/Celebrity.zip/download <tt>here</tt>].<br>
 +
We will here build the context ''Celebrity_C0''.
  
==Semantics of Records==
+
=== Create a context, add elements to it ===
The semantics of Records are given by their translation into 'pure' Event-B. This translation is performed by extensions to the static checker which generates a 'checked context' (.BCC file) containing pure Event-B from an unchecked (.BUC file) containing record elements. Hence the translated Event-B is not visible to the user.  
+
Let's create a Rodin project, and add a context component called ''Celebrity_C0'' to it.<br>
 +
-- By opening this context with the Rodin Editor (right click > Open with > Rodin Editor) you shall obtain the following:<br>
 +
[[Image:RodinEditor_UserGuide_step1.png]]
  
<formatting/presentation of this will be improved>
+
This editor allows to do things based on the position of the caret.<br>
 +
-- The caret is place at the front of the context name, and this is fine because we want to add a constant
 +
to the context.
 +
-- To add a constant, right click and select '[Child]-> Add Constant' as in the picture below:
  
Record R Supertypes <null> --> Carrier Set R
+
[[Image:RodinEditor_UserGuide_step3.png|400px]]
  
Record S Supertypes R          --> Constant S,   Axiom S : POW(R)
+
-- Save the file. <br>
 +
After saving the file, the error markers are recalculated, and you have an error that appears on the newly created constant 'cst1'.<br>
 +
You shall see something like this :
  
Field f : F                                -->  Constant f, Axiom f : R  --> F
+
[[Image:RodinEditor_UserGuide_step4.png|400px]]
  
[It may be instructive to open the *.bcc file with a text editor to examine the generated carrier sets, constants, and axioms]
+
Note that you can visualize the error message by going over the error marker with the mouse.
  
 +
-- Now we enter the edition mode by clicking inside the label 'cst1', as we want to name the constant 'cst1' to 'k'.
  
==Usage==
+
[[Image:RodinEditor_UserGuide_step5.png|550px]]
  
First define Records in the Record Declarations section. Some of these can subtype others but you need at least one that is not a subset, i.e. has no supertypes. Note that we decided not to allow records to subtype or extend Carrier Sets, but you can do the equivalent by defining a record without any fields and subtyping/extending that. Add fields and give them a type by entering an expression that evaluates to a set. (You can use records, fields, constants and sets  in the expression).
+
The overlay editor then appears (the background is grey and a box is drawn[see above]) and you can modify the label of the constant.<br>
 +
-- Modify the label to be 'k'and exit the overlay edition by pressing 'Enter' or click next to k. ''Note that because 'Enter' is used to enter or exit the overlay mode under the caret, in order to insert carriage return in text, you have to press CTRL+ENTER (Apple+Enter) on mac platforms.<br>''
 +
You can then save the file. <br>
 +
You then see something like the following.
  
For Record Extensions just select the record you want to add new fields to from the drop down list. and then add the new fields.
+
[[Image:RodinEditor_UserGuide_step6.png|300px]]
  
You can refer to records and fields in axioms/theorems. E.g., you could define a constant to be an instance of a record. In all cases you can refer to records and fields in the current or visible abstract (extended*) contexts.
+
Then we want to give this constant an integer type. As the caret is near 'k', and k is a constant, we will use '[Sibling]-> Add sibling' command to add an axiom.<br>
 +
-- Right-click and select "[Sibling]-> Add Axiom" you see then that a new axiom was created, named 'axm1'.
  
You use fields as if they were functions (which is what they are in the checked context).
+
[[Image:RodinEditor_UserGuide_step8.png|400px]]
e,g if r1, belongs to myRecord which has a field myField : NAT then I could write in a predicate... myField(r1) > 5
 
  
==Current Limitations==
+
You've just created an axiom that you can edit to give the constant k a type.
* Records are not supported by the Camille text editor (see warning below)
+
You can then enter the overlay edition mode to change this value to 'k : INT'.<br>
* Records are not supported by the Pretty print facility
+
After saving the file, you obtain the following context :
* Records are not supported by the Synthesis view facility
 
* Records are not supported by the EventB2Latex plug-in
 
* Records may have, at most, one supertype.
 
* Records may only have records as supertypes (not carrier sets)
 
  
==Warning==
+
[[Image:RodinEditor_UserGuide_step9.png|500px]]
  
Records are not supported in the Camille text editor. Editing a context that contains records with the Camille editor may result in the Records being lost.
+
and the markers disappear because there is no error left in your context.
 +
Finally, suppose that the axiom axm1 should be considered as a theorem, click on not theorem after the axiom formula, to change the attribute of the predicate to a theorem.
  
[[Category:Work in progress]] [[Category:Design]]
+
''' CONGRATULATIONS! You learned how to use the Rodin Editor.'''
 +
You learned that :
 +
# To create an element:
 +
## or you place the caret before the label of its parent, and create a child using '[Child]->Add xxx' where xxx is the type of element you want to add, from the contextual menu,
 +
## or you place the caret next to a sibling element and you create a sibling using '[Sibling]->Add xxx' where xxx is the type of element you want to add, from the contextual menu.
 +
# To edit the attributes of an element:
 +
## you enter the overlay edition with left click or with "ENTER" and modify the textual contents,
 +
## you press 'ENTER' to quit overlay edition (or click outside the overlay editor).
 +
 
 +
=== Select, Move and delete elements ===
 +
 
 +
-- To select elements, you can double-click on them, or press CTRL and click on one element. The selected elements appear with a blue background,
 +
or a gray background if they are of different types. See the picture below.
 +
 
 +
[[Image:RodinEditor_UserGuide_step11.png|350px]]
 +
 
 +
-- To unselect element, by default, press ESC.
 +
 
 +
-- To move elements, try both:
 +
* Move Up and Move Down commands in the context menu, once elements are selected,
 +
* Drag and drop on the selection.
 +
 
 +
-- To delete elements, try both:
 +
* Use the 'Delete' command on a selection from the context menu,
 +
* Press the DEL or SUPPR key after selecting the elements you want to delete.
 +
 
 +
=== Using keyboard shorcuts ===
 +
Here is the list of the currently key bindings which are set by default and specific to the Rodin Editor.
 +
 
 +
{{SimpleHeader}}
 +
|-
 +
! scope=col | KEY SEQUENCE || ACTION
 +
|-
 +
| BACKSPACE (ENTER) || Enter the edition mode using the overlay editor if the caret is on an editable place.
 +
|-
 +
| DEL || Suppress the element after the caret position
 +
|-
 +
| ALT+T || Add a sibling of the element pointed by the caret position. The sibling is placed just after this latter one.
 +
|-
 +
| ALT+G || Opens a popup to select the element type of the child to add to the element pointed by the caret position. Note that if there is only one child type, the child will be directly created.
 +
|-
 +
| CTRL+BACKSPACE || Insert a new carriage return while editing with the overlay editor.
 +
|-
 +
| ALT+ARROW_UP || Move up the selected elements.
 +
|-
 +
| ALT+ARROW_DOWN || Move down the selected elements.
 +
|-
 +
| SHIFT+ARROW_UP || Select elements up.
 +
|-
 +
| SHIFT+ARROW_DOWN || Select elements down.
 +
|-
 +
| ESC || Quit the current overlay edition (if any) and forget the modifications made, frees the current selection.
 +
|-
 +
| TAB || Go to the next editable place (i.e. to the next editable element attribute)
 +
|-
 +
| SHIFT+TAB || Go to the previous editable place (i.e. to the next editable element attribute)
 +
|}
 +
 
 +
=== Customize these shortcuts ===
 +
If you don't like these shortcuts, you can modify them by setting your own key preferences.
 +
To do so, go to Window > Preferences and then General > Key. A table appears were you can find and edit the shortcuts.
 +
 
 +
<!--== Tips & Tricks ==
 +
A command currently disable the possibility to use the ESC instead of ALT+ESC sequence. This is quite cumbersome, and can be tuned!
 +
To do so, open the preference table for key shortcuts (described above) and after ensuring you disabled the filters of uncategorized commands (using the Filters... dialog)
 +
search for the command named "Restore Styles". This is the command to release the highlights in the proving views. You can then swith the sequence of this command to ALT+ESC and change the value of the "Abort edition and free selected items" command to ESC. After applying these settings, the shortcuts will be modified as wished above.
 +
-->

Revision as of 10:09, 18 July 2012

Introduction

The Rodin Editor plug-in provides a structured editor to model in Event-B withing Rodin. This editor uses a textual representation, and edition is done through an overlay text editor and action depending on the caret position in the text.
For more details about the principles of this editor, see the Rodin Editor Plug-in page.

IMPORTANT FOR RODIN PLATFORMS BELOW RODIN 2.5 : we identified a source of concurrency issue in the current version (0.5.0) of the plug-in.
The Rodin Editor is not maintained for these versions of Rodin since Rodin 2.4. Please try to upgrade your plaform to the latest version of Rodin available. To avoid any trouble, please do not generate files while having some Rodin Editor open, and edit only one model per project at once.

Installation

Setup

Since Rodin 2.4, the Rodin Editor is part of the core platform (i.e. it is pre-installed and available out of the box). Once you've installed Rodin 2.4 or upper, you are ready to use the Rodin Editor plug-in.

Release Notes

See Rodin Editor Release Notes


Editing

This is a small exercice to get used to the principles of the new structured editor. It is based on the 'Celebrity' project of the tutorial. You can download the resulting project here.
We will here build the context Celebrity_C0.

Create a context, add elements to it

Let's create a Rodin project, and add a context component called Celebrity_C0 to it.
-- By opening this context with the Rodin Editor (right click > Open with > Rodin Editor) you shall obtain the following:
RodinEditor UserGuide step1.png

This editor allows to do things based on the position of the caret.
-- The caret is place at the front of the context name, and this is fine because we want to add a constant to the context. -- To add a constant, right click and select '[Child]-> Add Constant' as in the picture below:

RodinEditor UserGuide step3.png

-- Save the file.
After saving the file, the error markers are recalculated, and you have an error that appears on the newly created constant 'cst1'.
You shall see something like this :

RodinEditor UserGuide step4.png

Note that you can visualize the error message by going over the error marker with the mouse.

-- Now we enter the edition mode by clicking inside the label 'cst1', as we want to name the constant 'cst1' to 'k'.

RodinEditor UserGuide step5.png

The overlay editor then appears (the background is grey and a box is drawn[see above]) and you can modify the label of the constant.
-- Modify the label to be 'k'and exit the overlay edition by pressing 'Enter' or click next to k. Note that because 'Enter' is used to enter or exit the overlay mode under the caret, in order to insert carriage return in text, you have to press CTRL+ENTER (Apple+Enter) on mac platforms.
You can then save the file.
You then see something like the following.

RodinEditor UserGuide step6.png

Then we want to give this constant an integer type. As the caret is near 'k', and k is a constant, we will use '[Sibling]-> Add sibling' command to add an axiom.
-- Right-click and select "[Sibling]-> Add Axiom" you see then that a new axiom was created, named 'axm1'.

RodinEditor UserGuide step8.png

You've just created an axiom that you can edit to give the constant k a type. You can then enter the overlay edition mode to change this value to 'k : INT'.
After saving the file, you obtain the following context :

RodinEditor UserGuide step9.png

and the markers disappear because there is no error left in your context. Finally, suppose that the axiom axm1 should be considered as a theorem, click on not theorem after the axiom formula, to change the attribute of the predicate to a theorem.

CONGRATULATIONS! You learned how to use the Rodin Editor. You learned that :

  1. To create an element:
    1. or you place the caret before the label of its parent, and create a child using '[Child]->Add xxx' where xxx is the type of element you want to add, from the contextual menu,
    2. or you place the caret next to a sibling element and you create a sibling using '[Sibling]->Add xxx' where xxx is the type of element you want to add, from the contextual menu.
  2. To edit the attributes of an element:
    1. you enter the overlay edition with left click or with "ENTER" and modify the textual contents,
    2. you press 'ENTER' to quit overlay edition (or click outside the overlay editor).

Select, Move and delete elements

-- To select elements, you can double-click on them, or press CTRL and click on one element. The selected elements appear with a blue background, or a gray background if they are of different types. See the picture below.

RodinEditor UserGuide step11.png

-- To unselect element, by default, press ESC.

-- To move elements, try both:

  • Move Up and Move Down commands in the context menu, once elements are selected,
  • Drag and drop on the selection.

-- To delete elements, try both:

  • Use the 'Delete' command on a selection from the context menu,
  • Press the DEL or SUPPR key after selecting the elements you want to delete.

Using keyboard shorcuts

Here is the list of the currently key bindings which are set by default and specific to the Rodin Editor.


KEY SEQUENCE ACTION
BACKSPACE (ENTER) Enter the edition mode using the overlay editor if the caret is on an editable place.
DEL Suppress the element after the caret position
ALT+T Add a sibling of the element pointed by the caret position. The sibling is placed just after this latter one.
ALT+G Opens a popup to select the element type of the child to add to the element pointed by the caret position. Note that if there is only one child type, the child will be directly created.
CTRL+BACKSPACE Insert a new carriage return while editing with the overlay editor.
ALT+ARROW_UP Move up the selected elements.
ALT+ARROW_DOWN Move down the selected elements.
SHIFT+ARROW_UP Select elements up.
SHIFT+ARROW_DOWN Select elements down.
ESC Quit the current overlay edition (if any) and forget the modifications made, frees the current selection.
TAB Go to the next editable place (i.e. to the next editable element attribute)
SHIFT+TAB Go to the previous editable place (i.e. to the next editable element attribute)

Customize these shortcuts

If you don't like these shortcuts, you can modify them by setting your own key preferences. To do so, go to Window > Preferences and then General > Key. A table appears were you can find and edit the shortcuts.