imported>Son |
imported>Son |
Line 1: |
Line 1: |
| + | 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 21: |
Line 23: |
| === KNOWN ISSUES === | | === KNOWN ISSUES === |
| - Converting to XText: Currently, the "extended" attribute of events are not serialised. | | - Converting to XText: Currently, the "extended" attribute of events are not serialised. |
− |
| |
− | == 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 (v0.0.3) 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.
| |