Difference between pages "Rodin Editor" and "UML-B"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
 
Line 1: Line 1:
{{TOCright}}
 
 
Return to [[Rodin Plug-ins]]
 
Return to [[Rodin Plug-ins]]
  
[[Image:RodinEditor_basicView1.png|400px|left|a basic view of the Rodin Editor on a context]]
+
UML-B provides a 'UML-like' graphical front end for Event-B. It provides various diagrammatic modelling notations and editors for creating models which are then translated into Event-B for verification. [[UML-B]] works alongside Event-B allowing the modeller to model in normal Event-B but also contribute some aspects of the model via diagrams.
  
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.
+
Our [https://www.uml-b.org UML-B] website contains more information about installing UML-B and getting started, as well as our current research and collaborations.
  
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.
+
UML-B is a collection of diagrammatic editors for Event-B. The diagrams are used to elaborate the machine and its content with extra model features. The diagrams may either by contained within the machine they contribute to, or can be contained in a separate UML-B model file that is linked to the machine.
<br style="clear: both" />
 
  
Please have a look also at the [[Rodin Editor User Guide]].
+
* [[Image:IUMLB.png]] [[Event-B Statemachines| State-machine diagrams]] a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine.
=== Current version ===
 
Since Rodin 2.4, release on February 2nd, the Rodin Editor is part of the core platform.
 
  
Thus, the Rodin Editor is no longer available as a separate plug-in from the main Rodin update site.
+
* [[Image:IUMLB.png]] [[Event-B Classdiagrams| Class diagrams]] a class diagram editor which can be used to define data entities and their relationships and to lift behaviour based on data sets.
  
=== Principles ===
+
==Lectures==
'''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:
+
* [[Media:iUML-BClassDiagramsLecture.pdf | UML-B Class-diagrams Lecture]] : Lecture slides on the use of UML-B Class-diagrams
* 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"''.
+
* [[Media:iUML-BStatemachinesLecture.pdf | UML-B State-machines Lecture]] : Lecture slides on the use of UML-B State-machines.
  
'''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:
+
==Tutorials==
* 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)
+
* [[iUML-B Class-diagrams Tutorial]] : A tutorial on the use of UML-B Class-diagrams.
[[Image:RodinEditor_basicView4.png|500px|center]]
 
  
=== A basic overview ===
+
* [[iUML-B State-machines Tutorial]] : A tutorial on the use of UML-B State-machines.
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]]
+
==Guidelines==
  
On the figure above, you see the context component.<br>
+
* [[UML-B - Modelling a control system]] : Some guidelines on modelling styles for a control system
* 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:User documentation]]
 +
[[Category:UML-B]]
 
[[Category:Plugin]]
 
[[Category:Plugin]]
[[Category:User documentation]]
 

Revision as of 22:09, 30 September 2020

Return to Rodin Plug-ins

UML-B provides a 'UML-like' graphical front end for Event-B. It provides various diagrammatic modelling notations and editors for creating models which are then translated into Event-B for verification. UML-B works alongside Event-B allowing the modeller to model in normal Event-B but also contribute some aspects of the model via diagrams.

Our UML-B website contains more information about installing UML-B and getting started, as well as our current research and collaborations.

UML-B is a collection of diagrammatic editors for Event-B. The diagrams are used to elaborate the machine and its content with extra model features. The diagrams may either by contained within the machine they contribute to, or can be contained in a separate UML-B model file that is linked to the machine.

  • IUMLB.png State-machine diagrams a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine.
  • IUMLB.png Class diagrams a class diagram editor which can be used to define data entities and their relationships and to lift behaviour based on data sets.

Lectures

Tutorials

Guidelines