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

From Event-B
Jump to: navigation, search
m (XContext)
m (XMachine)
Line 64: Line 64:
  
 
=== XMachine ===
 
=== 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 ==
 
== Converting Rodin files to Event-B XText ==

Revision as of 18:54, 4 November 2016

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.

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 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