Difference between revisions of "CamilleX User Guide"

From Event-B
Jump to: navigation, search
m
m
Line 3: Line 3:
 
== Introduction ==
 
== Introduction ==
  
The XEvent-B provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.<br>
+
The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.<br>
For more details about the principles on XEvent-B,  see the [[XEvent-B|XEvent-B page]].<br>
+
For more details about the principles on CamilleX,  see the [[CamilleX|CamilleX page]].<br>
  
 
== Installation ==
 
== Installation ==
  
 
=== Setup ===
 
=== Setup ===
* Before install XEvent-B, you need to add the XText update site (http://download.eclipse.org/modeling/tmf/xtext/updates/composite/releases/) as an additional software site.
+
* Before install CamilleX, you need to add the XText update site (http://download.eclipse.org/modeling/tmf/xtext/updates/composite/releases/) as an additional software site.
* XEvent-B is available as a separate plug-in from the main Rodin update site (under ''Modelling Extensions'' category)
+
* CamilleX is available as a separate feature from the main Rodin update site (under ''Modelling Extensions'' category)
=== Configuration ===
 
* By default, XContext files (extension .bucx) and XMachine files (extension .bumx) are not displayed in the ''Event-B Explorer''. To enable this, select ''Customize view'' for Event-B Explorer and uncheck the option ''All files and folders''.
 
  
 
=== Release Notes ===
 
=== Release Notes ===
See [[XEvent-B_Release_Notes | XEvent-B Release Notes]]
+
See [[CamilleX_Release_Notes | CamilleX Release Notes]]
  
 
=== IMPORTANT ===
 
=== IMPORTANT ===

Revision as of 14:23, 13 November 2018

The latest XEvent-B User Guide is available as pdf here. Some important information is listed below.

Introduction

The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.
For more details about the principles on CamilleX, see the CamilleX page.

Installation

Setup

Release Notes

See CamilleX Release Notes

IMPORTANT

  • Currently, XEvent-B supports "standard" Event-B machines and contexts and machine inclusion/event synchronisation mechanisms.
  • 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 be lost.
  • DO NOT USE XEvent-B if you use modelling extensions such as iUML-B state-machines and class-diagrams, as the additional modelling elements will be over-written.
  • Windows users must change the workspace text file encoding to UTF-8. This can be updated under the Rodin Preferences: General/Workspace then in the Text file encoding section, select Other: UTF-8.

KNOWN ISSUES

  • Converting to XText: Currently, the "extended" attribute of events are not serialized.
  • Machine Inclusion:
    • Including the same machine to both the abstract and its refining machine can result in the repetition of invariants.