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

From Event-B
Jump to: navigation, search
m (XContext)
Line 1: Line 1:
 +
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 ==
 
== Introduction ==
  
Line 21: Line 23:
 
=== KNOWN ISSUES ===
 
=== KNOWN ISSUES ===
 
- Converting to XText: Currently, the "extended" attribute of events are not serialised.
 
- Converting to XText: Currently, the "extended" attribute of events are not serialised.
 
== Configuration ==
 
 
=== 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 (v0.0.3) 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
 
  ;
 
 
=== Type Setting Event-B Symbols ===
 
The Event-B Symbols are supported via Content assist, e.g., when type setting invariant or action. Sometime, a preceding blank space is required to enable the correct content assist.
 
 
== 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.
 

Revision as of 20:16, 28 January 2017

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

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.