CamilleX User Guide

From Event-B
Revision as of 14:24, 13 November 2018 by imported>Son
Jump to navigationJump to search

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


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.



Release Notes

See CamilleX Release Notes


  • Currently, CamilleX not only supports "standard" Event-B machines and contexts, but also 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 CamilleX 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.


  • Machine Inclusion:
    • Including the same machine to both the abstract and its refining machine can result in the repetition of invariants.