CamilleX User Guide: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Son
No edit summary
Asieh (talk | contribs)
No edit summary
 
(19 intermediate revisions by 2 users not shown)
Line 1: Line 1:
The complete XEvent-B User Guide is available as pdf [https://sourceforge.net/projects/rodin-b-sharp/files/Plugin_XEventB/0.0.6/XEventBUserManual_v0.0.2.pdf/download here]. Some important information is listed below.
The latest CamilleX release (2.1.1) included in the Rodin Bundle 3.7.0 is available '''[https://github.com/eventB-Soton/Rodin-Bundles/releases here</font>]'''
 
More information about the installation can be found '''[https://github.com/eventB-Soton/Rodin-Bundles/wiki/Installation here</font>]'''
 
The CamilleX User Guide is available as pdf '''[https://sourceforge.net/projects/rodin-b-sharp/files/Plugin_CamilleX/1.0.0/CamilleXUserManual_v1.0.0.pdf/download<font> here</font>]'''.  
 


== Introduction ==
== 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.<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 of this editor,  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 CamilleX, 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 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.
* CamilleX is available as a separate feature from the main Rodin update site (under ''Modelling Extensions'' category)
* XEvent-B is available as a separate plug-in from the main Rodin update site (under ''Modelling Extensions'' category)


=== Release Notes ===
=== Release Notes ===
See [[XEvent-B_Release_Notes | XEvent-B Release Notes]]
See [[CamilleX_Release_Notes | CamilleX Release Notes]]


=== IMPORTANT ===
=== IMPORTANT ===
* Currently, XEvent-B supports "standard" Event-B machines and contexts and machine inclusion/event synchronisation mechanisms.
* 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 not be lost.
* 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.
* '''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''.
* 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 ===
=== KNOWN ISSUES ===
- Converting to XText: Currently, the "extended" attribute of events are not serialized.
* Machine Inclusion:  
- 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.
- Machine Inclusion: Including the same machine to both the abstract and its refining machine can result in the repetition of invariants.

Latest revision as of 12:31, 9 March 2023

The latest CamilleX release (2.1.1) included in the Rodin Bundle 3.7.0 is available here

More information about the installation can be found here

The CamilleX User Guide is available as pdf here.


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, 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.

KNOWN ISSUES

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