Event-B XText Front-end User Guide: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Son
imported>Son
No edit summary
 
(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’