Difference between revisions of "Event-B XText Front-end User Guide"

Latest revision as of 23:27, 21 July 2017

IMPORTANT: Event-B XText Front-end is now developed into extended Event-B (XEvent-B).

The complete Event-B XText Front-end User Guide is available as pdf here. Some important information is listed below.

Introduction

The Event-B XText front-end provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.
For more details about the principles of this editor, see the Event-B XText Front-end page.

Installation

Setup

Before install the Event-B XText front-end, you need to add the XText update site (http://download.eclipse.org/modeling/tmf/xtext/updates/composite/releases/) as an additional software site.
The Event-B XText front-end is available as a separate plug-in from the main Rodin update site (under 'Editors' category)

Release Notes

See Event-B XText Front-end Release Notes

IMPORTANT

Currently, Event-B XText front-end ONLY supports "standard" Event-B machines and contexts.
Since the XContexts and XMachines are compiled to the Rodin files, the corresponding Rodin contexts and machines will be OVER-WRITTEN. Any changes in the Rodin files will not be lost.
DO NOT USE the Event-B XText Front-end if you use modelling plug-ins such as iUML-B state-machines and class-diagrams, as the additional modelling elements will be over-written.

KNOWN ISSUES

- Converting to XText: Currently, the "extended" attribute of events are not serialised.

@@ Line 1: / Line 1: @@
+'''IMPORTANT''': Event-B XText Front-end is now developed into [[XEvent-B| ''extended Event-B (XEvent-B)'']].
+The complete Event-B XText Front-end User Guide is available as pdf [https://sourceforge.net/projects/rodin-b-sharp/files/Plugin_EventBXText/0.0.5/EventBXTextUserManual_v0.0.1.pdf/download here]. Some important information is listed below.
 == Introduction ==
@@ Line 19: / Line 23: @@
 * '''DO NOT USE''' the Event-B XText Front-end if you use modelling plug-ins such as iUML-B state-machines and class-diagrams, as the additional modelling elements will be over-written.
-== Configuration ==
+=== KNOWN ISSUES ===
+- Converting to XText: Currently, the "extended" attribute of events are not serialised.
-=== Event-B Explorer ===
-By default, XContext files (extension ''bucx'') and XMachine files (extension ''bumx'') are not display in the ''Event-B Explorer''. To enable this, select ''Customize view'' for ''Event-B Explorer'' and uncheck the option ''All files and folders''.
-== Editing ==
-=== XContext ===
-* Any file with extension ''*.bucx'' will be recognised as XContext file. As a result, XContext file can be created by the standard ''New File'' wizard of Eclipse.
-* The XText syntax of XContext file is as follows.
-  XContext returns econtext::Context:
-    {econtext::Context}
-    (comment=(ML_COMMENT | SL_COMMENT))?
-    'context' name=ID
-    ('extends' extends+=[econtext::Context]+)?
-    ('sets' sets+=XCarrierSet+)?
-    ('constants' constants+=XConstant+)?
-    ('axioms' axioms+=XAxiom+)?
-    'end'
-  ;
-  XCarrierSet returns econtext::CarrierSet:
-    {econtext::CarrierSet}
-    (comment=(ML_COMMENT | SL_COMMENT))?
-    name=ID
-  ;
-  XConstant returns econtext::Constant:
-    {econtext::Constant}
-    (comment=(ML_COMMENT | SL_COMMENT))?
-    name=ID
-  ;
-  XAxiom returns econtext::Axiom:
-    {econtext::Axiom}
-    (comment=(ML_COMMENT | SL_COMMENT))?
-    name=XLABEL predicate=STRING (theorem?='theorem')?
-  ;
-  terminal XLABEL returns ecore::EString:
-    '@' !(':')+ ':'
-  ;
-=== XMachine ===
-* Any file with extension ''*.bumx'' will be recognised as XMachine file. As a result, XMachine file can be created by the standard ''New File'' wizard of Eclipse.
-* The XText syntax of XMachine file is as follows.
-  XMachine returns emachine::Machine:
-    {emachine::Machine}
-    (comment=(ML_COMMENT|SL_COMMENT))?
-    'machine' name=ID
-    ('refines' refines+=[emachine::Machine])?
-    ('sees' sees+=[econtext::Context]+)?
-    ('variables' variables+=XVariable+)?
-    ('invariants' invariants+=XInvariant+)?
-    ('variant' variant=XVariant)?
-    ('events' events+=XEvent (';' events+=XEvent)*)?
-    ('end')
-  ;
-  XVariable returns emachine::Variable:
-    {emachine::Variable}
-    (comment=(ML_COMMENT|SL_COMMENT))?
-    name=ID
-  ;
-  XInvariant returns emachine::Invariant:
-    {emachine::Invariant}
-    (comment=(ML_COMMENT|SL_COMMENT))?
-    name=XLABEL predicate=STRING (theorem?='theorem')?
-  ;
-  terminal XLABEL returns ecore::EString:
-    '@' !(':')+ ':'
-  ;
-  XVariant returns emachine::Variant:
-    {emachine::Variant}
-    (comment=(ML_COMMENT|SL_COMMENT))?
-    expression=STRING
-  ;
-  XEvent returns emachine::Event:
-    {emachine::Event}
-    (comment=(ML_COMMENT|SL_COMMENT))?
-    name=ID
-    (
-      (extended?='extended')? &
-      (convergence=XConvergence)?
-    )
-    ('refines' refines+=[emachine::Event]+)?
-    (
-      ('with' witnesses+=XWitness+)?
-      'begin'
-        actions+=XAction+
-      'end'
-    |
-      'when'
-        guards+=XGuard+
-      ('with' witnesses+=XWitness+)?
-      ('then'
-        actions+=XAction+)?
-      'end'
-    |
-      'any'
-         parameters+=XParameter+
-      'where'
-        guards+=XGuard+
-      ('with' witnesses+=XWitness+)?
-      ('then'
-        actions+=XAction+)?
-      'end'
-    )?
-  ;
-  enum XConvergence returns emachine::Convergence:
-    ordinary = 'ordinary' | convergent = 'convergent' | anticipated = 'anticipated';
-  XParameter returns emachine::Parameter:
-    {emachine::Parameter}
-    (comment=(ML_COMMENT|SL_COMMENT))?
-    name=ID
-  ;
-  XGuard returns emachine::Guard:
-    {emachine::Guard}
-    (comment=(ML_COMMENT|SL_COMMENT))?
-    name=XLABEL predicate=STRING (theorem?='theorem')?
-  ;
-  XWitness returns emachine::Witness:
-    {emachine::Witness}
-    (comment=(ML_COMMENT|SL_COMMENT))?
-    name=XLABEL predicate=STRING
-  ;
-  XAction returns emachine::Action:
-    {emachine::Action}
-    (comment=(ML_COMMENT|SL_COMMENT))?
-    name=XLABEL action=STRING
-  ;
-== Converting Rodin files to Event-B XText ==
-Rodin contexts and machines can be converted to XContext and XMachine files using context menu. From the ''Event-B Explorer'', right click on a Rodin project, a Rodin context, or a Rodin machine will offer option ''Convert to XText''. When a Rodin project is selected, all Rodin contexts and machines within that project will be converted.

Difference between revisions of "Event-B XText Front-end User Guide"

Latest revision as of 23:27, 21 July 2017

Contents

Introduction

Installation

Setup

Release Notes

IMPORTANT

KNOWN ISSUES

Navigation menu

Page actions

Page actions

Personal tools

Navigation

contribute

Search

Tools