Difference between pages "AnimB limitations" and "Code Generation Activity"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Wohuai
(New page: When you try to animate a non-trivial model, it might happen that you get an internal error. It might also happen that some events are gray, which means that the animator is unable to eval...)
 
imported>Andy
 
Line 1: Line 1:
When you try to animate a non-trivial model, it might happen that you get an
+
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
internal error.
+
=== Code Generation Feature - Version 0.2.0 ===
It might also happen that some events are gray, which means that the animator is unable
+
This section is undergoing maintenance. We are planning to release a new version of the code generator in the next few days.
to evaluate their guards.  
+
The main changes are:
Below we list some guidelines of how to prevent such problems. This page will be continuously updated.
+
* The new code generators have been completely re-written. The translators are now implemented in Java, i.e. there is no longer a dependence on the Epsilon tool set. This was undertaken for code maintenance reasons.
 +
* Tasking Event-B is now integrated with the Event-B explorer.
 +
* The Rose Editor is used for editing the Tasking Event-B, and
 +
* a TaskBody text-based editor is provided, in Rose, for specifying the flow control. This feature has been added to address some of the usability issues.
 +
* The EMF tree editor in Rose is only used minimally, and we plan further enhancements to reduce this.
 +
* Composed machines are used to store event 'synchronizations'. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events.
 +
* The code generation approach is now extensible; new target language constructs can be added using the Eclipse extension mechanism.
 +
* The translation, of the mathematical language of target languages, is specified in the Theory plug-in.
 +
* Translated code is deposited in a directory in the appropriate files. An Ada project file is generated for use with AdaCore's GPS workbench. Eventually this could be enabled/disabled in a preferences dialog box.
  
==Finding the Source of the Problem==
+
=== 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.
  
AnimB sends error messages to the "Console" (Window -> Show View -> Other -> General -> Console).
+
* The new v0.1.5 feature is available from the Rodin Update Site, it resides in the Utilities Category.
This error messages might help you to find out the places of your model that you have to change.
 
  
==How To Write Your Event-B Models==
+
* 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/
  
AnimB cannot properly deal with every Event-B model. If you want to animate your model, you have to write it in a certain way. We give some guidelines, which you have to apply to <b>any</b> machine and <b>any</b> context.
+
* Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
  
* AnimB (currently) does not read invariants, theorems, the variant, or axioms. So changing any of them will not solve problems with the animator.
+
A new [http://wiki.event-b.org/index.php?title=Tasking_Event-B_Tutorial Code Generation Tutorial] has been produced, that makes use of these new features. There is an explanation of the heating controller, upon which it is based, [http://wiki.event-b.org/index.php/Development_of_a_Heating_Controller_System here].
* Avoid all sorts of relational operators (<math>\pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij,
 
\rel, \trel, \srel, \strel</math>).
 
* AnimB is not good in inferring the types of parameters and quantified variables. For each event parameter you might need a guard stating the type of the parameter. For each quantified variable you have to state the type of the variable. Write:
 
# <math>\forall x\qdot x \in PERSON \limp x \in \dom(mother)</math>
 
# <math>\exists x\qdot x \in PERSON \land x \in \ran(mother)</math>
 
Do not write:
 
# <math>\forall x\qdot x \in \dom(mother)</math>
 
# <math>\exists x\qdot x \in \ran(mother)</math>
 
* AnimB cannot really deal with integers.
 
  
==Avoid Simultaneous Animation of All Machines==
+
The example/tutorial projects, and also and a Bundled Windows 7 version, are available in the [http://deploy-eprints.ecs.soton.ac.uk/304/ Deploy E-Prints archive] or [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/HeatingController_Tutorial_v0.1.4/ Examples SVN site].
The animator tries to animate all machines simultaneously, not only the
 
last one. If you do not want to adopt all your machines so that the animator can
 
handle them, you might apply the following steps:
 
  
* Create a new machine <b>m_anim</b> that refines the machine <b>m</b> you want to animate. The new machine <b>m_anim</b> should have the same events as <b>m</b>.
+
=== The Code Generation Demonstrator for Rodin 2.1.x ===
* Change <b>m_anim</b> such that it does not refine <b>m</b> anymore.
+
 
** Set the field "Abstract Machine" in "Dependencies" to "None".
+
Released 24 January 2011.
** Remove all "Refines" clauses from all events.
+
 
** Add trivial typing invariants to avoid error messages from the type checker.
+
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
* If you have not already done that in <b>m</b>, add type information for parameters and quantified variables.
+
 
 +
  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 [[http://wiki.event-b.org/images/Translation.pdf]]
 +
 
 +
== 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
 +
 
 +
 
 +
 
 +
[[Category:Work in progress]]

Revision as of 15:51, 24 November 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

Code Generation Feature - Version 0.2.0

This section is undergoing maintenance. We are planning to release a new version of the code generator in the next few days. The main changes are:

  • The new code generators have been completely re-written. The translators are now implemented in Java, i.e. there is no longer a dependence on the Epsilon tool set. This was undertaken for code maintenance reasons.
  • Tasking Event-B is now integrated with the Event-B explorer.
  • The Rose Editor is used for editing the Tasking Event-B, and
  • a TaskBody text-based editor is provided, in Rose, for specifying the flow control. This feature has been added to address some of the usability issues.
  • The EMF tree editor in Rose is only used minimally, and we plan further enhancements to reduce this.
  • Composed machines are used to store event 'synchronizations'. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events.
  • The code generation approach is now extensible; new target language constructs can be added using the Eclipse extension mechanism.
  • The translation, of the mathematical language of target languages, is specified in the Theory plug-in.
  • Translated code is deposited in a directory in the appropriate files. An Ada project file is generated for use with AdaCore's GPS workbench. Eventually this could be enabled/disabled in a preferences dialog box.

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 new v0.1.5 feature is available from the Rodin Update Site, it resides in the Utilities Category.
  • Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.

A new Code Generation Tutorial has been produced, that makes use of these new features. There is an explanation of the heating controller, upon which it is based, here.

The example/tutorial projects, and also and a Bundled Windows 7 version, are available in the Deploy E-Prints archive or Examples 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