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

From Event-B
Jump to navigationJump to search
imported>Son
imported>Son
 
(6 intermediate revisions by the same user not shown)
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 ==
 
== 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.
 
* '''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 ===
 
−
 
 
−
== Converting Rodin files to Event-B XText ==
 

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

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.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Event-B_XText_Front-end_User_Guide&oldid=4329’