CamilleX User Guide

The complete XEvent-B 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 XEvent-B page.

Installation

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.
• XEvent-B is available as a separate plug-in from the main Rodin update site (under Modelling Extensions category)

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 not 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:
  • Currently a machine can be only included if it is in the same project.
  • Including the same machine to both the abstract and its refining machine can result in the repetition of invariants.