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

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

Revision as of 18:46, 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

Converting Rodin files to Event-B XText