Difference between pages "TextEditor EBNF" and "UML-B"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Fabian
 
m (move content of iUML-B page to this one)
 
Line 1: Line 1:
{| align="right"
+
Return to [[Rodin Plug-ins]]
| __TOC__
 
|}
 
This page describes the text syntax for Event-B models in the TextEditor. It shows an EBNF and explains some details and design decisions.
 
  
See the [[Text_Editor]] page for details of the editor and the usage of the text syntax.
+
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 [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.
  
===EBNF for the TextEditor's syntax ===
+
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.
  
parse_unit =
+
* [[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.
    comment?
 
    'machine' identifier_literal
 
    ('refines' identifier_literal (',' identifier_literal)*)?
 
    ('sees' identifier_literal (',' identifier_literal)*)?
 
    ('variables' identifier_list)?
 
    ('invariants' labeled_predicate_with_theorem+)?
 
    ('variant' variant)?
 
    ('events' event+)?
 
    end |
 
   
 
    comment?
 
    'context' identifier_literal
 
    ('extends' identifier_literal (',' identifier_literal)*)?
 
    ('sets' identifier_list)?
 
    ('constants' identifier_list)?
 
    ('axioms' labeled_predicate_with_theorem+)?
 
    end ;
 
 
variant = comment? expression ;
 
 
event =
 
    comment?
 
    convergence? 'event' identifier_literal
 
    event_refinement?
 
    ('any' identifier_list)?
 
    ('where' labeled_predicate+)?
 
    ('with' labeled_predicate+)?
 
    ('then' labeled_action+)? ;
 
 
convergence = 'ordinary' | 'convergent' | 'anticipated' ;
 
 
event_refinement =
 
    'refines' identifier_literal (',' identifier_literal)* |
 
    'extends' identifier_literal ;
 
 
labeled_action = comment? '@' identifier_literal action ;
 
 
labeled_predicate = comment? '@' identifier_literal predicate ;
 
 
labeled_predicate_with_theorem =
 
    comment? '@' identifier_literal predicate |
 
    comment? 'theorem' '@' identifier_literal predicate ;
 
 
identifier = comment? identifier_literal ;
 
 
identifier_list = identifier (',' identifier)* ;
 
 
comment =
 
    '//' string-to-next-linebreak |
 
    '/*' string '*/' ;
 
  
 +
* [[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.
  
===Explanation ===
+
==Lectures==
====Formulas ====
 
As you might notice the grammar only describes the structure of machines and contexts. For the terminals ''predicate'', ''expression'' and ''action'' you can use the syntax for formulas which you already know from editing models with the graphical Event-B editor. You can use the ASCII representation of mathematical symbols or their unicode. See the Rodin help for details about the mathematical symbols and their ASCII counterparts.
 
  
====Comments ====
+
* [[Media:iUML-BClassDiagramsLecture.pdf | iUML-B Class-diagrams Lecture]] : Lecture slides on the use of iUML-B Class-diagrams
Also note that the rather strict position for comments is necessary. In the RodinDB most elements can be commented. That means if you comment an element this comment is attached to the element. To reflect this in a text syntax we need to exactly specify to which textual element a comment belongs. Therefore we decided to always associate a comment to the previous element.
+
 
Additionally database only allows one comment per element. The grammar allows multiple comments, but to reflect the database restriction to one internally multiple comments are concatenated to one with linebreaks between the separate comments.
+
* [[Media:iUML-BStatemachinesLecture.pdf | iUML-B State-machines Lecture]] : Lecture slides on the use of iUML-B State-machines.
 +
 
 +
==Tutorials==
 +
 
 +
* [[iUML-B Class-diagrams Tutorial]] : A tutorial on the use of iUML-B Class-diagrams.
 +
 
 +
* [[iUML-B State-machines Tutorial]] : A tutorial on the use of iUML-B State-machines.
 +
 
 +
==Guidelines==
 +
 
 +
* [[iUML-B Modelling a control system]] : Some guidelines on modelling styles for a control system
 +
 
 +
 
 +
[[Category:User documentation]]
 +
[[Category:UML-B]]
 +
[[Category:Plugin]]

Revision as of 21:53, 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