Difference between pages "Camille Editor" and "Code Generation Activity"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Fabian
 
imported>Andy
 
Line 1: Line 1:
−
{| align="right"
+
Tasking Event-B is the extension of Event-B for defining concurrent systems sharing data, for details see the [[Tasking Event-B Overview]] page. For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk
−
| __TOC__
+
=== Sensing and Actuating for Tasking Event-B ===
−
|}
+
Version 0.1.5. Sensing and actuating events, and an Environ Machine have been added to allow simulation of the environment and implementation using memory mapped IO.
−
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.
+
Available from the Rodin Update Site in the Utilities Category.
  
 +
As in previous releases, the code generation plug-in relies on the Epsilon tool suite. Add the following Epsilon interim update site to the list of available update sites in the Eclipse menu ''help/install new software'': http://download.eclipse.org/modeling/gmt/epsilon/interim/
  
−
{| style="width:auto; background-color:#FFFF00; border:2px solid red;  padding:3px;"
+
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
−
|<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.
 
  
−
|}
+
A new case study has been produced that makes use of these new features, details available at http://wiki.event-b.org/index.php/Event-B_Examples
  
 +
The example/tutorial projects, and also and a Bundled Windows version, are available in the [http://deploy-eprints.ecs.soton.ac.uk/304/ Deploy E-Prints archive].
  
−
==Installing ==
+
The projects are also available from the [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/HeatingController_Tutorial_v0.1.4/ Examples SVN site].
−
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:
 
  
−
# Download a build of Rodin from our [http://cruise.cs.uni-duesseldorf.de/dashboard/tab/builds CruiseControl server]:
+
Sources for Tasking Event-B and Code Generators are available from a branch on the [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration Rodin SVN site].
−
## Point your browser to http://cruise.cs.uni-duesseldorf.de/dashboard/tab/build/detail/org.rodinp.platform
 
−
## 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.
 
−
# Extract the downloaded zip file.
 
−
# Start Rodin from the folder where you extracted the zip file in the previous step.
 
−
# Install the TextEditor:
 
−
## 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.
 
  
 +
=== The Code Generation Demonstrator for Rodin 2.1.x ===
  
−
Now you are ready to use the TextEditor.
+
Released 24 January 2011.
  
 +
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
  
−
==Updating ==
+
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
−
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:
+
The update-site is available through the Rodin update site in the ''Utilities'' category.
  
−
# In Rodin open the preferences (''Window'' -> ''Preferences'' or for Mac: ''Rodin'' -> ''Preferences'')
+
The code generation tutorial examples are available for download at:
−
# Find ''Install/Update'' -> ''Automatic Updates''
 
−
# 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.
+
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
  
 +
The code generation plug-in relies on the Epsilon tool suite. Install Epsilon manually, since the automatic install utility does not seem to work for this feature. We currently use the Epsilon interim update site available at:
  
−
==Usage ==
+
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
−
This section should help you to get started with the TextEditor.
 
  
−
====Opening with the TextEditor ====
+
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
−
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.
+
== Code Generation Status ==
 +
=== Latest Developments ===
 +
* Demonstrator plug-in feature version 0.1.0
 +
** for Rodin 2.1.x version is available.
  
−
====Syntax ====
+
* The Code Generation feature consists of,
−
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.
+
** a tasking Development Generator.
 +
** a tasking Development Editor (Based on an EMF Tree Editor).
 +
** a translator, from Tasking Development to Common Language Model (IL1).
 +
** a translator, from the Tasking Development to Event-B model of the implementation.
 +
** a pretty-printer for the Tasking Development.
 +
** a pretty-printer for Common Language Model, which generates Ada Source Code.
  
−
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.
+
* A tutorial is available [[Code Generation Tutorial]]
 +
** Step 1 - Create the tasking development.
 +
** Step 2 - Add annotations.
 +
** Step 3 - Invoke translators.
  
−
====Editing ====
+
=== Ongoing Work ===
−
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.
+
* Full Rodin Integration
 +
* Sensed Variables
 +
* Branching in Shared Machines
  
−
* ''Syntax highlighting'': Keywords (structural and in formulas), labels and comments are highlighted. This happends directly when typing
+
=== Future Work ===
 +
* Support for Interrupts.
 +
* Richer DataTypes.
 +
* Accommodation of duplicate event names in tasking developments.
  
−
* ''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.
+
== Metamodels ==
 +
* In the plug-in we define several meta-models:
 +
** CompositeControl: for the control flow (algorithmic) constructs such as branch, loop and sequence etc. These constructs may be used in the specification of either  sequential or concurrent systems.
 +
** Tasking Meta-model: defines the tasking model where we attach tasking specific details, such as task priority, task type. The tasking structures provide the ability to define single tasking or multi-tasking (concurrent) systems. We make use of the composite control plug-in to specify the flow of control.  
 +
** Common Language (IL1) Meta-model: defines an abstraction of common programming language constructs for use in translations to implementations.
  
−
* ''Code completion'': The following elements are available for code completion (invoked by Ctrl+Space on the most computers)
+
== Translation Rules ==
−
** ''Keywords''
+
* Tasking to IL1/Event-B translation rules [[http://wiki.event-b.org/images/Translation.pdf]]
−
** ''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.
+
== Release History ==
 +
=== The Code Generation Demonstrator for Rodin 1.3.x ===
  
−
* ''Quick Navigation'': The outline view allows clicking on an element to jump to its position within the text.
 
  
 +
First release: 30 November 2010.
  
−
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, ...
+
available from:
  
−
====Restrictions ====
+
https://sourceforge.net/projects/codegenerationd/files/
−
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.
+
The zip file contains a windows XP bundle, and a Windows V7 bundle. Alternatively, if you wish to build using an update-site, this is also included in the zip file, along with some notes on installation. However, note that the demonstrator tool is only compatible with Rodin 1.3.  
  
−
* Also see the [[TextEditor_EBNF|EBNF page]] for some restrictions in the syntax.
+
A simple shared buffer example is provided. This will form the basis of a tutorial (which is work in progress). The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code Generation plug-ins, together with a patch plug-in. The patch plug-in is required to correct an inconsistency in the org.eventb.emf.persistence plug-in. For the bundles, simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed - the only configuration necessary may be to switch workspace to ''<installPath>\rodin1.3bWin7\workspace''. When using the update-site the example projects, and the project forming the basis of a simple tutorial, are provided in the accompanying zip file. These should be imported manually.
  
−
==Bugs and Features ==
+
Mac users - no bundled version available at present, but use the update site in the 'advanced' folder.  
−
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!''
+
'''A step-by-step [[Code Generation Tutorial]] is available'''  
  
 +
==== About the Initial Release ====
 +
The Code Generation (CG) Feature in the initial release is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, therefore, there will be a heavy reliance on docs and dialogue to facilitate exploration of the tools and concepts.
  
−
====Bugs ====
+
==== Source Code ====
−
* ''please add it when you fine one''
 
  
−
====Feature Requests ====
+
The sources are available from,
−
* Make TextEditor an [http://en.wikipedia.org/wiki/Eierlegende_Wollmilchsau Eierlegende Wollmilchsau]... ;-)
 
  
−
====Comments ====
+
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
−
Of course any other feedback is welcome too! We appreciate when you let us now what you think about the TextEditor.
+
 
 +
Note - I used Eclipse 3.5 Galileo, and you will need to install (or have sources from) Epsilon's interim update site. There is also dependency on Camille v2.0.0
 +
 
 +
 
 +
 
 +
[[Category:Work in progress]]

Revision as of 11:07, 17 May 2011

Tasking Event-B is the extension of Event-B for defining concurrent systems sharing data, for details see the Tasking Event-B Overview page. For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk

Sensing and Actuating for Tasking Event-B

Version 0.1.5. Sensing and actuating events, and an Environ Machine have been added to allow simulation of the environment and implementation using memory mapped IO.

Available from the Rodin Update Site in the Utilities Category.

As in previous releases, the code generation plug-in relies on the Epsilon tool suite. Add the following Epsilon interim update site to the list of available update sites in the Eclipse menu help/install new software: http://download.eclipse.org/modeling/gmt/epsilon/interim/

Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.

A new case study has been produced that makes use of these new features, details available at http://wiki.event-b.org/index.php/Event-B_Examples

The example/tutorial projects, and also and a Bundled Windows version, are available in the Deploy E-Prints archive.

The projects are also available from the Examples SVN site.

Sources for Tasking Event-B and Code Generators are available from a branch on the Rodin SVN site.

The Code Generation Demonstrator for Rodin 2.1.x

Released 24 January 2011.

The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at: 

 https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration

The update-site is available through the Rodin update site in the Utilities category.

The code generation tutorial examples are available for download at: 

 https://sourceforge.net/projects/codegenerationd/files/DemoFiles/

The code generation plug-in relies on the Epsilon tool suite. Install Epsilon manually, since the automatic install utility does not seem to work for this feature. We currently use the Epsilon interim update site available at: 

 http://download.eclipse.org/modeling/gmt/epsilon/interim/

Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.

Code Generation Status

Latest Developments

  • Demonstrator plug-in feature version 0.1.0
    • for Rodin 2.1.x version is available.
  • The Code Generation feature consists of,
    • a tasking Development Generator.
    • a tasking Development Editor (Based on an EMF Tree Editor).
    • a translator, from Tasking Development to Common Language Model (IL1).
    • a translator, from the Tasking Development to Event-B model of the implementation.
    • a pretty-printer for the Tasking Development.
    • a pretty-printer for Common Language Model, which generates Ada Source Code.
  • A tutorial is available Code Generation Tutorial
    • Step 1 - Create the tasking development.
    • Step 2 - Add annotations.
    • Step 3 - Invoke translators.

Ongoing Work

  • Full Rodin Integration
  • Sensed Variables
  • Branching in Shared Machines

Future Work

  • Support for Interrupts.
  • Richer DataTypes.
  • Accommodation of duplicate event names in tasking developments.

Metamodels

  • In the plug-in we define several meta-models:
    • CompositeControl: for the control flow (algorithmic) constructs such as branch, loop and sequence etc. These constructs may be used in the specification of either sequential or concurrent systems.
    • Tasking Meta-model: defines the tasking model where we attach tasking specific details, such as task priority, task type. The tasking structures provide the ability to define single tasking or multi-tasking (concurrent) systems. We make use of the composite control plug-in to specify the flow of control.
    • Common Language (IL1) Meta-model: defines an abstraction of common programming language constructs for use in translations to implementations.

Translation Rules

  • Tasking to IL1/Event-B translation rules [[1]]

Release History

The Code Generation Demonstrator for Rodin 1.3.x

First release: 30 November 2010.

available from: 

https://sourceforge.net/projects/codegenerationd/files/

The zip file contains a windows XP bundle, and a Windows V7 bundle. Alternatively, if you wish to build using an update-site, this is also included in the zip file, along with some notes on installation. However, note that the demonstrator tool is only compatible with Rodin 1.3.

A simple shared buffer example is provided. This will form the basis of a tutorial (which is work in progress). The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code Generation plug-ins, together with a patch plug-in. The patch plug-in is required to correct an inconsistency in the org.eventb.emf.persistence plug-in. For the bundles, simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed - the only configuration necessary may be to switch workspace to <installPath>\rodin1.3bWin7\workspace. When using the update-site the example projects, and the project forming the basis of a simple tutorial, are provided in the accompanying zip file. These should be imported manually.

Mac users - no bundled version available at present, but use the update site in the 'advanced' folder.

A step-by-step Code Generation Tutorial is available

About the Initial Release

The Code Generation (CG) Feature in the initial release is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, therefore, there will be a heavy reliance on docs and dialogue to facilitate exploration of the tools and concepts.

Source Code

The sources are available from, 

https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd

Note - I used Eclipse 3.5 Galileo, and you will need to install (or have sources from) Epsilon's interim update site. There is also dependency on Camille v2.0.0

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