Difference between pages "Rodin Editor User Guide" and "Rodin Workshop 2021"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
 
Line 1: Line 1:
−
== Introduction ==
+
==9th Rodin User and Developer Workshop==
  
−
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 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)
−
For more details about the principles of this editor, see [[Rodin_Editor|the Rodin Editor Plug-in page]].
 
−
''<span style="color:#FF4500">IMPORTANT :  we identified a source of concurrency issue 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>
 
  
−
== Installation ==
+
''The proceedings of the workshop is now available as a [technical report] at the University of Southampton.''
  
−
=== Setup ===
+
The programme now available on [https://abz2021.uni-ulm.de/program-overview  the ABZ2021 website] and [[#Programme|below]] (with texts).
−
Install the Rodin Editor plug-in:
 
−
# In the menu choose Help -> Install New Software...
 
−
# In the Work with dropdown list, choose the location URL: Rodin - http://rodin-b-sharp.sourceforge.net/updates
 
−
# Select the Rodin Editor feature then click the check box
 
−
# Click Next, after some time, the Install Details page appears
 
−
# Click Next and accept the license
 
−
# Click Finish
 
−
# A Security Warning window may appear: click OK
 
−
# Restart Rodin as suggested.
 
−
Now you are ready to use the new Rodin Editor plug-in.
 
  
−
=== Release Notes ===
+
Event-B is a formal method for system-level modelling and analysis. The
−
See [[Rodin_Editor_Release_History | Rodin Editor Release Notes]]
+
Rodin Platform is an Eclipse-based toolset for Event-B that provides
 +
effective support for modelling and automated proof. The platform is open
 +
source and is further extendable with plug-ins. A range of plug-ins have
 +
already been developed.
  
 +
The 9th Rodin workshop will be collocated with the [https://abz2021.uni-ulm.de/ ABZ 2021 Conference].
  
−
== Editing ==
+
The purpose of this workshop  is to bring together existing and potential
 +
users and developers of the Rodin  toolset and to foster a broader community
 +
of Rodin users and developers.
  
−
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>
+
For Rodin users the workshop will provide an opportunity to share tool
−
We will here build the context ''Celebrity_C0''.
+
experiences and to gain an understanding of on-going tool developments.
 +
For plug-in developers the workshop will provide an opportunity to showcase
 +
their tools and to achieve better coordination of tool development effort.
  
−
=== Create a context, add elements to it ===
 
−
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]]
 
  
−
This editor allows to do things based on the position of the caret.<br>
+
=== Programme ===
−
-- Place the caret at one location on the line of the context label, and before the label, as on the figure below:
 
  
−
[[Image:RodinEditor_UserGuide_step2.png]]
+
'''09:00 - 10:30'''
 +
* Domain knowledge as Ontology-based Event-B Theories - ''I. Mendil, Y. Aït-Ameur, N. K. Singh, D. Méry, and P. Palanque'' ([[Media:RodinWorkshop2021_Domain knowledge as Ontology-based Event-B Theories.pdf|pdf]], [[Media:RodinWorkshop2021_Domain knowledge as Ontology-based Event-B Theories_slides.pdf|slides]])
 +
* OntoEventB: A Generator of Event-B contexts from Ontologies - ''Idir Ait-Sadoune'' ([[Media:RodinWorkshop2021_OntoEventB.pdf|pdf]], [[Media:RodinWorkshop2021_OntoEventB_slides.pdf|slides]])
 +
* EVBT — an Event-B tool for code generation and documentation - ''Fredrik Öhrström'' ([[Media:RodinWorkshop2021_EVBT.pdf|pdf]])
 +
* Scenario Checker: An Event-B tool for validating abstract models - ''Colin Snook, Thai Son Hoang, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler'' ([[Media:RodinWorkshop2021_Scenario Checker.pdf|pdf]], [[Media:RodinWorkshop2021_Scenario Checker_slides.pdf|slides]])
  
−
-- Then right click, and add a 'Constant' child using the menus :
+
'''10:30 - 11:00''' ''Break''
  
−
[[Image:RodinEditor_UserGuide_step3.png|600px]]
+
'''11:00--12:30'''
 +
* Context instantiation plug-in: a new approach to genericity in Rodin - ''Guillaume Verdier, Laurent Voisin'' ([[Media:RodinWorkshop2021_Context instantiation plug-in.pdf|pdf]], [[Media:RodinWorkshop2021_Context instantiation plug-in_slides.pdf|slides]])
 +
* Examples of using the Instantiation Plug-in - ''Dominique Cansell, Jean-Raymond Abrial'' ([[Media:RodinWorkshop2021_Examples of using the Instantiation Plug-in.pdf|pdf]], [[MEDIA:RodinWorkshop2021_Examples of using the Instantiation Plug-in_slides.pdf|slides]])
 +
* Data-types definitions: Use of Theory and Context instantiations Plugins - ''Peter Riviere, Yamine Ait-Ameur, and Neeraj Kumar Singh'' ([[Media:RodinWorkshop2021_Data-types_definitions.pdf|pdf]], [[Media:RodinWorkshop2021_Data-types_definitions_slides.pdf|slides]])
 +
* Towards CamilleX 3.0 - ''Thai Son Hoang, Colin Snook, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler'' ([[Media:RodinWorkshop2021_Towards CamilleX 3.0.pdf|pdf]], [[Media:RodinWorkshop2021_Towards CamilleX 3.0_slides.pdf|slides]])
  
−
-- Save the file. <br>
+
'''12:30--13:30''' ''Lunch''
−
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 this :
 
  
−
[[Image:RodinEditor_UserGuide_step4.png|600px]]
+
'''13:30--15:00'''
 +
* Keynote: Safety and Security Case Study Experiences with Event-B and Rodin - ''Jonathan Hammond, Capgemini Engineering'' ([[Media:RodinWorkshop2021_Safety and Security Case Study Experiences with Event-B and Rodin.pdf|slides]])
 +
* Large Scale Biological Models in Rodin - ''Usman Sanwal, Thai Son Hoang, Luigia Petre, and Ion Petre'' ([[Media:RodinWorkshop2021_Large Scale Biological Models in Rodin.pdf|pdf]], [[Media:RodinWorkshop2021_Large Scale Biological Models in Rodin_slides.pdf|slides]])
 +
* Formal Verification of EULYNX Models Using Event-B and RODIN - ''Abdul Rasheeq, Shubhangi Salunkhe'' ([[Media:RodinWorkshop2021_Formal Verification of EULYNX Models Using Event-B and RODIN.pdf|pdf]], [[MEDIA:RodinWorkshop2021_Formal Verification of EULYNX Models Using Event-B and RODIN_slides.pdf|slides]])
  
−
Note that you can visualize the error message by going over the error marker with the mouse.
+
=== Organisers ===
−
 
+
<p>Chair: Asieh Salehi Fathabadi, University of Southampton, UK</p>
−
-- Enter the edition mode by clicking inside the label 'cst1'.
+
<p>Co-chair: Thai Son Hoang, University of Southampton, UK</p>
−
 
+
<p>Co-chair: Colin Snook, University of Southampton, UK</p>
−
[[Image:RodinEditor_UserGuide_step5.png]]
+
<p>Co-chair: Yamine Ait Ameur, Toulouse National Polytechnique Institute, France</p>
−
 
 
−
The overlay editor then appears (cst1 is in black, and the background is gray[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'. ''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.<br>''
 
−
You can then save the file. <br>
 
−
You then see something like the following.
 
−
 
 
−
[[Image:RodinEditor_UserGuide_step6.png]]
 
−
 
 
−
Then we want to add another constant. As we have 'k' already, we will use 'add sibling' command to add another constant after k.<br>
 
−
-- Place the caret before k as on the following picture :
 
−
 
 
−
[[Image:RodinEditor_UserGuide_step7.png]]
 
−
 
 
−
-- Right-click. The following context menu appears :
 
−
 
 
−
[[Image:RodinEditor_UserGuide_step8.png|200px]]
 
−
 
 
−
-- Click on "Add Sibling" you see then that a new constant was created, named 'cst1'.
 
−
 
 
−
[[Image:RodinEditor_UserGuide_step9.png]]
 
−
 
 
−
You can then enter the overlay edition mode to change this value to 'c'.<br>
 
−
After saving the file, you obtain the following context :
 
−
 
 
−
[[Image:RodinEditor_UserGuide_step10.png]]
 
−
 
 
−
''' 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 'create child' in the contextual menu,
 
−
## or you place the caret next to a sibling element and you create a sibling using 'create sibling' in 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.
 
−
 
 
−
=== 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
 
−
|-
 
−
| CTRL+T || Add a sibling of the element pointed by the caret position. The sibling is placed just after this latter one.
 
−
|-
 
−
| CTRL+SHIFT+N || 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.
 
−
|-
 
−
| ALT+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 this list ===
 
−
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 (i.e. in Rodin 2.2) 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.
 

Latest revision as of 09:41, 29 June 2021

9th Rodin User and Developer Workshop

The 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)

The proceedings of the workshop is now available as a [technical report] at the University of Southampton.

The programme now available on the ABZ2021 website and below (with texts).

Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset for Event-B that provides effective support for modelling and automated proof. The platform is open source and is further extendable with plug-ins. A range of plug-ins have already been developed.

The 9th Rodin workshop will be collocated with the ABZ 2021 Conference.

The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers.

For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort.


Programme

09:00 - 10:30

  • Domain knowledge as Ontology-based Event-B Theories - I. Mendil, Y. Aït-Ameur, N. K. Singh, D. Méry, and P. Palanque (pdf, slides)
  • OntoEventB: A Generator of Event-B contexts from Ontologies - Idir Ait-Sadoune (pdf, slides)
  • EVBT — an Event-B tool for code generation and documentation - Fredrik Öhrström (pdf)
  • Scenario Checker: An Event-B tool for validating abstract models - Colin Snook, Thai Son Hoang, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler (pdf, slides)

10:30 - 11:00 Break

11:00--12:30

  • Context instantiation plug-in: a new approach to genericity in Rodin - Guillaume Verdier, Laurent Voisin (pdf, slides)
  • Examples of using the Instantiation Plug-in - Dominique Cansell, Jean-Raymond Abrial (pdf, slides)
  • Data-types definitions: Use of Theory and Context instantiations Plugins - Peter Riviere, Yamine Ait-Ameur, and Neeraj Kumar Singh (pdf, slides)
  • Towards CamilleX 3.0 - Thai Son Hoang, Colin Snook, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler (pdf, slides)

12:30--13:30 Lunch

13:30--15:00

  • Keynote: Safety and Security Case Study Experiences with Event-B and Rodin - Jonathan Hammond, Capgemini Engineering (slides)
  • Large Scale Biological Models in Rodin - Usman Sanwal, Thai Son Hoang, Luigia Petre, and Ion Petre (pdf, slides)
  • Formal Verification of EULYNX Models Using Event-B and RODIN - Abdul Rasheeq, Shubhangi Salunkhe (pdf, slides)

Organisers

Chair: Asieh Salehi Fathabadi, University of Southampton, UK

Co-chair: Thai Son Hoang, University of Southampton, UK

Co-chair: Colin Snook, University of Southampton, UK

Co-chair: Yamine Ait Ameur, Toulouse National Polytechnique Institute, France

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Editor_User_Guide&oldid=14475’