Difference between revisions of "CamilleX User Guide"
From Event-B
Jump to navigationJump to searchimported>Son |
imported>Son |
||
| (3 intermediate revisions by the same user not shown) | |||
| Line 3: | Line 3: | ||
== Introduction == | == Introduction == | ||
| − | The | + | The XEvent-B 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 | + | For more details about the principles on XEvent-B, see the [[XEvent-B|XEvent-B 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 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) | * XEvent-B is available as a separate plug-in from the main Rodin update site (under ''Modelling Extensions'' category) | ||
| + | === Configuration === | ||
| + | * By default, XContext files (extension .bucx) and XMa- chine 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 === | ||
| Line 23: | Line 24: | ||
=== KNOWN ISSUES === | === 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. | ||
Revision as of 20:12, 25 July 2017
The complete XEvent-B User Guide is available as pdf here. Some important information is listed below.
Contents
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
- 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)
Configuration
- By default, XContext files (extension .bucx) and XMa- chine 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
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.
