Difference between pages "Atomicity Decomposition Plug-in User Guide" and "Camille Editor"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Asiehsalehi
 
imported>Fabian
 
Line 1: Line 1:
−
== Introduction ==
+
{| align="right"
−
The Atomicity Decomposition (AD) plug-in allows an explicit representation of control flow and explicit representation of refinement relationships between an abstract event and the corresponding concrete events.  
+
| __TOC__
 +
|}
 +
The first version of the Text Editor will be released in a few weeks, that means in second half of June and not before the Rodin release 1.0 has been published.
 +
 
 +
Until then we are going to release a few testing releases (beta) for interested users. You will find instructions how to install and use these beta releases on this page.
 +
 
  
−
See the [http://wiki.event-b.org/index.php/Atomicity_Decomposition Atomicity Decomposition] page for technical details.
+
{| style="width:auto; background-color:#FFFF00; border:2px solid red;  padding:3px;"
 +
|<b title="Usage warning"><font size="3"> Warning:</font size="3"></b><font size="1">
 +
Don't use the TextEditor yet with your production models!
 +
* The TextEditor is still in development
 +
* It is based on latest SVN Rodin version which uses a changed database model. Therefore its projects cannot be used in older Rodin versions.
  
−
Currently the AD diagrams can be defined in an EMF tree structure included in an Event-B machine which is opened by Rose editor. After defining the control flow and refinement relationships via AD diagrams, the AD diagrams can automatically transformed to the Event-B notation.
+
|}
  
−
== Installing and Requirements ==
 
  
−
=== Setup ===
+
==Installing ==
−
The following steps will guide you through the setup process:
+
The TextEditor relies on features of the Rodin release 1.0 which is not yet released. Therefore you will have to create a new Rodin installation. The following steps will guide you through this process:
−
# Start Rodin.
+
 
−
# In the menu choose ''Help'' -> ''Install New Software...''.
+
# Download a build of Rodin from our [http://cruise.cs.uni-duesseldorf.de/dashboard/tab/builds CruiseControl server]:
−
# In the ''Work with'' dropdown list, choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates].
+
## Point your browser to http://cruise.cs.uni-duesseldorf.de/dashboard/tab/build/detail/org.rodinp.platform
−
# Select the ''Event-B Atomicity Decomposition'' feature under the ''Modelling Extensions'' category, then click the check box.
+
## Download a zip file with a name starting with ''rodin-product'' and matching your platform. For example ''rodin-product-linux.gtk.x86.zip'' if you are working on a Linux system.
−
# Click ''Next'', after some time, the ''Install Details'' page appears.
+
# Extract the downloaded zip file.
−
# Click ''Next'' and accept the license.
+
# Start Rodin from the folder where you extracted the zip file in the previous step.
−
# Click ''Finish''.
+
# Install the TextEditor:
−
# A ''Security Warning'' window may appear: click ''OK''.
+
## In the menu choose ''Help'' -> ''Software Updates...''
 +
## Select the tab ''Available Software'' and click ''Add Site...''
 +
## Use the location URL: <tt>http://www.stups.uni-duesseldorf.de/update-beta/</tt>
 +
## Back in ''Available Software'' open the update site you just added
 +
## Select ''Event-B EMF Framework'' and ''Event-B TextEditor'' and click ''Install...''
 
# Restart Rodin as suggested.
 
# Restart Rodin as suggested.
  
−
=== Requirements ===
 
−
* The AD plug-in relies on the Epsilon tool suite. Install Epsilon useing the Epsilon interim update site available at:
 
  
−
  [http://download.eclipse.org/modeling/gmt/epsilon/interim/]
+
Now you are ready to use the TextEditor.
  
−
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for AD plug-in.
 
  
−
* To create the AD diagrams you need to install [http://wiki.event-b.org/index.php/Rose_(Structured)_Editor Rose Editor]. To install Rose Editor:
+
==Updating ==
 +
As often as possible we are going to publish updated beta releases. We recommend that you update your new Rodin installation with these updates for the TextEditor (and EMF Framework).
  
−
# In the menu choose ''Help'' -> ''Install New Software...''.
+
Although we will try to announce these updates on this site too, it is a lot easier if you setup Rodin to let you know when an update is available. The following steps guide you through this process:
−
# In the ''Work with'' dropdown list, choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates].
+
 
−
# Select the ''Rose Event-B Editor'' feature under the ''Editors'' category, then click the check box.
+
# In Rodin open the preferences (''Window'' -> ''Preferences'' or for Mac: ''Rodin'' -> ''Preferences'')
−
# Click ''Next'', after some time, the ''Install Details'' page appears.
+
# Find ''Install/Update'' -> ''Automatic Updates''
−
# Click ''Next'' and accept the license.
+
# Select ''Automatically find new updates and notify me''
−
# Click ''Finish''.
+
 
−
# A ''Security Warning'' window may appear: click ''OK''.
+
As soon as Rodin finds a new update it will ask you if you would like to install it.
−
# Restart Rodin as suggested.
+
 
 +
 
 +
==Usage ==
 +
This section should help you to get started with the TextEditor.
 +
 
 +
====Opening with the TextEditor ====
 +
At the moment the TextEditor competes with the current graphical Event-B editor when it comes to the selection of a default editor for the double click action to open a model file.
 +
 
 +
Thus from time to time you might experience that an unexpected editor opens. If this happens you can right-click on the model file and select ''Open with TextEditor'' to use the text editor. Usually you should be able to just use a double-click to open a machine or context with the TextEditor.
  
−
== Creating Flow Diagrams ==
+
====Syntax ====
 +
The text syntax for machines and contexts is closely related with the pretty-print you might know from the graphical Event-B editor. See the grammar's [[TextEditor_EBNF|EBNF]] for details.
  
−
First you need to open the machine in the Rose editor by right-clicking on the machine.  
+
As you might notice in the grammar it only describes the structure of machines and contexts. For the terminals ''predicate'', ''expression'' and ''action'' you can use the syntax for formulas which you already know from editing models with the graphical Event-B editor. You can use the ASCII representation of mathematical symbols or their unicode. See the Rodin help for details about the mathematical symbols and their ASCII counterparts.
  
−
[[Image:machine_rose.jpg]]
+
====Editing ====
 +
The TextEditor currently offers the following features:
 +
* ''Syntax error marking'': Syntactical errors are highlighted in the input text.
  
−
Then a flow can be created:
+
* ''Mathmatical language'': You can type formulas in ASCII syntax and the TextEditor will replace ASCII symbols with their unicode counterparts as soon as you stop typing for a short while.
−
{|
 
−
|-
 
−
|1. Either for an Event-B machine, when right-clicking on the machine.
 
−
|2. Or for a pre-defined leaf, when right-clicking on the leaf.
 
−
|-
 
−
| valign="top" | [[Image:flow_machine.jpg|center]]
 
−
| valign="top" | [[Image:flow_leaf.jpg|center]]
 
−
|}
 
  
−
The following steps will guide you through a combined atomicity decomposition diagram:
+
* ''Syntax highlighting'': Keywords (structural and in formulas), labels and comments are highlighted. This happends directly when typing
−
* Create a flow for the most abstract machine.
 
−
* When refining a machine, the pre-defined flows are copied to the new (refining) machine.
 
−
* In the new machine, you can create a new flow for each pre-defined leaf.
 
  
−
== Elements and Properties ==
+
* ''Semantic highlighting'': Identifiers are highlighted based on their semantic meaning, i.e., as variables, constants, parameters, sets, local variables. This highlighting is updated when you stop typing for a short while.
  
−
For each flow, you can define one or more of the below elements, when right-clicking on the flow:
+
* ''Code completion'': The following elements are available for code completion (invoked by Ctrl+Space on the most computers)
−
* typed parameter
+
** ''Keywords''
−
* leaf
+
** ''Identifiers''
−
* ''loop'' constructor including one leaf (right-click on the ''loop'')
+
** ''Templates'' (very few so far, please let us know which templates you would like to add)
−
* ''and'' constructor including two or more leaves (right-click on the ''and'')
 
−
* ''or'' constructor including two or more leaves (right-click on the ''or'')
 
−
* ''xor'' constructor including two or more leaves (right-click on the ''xor'')
 
−
* ''all'' constructor including one leaf and one parameter (right-click on the ''all'')
 
−
* ''some'' constructor including one leaf and one parameter (right-click on the ''some'')
 
−
* ''one'' constructor including one leaf and one parameter (right-click on the ''one'')
 
  
−
[[Image:flow_children.jpg]]
+
* ''Outline View'': An outline view gives you an overview of the model's structure.
  
−
=== Flow Properties ===
+
* ''Quick Navigation'': The outline view allows clicking on an element to jump to its position within the text.
−
* Name: a string containing the name of the root event.
 
−
* Sw: a boolean indicates strong (''true'') / weak (''false'') sequencing.
 
  
−
=== Leaf Properties ===
 
−
* Name: a string containing the name of the event.
 
−
* Ref: a boolean indicates refining (''true'') / non-refining (''false'') event.
 
  
−
[[Image:leaf_properties.jpg]]
+
Of course the TextEditor offers the common features you know from other text editors, such as: copy, paste, moving of text (try Alt+Up or Alt+Down), undo, redo, ...
  
−
=== Constructor Properties ===
+
====Restrictions ====
−
* Ref: a boolean indicates refining (''true'') / non-refining (''false'') constructor (''loop'', ''and'' / ''or'' / ''xor'' / ''all'' / ''some'' / ''one'').
+
Due to some design decisions and its combination with the Rodin platform the TextEditor comes with a few restrictions:
−
NOTE: The refining property for (''loop'' / ''and'' / ''or'' / ''all'' / ''some'') constructors has to be ''false''.
+
* Semantic analysis (for highlighting and code completion for example) can only performed if the overall structure of the input is parsable. Therefore you might experience situtions when the semantic highlighting or the code completion produces unexpected results because it is based on outdated parsing information.
  
−
=== Parameter Properties ===
+
* Parsing for formulas, i.e., predicates, actions and expressions can only be performed if the overall structure of the input is parsable. If the structure is not parsable ascii symbols will not be replaced until you correct the overall structure.
−
* Name: a string containing the name of the parameter.
 
−
* Type: a string containing the type of the parameter.
 
−
NOTE: the parameter type has to be defined in the context.
 
  
−
== Transforming to Event-B ==
+
* Also see the [[TextEditor_EBNF|EBNF page]] for some restrictions in the syntax.
  
−
For each machine, after completing the flow construction process, you can perform the translation rules to transform the defined AD flow to the Event-B notation (For technical details see [http://wiki.event-b.org/index.php/Atomicity_Decomposition Atomicity Decomposition] page). This is done by right-clicking on the machine and launch ''Atomicity Decomposition Transformation -> Transform to Event-B''.
 
  
−
As a result, some read-only event-B elements are generated in order to manage the defined control flow and refinement relationships. User defined event-B elements are allowed; but you can not alter the generated read-only elements.
+
==Bugs and Features ==
 +
Please use this section to report any bugs you find and let us know about features you would like to see in the TextEditor.
  
−
== Validation Rules to Follow ==
+
Regarding feature requests: Any feature request is welcome! But please keep in mind that we are preparing for a first stable release of the TextEditor. So we might not start working on your feature request in the next weeks. ''The focus until the first release is on stability!''
  
−
In order to perform the translation rules correctly, you will need to follow these rules:
 
−
(For more information about technical reasons see [http://wiki.event-b.org/index.php/Atomicity_Decomposition Atomicity Decomposition] page)
 
  
−
* Rules on the flow:
+
====Bugs ====
−
** Never change the ''copy'' property of a flow. This is an internal property use to make the internal programming decision.
+
* ''please add it when you fine one''
−
** A most abstract flow is a flow with (''sw'' = ''true'') and its children are all non-refining (''ref'' = ''false'').
 
−
** For each non-abstract flow, EXACTLY one refining child (''ref'' = ''true'') has to be defined.
 
−
** Each flow inherits its parameter from its parent flow and parent (''all'' / ''some'' / ''one'') constructor (if exists). This has to be done manually. For each new defined flow, copy and paste all necessary parameters from pre-defined parent flow / constructor.
 
−
** For technical reasons, a ''loop'' constructor never can placed as the first or last child of a flow.
 
  
−
*Rules on the parameter:
+
====Feature Requests ====
−
** The parameter type has to be defined in the context.
+
* Make TextEditor an [http://en.wikipedia.org/wiki/Eierlegende_Wollmilchsau Eierlegende Wollmilchsau]... ;-)
−
** The parameter name has to be unique.
 
  
−
* Rules on the constructors:
+
====Comments ====
−
** The refining property for (''loop'' / ''and'' / ''or'' / ''all'' / ''some'') constructors has to be ''false''.
+
Of course any other feedback is welcome too! We appreciate when you let us now what you think about the TextEditor.
−
** A constructor leaf inherits its refining property from its parent constructor. For example, for a refining ''xor'' (''ref'' = ''true''), all of its leaves' refining property has to be ''true''. Therefore the (''loop'' / ''and'' / ''or'' / ''all'' / ''some'') children refining property is always ''false''.
 

Revision as of 13:59, 27 May 2009

The first version of the Text Editor will be released in a few weeks, that means in second half of June and not before the Rodin release 1.0 has been published.

Until then we are going to release a few testing releases (beta) for interested users. You will find instructions how to install and use these beta releases on this page.


Warning:

Don't use the TextEditor yet with your production models!

  • The TextEditor is still in development
  • It is based on latest SVN Rodin version which uses a changed database model. Therefore its projects cannot be used in older Rodin versions.


Installing

The TextEditor relies on features of the Rodin release 1.0 which is not yet released. Therefore you will have to create a new Rodin installation. The following steps will guide you through this process:

  1. Download a build of Rodin from our CruiseControl server:
    1. Point your browser to http://cruise.cs.uni-duesseldorf.de/dashboard/tab/build/detail/org.rodinp.platform
    2. Download a zip file with a name starting with rodin-product and matching your platform. For example rodin-product-linux.gtk.x86.zip if you are working on a Linux system.
  2. Extract the downloaded zip file.
  3. Start Rodin from the folder where you extracted the zip file in the previous step.
  4. Install the TextEditor:
    1. In the menu choose Help -> Software Updates...
    2. Select the tab Available Software and click Add Site...
    3. Use the location URL: http://www.stups.uni-duesseldorf.de/update-beta/
    4. Back in Available Software open the update site you just added
    5. Select Event-B EMF Framework and Event-B TextEditor and click Install...
  5. Restart Rodin as suggested.


Now you are ready to use the TextEditor.


Updating

As often as possible we are going to publish updated beta releases. We recommend that you update your new Rodin installation with these updates for the TextEditor (and EMF Framework).

Although we will try to announce these updates on this site too, it is a lot easier if you setup Rodin to let you know when an update is available. The following steps guide you through this process:

  1. In Rodin open the preferences (Window -> Preferences or for Mac: Rodin -> Preferences)
  2. Find Install/Update -> Automatic Updates
  3. Select Automatically find new updates and notify me

As soon as Rodin finds a new update it will ask you if you would like to install it.


Usage

This section should help you to get started with the TextEditor.

Opening with the TextEditor

At the moment the TextEditor competes with the current graphical Event-B editor when it comes to the selection of a default editor for the double click action to open a model file.

Thus from time to time you might experience that an unexpected editor opens. If this happens you can right-click on the model file and select Open with TextEditor to use the text editor. Usually you should be able to just use a double-click to open a machine or context with the TextEditor.

Syntax

The text syntax for machines and contexts is closely related with the pretty-print you might know from the graphical Event-B editor. See the grammar's EBNF for details.

As you might notice in the grammar it only describes the structure of machines and contexts. For the terminals predicate, expression and action you can use the syntax for formulas which you already know from editing models with the graphical Event-B editor. You can use the ASCII representation of mathematical symbols or their unicode. See the Rodin help for details about the mathematical symbols and their ASCII counterparts.

Editing

The TextEditor currently offers the following features:

  • Syntax error marking: Syntactical errors are highlighted in the input text.
  • Mathmatical language: You can type formulas in ASCII syntax and the TextEditor will replace ASCII symbols with their unicode counterparts as soon as you stop typing for a short while.
  • Syntax highlighting: Keywords (structural and in formulas), labels and comments are highlighted. This happends directly when typing
  • Semantic highlighting: Identifiers are highlighted based on their semantic meaning, i.e., as variables, constants, parameters, sets, local variables. This highlighting is updated when you stop typing for a short while.
  • Code completion: The following elements are available for code completion (invoked by Ctrl+Space on the most computers)
    • Keywords
    • Identifiers
    • Templates (very few so far, please let us know which templates you would like to add)
  • Outline View: An outline view gives you an overview of the model's structure.
  • Quick Navigation: The outline view allows clicking on an element to jump to its position within the text.


Of course the TextEditor offers the common features you know from other text editors, such as: copy, paste, moving of text (try Alt+Up or Alt+Down), undo, redo, ...

Restrictions

Due to some design decisions and its combination with the Rodin platform the TextEditor comes with a few restrictions:

  • Semantic analysis (for highlighting and code completion for example) can only performed if the overall structure of the input is parsable. Therefore you might experience situtions when the semantic highlighting or the code completion produces unexpected results because it is based on outdated parsing information.
  • Parsing for formulas, i.e., predicates, actions and expressions can only be performed if the overall structure of the input is parsable. If the structure is not parsable ascii symbols will not be replaced until you correct the overall structure.
  • Also see the EBNF page for some restrictions in the syntax.


Bugs and Features

Please use this section to report any bugs you find and let us know about features you would like to see in the TextEditor.

Regarding feature requests: Any feature request is welcome! But please keep in mind that we are preparing for a first stable release of the TextEditor. So we might not start working on your feature request in the next weeks. The focus until the first release is on stability!


Bugs

  • please add it when you fine one

Feature Requests

Comments

Of course any other feedback is welcome too! We appreciate when you let us now what you think about the TextEditor.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Atomicity_Decomposition_Plug-in_User_Guide&oldid=1091’