Difference between revisions of "CamilleX User Guide"

From Event-B
Jump to: navigation, search
m
m
Line 1: Line 1:
The latest XEvent-B User Guide is available as pdf '''[https://sourceforge.net/projects/rodin-b-sharp/files/Plugin_XEventB/0.0.7/XEventBUserManual_v0.0.3.pdf/<font color="red">download here</font>]'''. Some important information is listed below.
+
The latest XEvent-B User Guide is available as pdf '''[https://sourceforge.net/projects/rodin-b-sharp/files/Plugin_XEventB/0.0.7/XEventBUserManual_v0.0.3.pdf/download<font color="red"> here</font>]'''. Some important information is listed below.
  
 
== Introduction ==
 
== Introduction ==

Revision as of 14:34, 21 September 2017

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

Introduction

The XEvent-B 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 XEvent-B, see the XEvent-B page.

Installation

Setup

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

See XEvent-B 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.