Event-B XText Front-end User Guide

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.

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
 ;

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.