Difference between pages "Code Generation Activity" and "FAQ"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Laurent
 
Line 1: Line 1:
−
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
+
== General ==
−
=== Code Generation Feature - Version 0.2.0 For Rodin 2.3===
+
=== What is Event-B? ===
−
This section is undergoing maintenance. We have release a new version of the code generator on 30/11/11, and documentation is being updated where necessary.
+
'''Event-B''' is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. More details are available in http://www.event-b.org/
−
===== Changes to the Tooling and Approach =====
 
−
The main changes are:
 
−
* The 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 text-based editor is provided, using the Rose extension, for editing the TaskBody. This feature has been added to address some of the usability concerns. It also overcomes the 'problem' experienced with duplicate event names in a development, since the parser-builder that has been implemented automatically selects the correct event.
 
−
* The EMF tree editor in Rose is only used minimally; we plan enhancements to further reduce its use.
 
−
* Composed machines are used to store event 'synchronizations'; these are generated automatically during the decomposition process. 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 target's mathematical language is now specified in the theory plug-in. This improves clarity since the the translation from source to target is achieved by specifying pattern matching rules. Extensibility is also improved; the theory plug-in is used to specify new data-types, and how they are implemented.
 
−
* 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.
 
−
* The Tasking Event-B to Event-B translator is now properly integrated. Control variable updates to the Event-B model are made in a similar way to the equivalent updates in the state-machine plug-in. The additional elements are added to the Event-B model and marked as 'generated'. This prevents users from manually modifying them, and allows them to be removed through a menu choice.
 
  
−
===== Changes to the Documentation =====
+
=== What is Rodin? ===
−
The following Pages have been updated:
+
The '''Rodin Platform''' is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.
−
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Overview Tasking Event-B Overview]
 
−
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Tutorial Tutorial]
 
  
−
===== Downloads =====
+
=== Where does the ''Rodin'' name come from? ===
−
* The Code Generation feature is available by accessing the main Rodin Update Site. In Eclispe click on Help/Install new Software. Find the Rodin update site from the list. In Utilities add Code Generation.
 
−
* There is a dependency on the 'Model Decomposition' and 'Shared Event Decomposition'. These can be downloaded from the main Rodin Update Site, in the Decomposition section.
 
−
* Tutorial projects are available from [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd SVN].
 
−
* Sources at: ???
 
  
 +
== General Tool Usage? ==
  
−
TODO
+
=== How do I install external plug-ins without using Eclipse Update Manager? ===
−
* Add array types.
+
Although it is preferred to install additional plug-ins into the Rodin platform using the Update Manager of Eclipse, this might not always be practical. In this case, a manner to install these plug-ins is to emulate either manually or using ad-hoc scripts the operations normally performed by the Update Manager.
−
* Add addressed variables (for direct read/write access to memory)
 
−
* Flattening of composed machines/implementation machines.
 
−
* Interrupts
 
  
−
=== Sensing and Actuating for Tasking Event-B ===
+
This manual installation of plug-ins is described in ''[[Installing external plug-ins manually]]''.
−
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.
+
=== The builder takes too long ===
 +
Generally, the builder spends most of its time attempting to prove POs. There are basically two ways to get it out of the way:
 +
* the first one is to disable the automated prover in the Preferences panel.
 +
* the second one is to mark some PO as reviewed when you don't want the auto-prover to attempt them anymore.
 +
Note that if you disable the automated prover, you always can run it later on some files by using the contextual menu in the event-B Explorer.
  
−
* 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/
+
To disable the automated prover, open Rodin <tt>Preferences</tt> (menu {{menu|Window > Preferences...}}).  In the tree in the left-hand panel, select {{menu|Event-B > Sequent Prover > Auto-tactic}}. Then, in the right-hand panel ensure that the checkbox labelled <tt>Enable auto-tactic for proving</tt> is disabled.
  
−
* Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
To review a proof obligation, just open it in the interactive prover, then click on the ''review'' button (this is a round blue button with a ''R'' in the proof control toolbar).  The proof obligation should now labelled with the same icon in the event-B explorer.
  
−
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].
+
===What are the ASCII shortcuts for mathematical operators===
  
−
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 ASCII shortcuts that can be used for entering mathematical operators are described in the help of the event-B keyboard plug-in. In the help system, this page has the following path {{menu|Event-B Keyboard User Guide > Getting Started > Special Combos}}.
  
−
=== The Code Generation Demonstrator for Rodin 2.1.x ===
+
This page is also available in the dynamic help system.  The advantage of using dynamic help is that it allows to display the help page side-by-side with the other views and editors. To start the dynamic help, click {{menu|Help > Dynamic Help}}, then click {{menu|All Topics}} and select the page in the tree.
  
−
Released 24 January 2011.
+
== Modeling and Proving==
 +
=== Witness for {{Ident|Xyz}} missing. Default witness generated ===
 +
A parameter as disappeared during a refinement. If this is intentional, you have to add a [[Witnesses (Modelling Language)|witness]] telling how the abstract parameter is refined.
  
−
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
+
=== I've added a witness for {{ident|Xyz}} but it keeps saying ''"Identifier {{ident|Xyz}} has not been defined"'' ===
 +
As specified in the [[Witnesses (Modelling Language)|modelling language manual]], the witness must be labelled by the name {{Ident|Xyz}} of the concrete variable being concerned.
  
−
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
+
=== How can I do a Proof by Induction? ===
 +
[[Induction proof]] will give you some tips about it.
  
−
The update-site is available through the Rodin update site in the ''Utilities'' category.
+
=== Labels  of proof tree nodes explained ===
 +
* {{ident|ah}} means ''add hypothesis'',
 +
* {{ident|eh}} means rewrite with ''equality from hypothesis'' from left to right,
 +
* {{ident|he}} means rewrite with ''equality from hypothesis'' from right to left,
 +
* {{ident|rv}} tell us that this goal as been manually [[The_Proving_Perspective_(Rodin_User_Manual)#The_Proof_Control_Window|reviewed]],
 +
* {{ident|sl/ds}} means ''selection/deselection'',
 +
* {ident|PP}} means ''discharged by the predicate prover''
 +
* {{ident|ML}} means ''discharged by the mono lemma prover''
  
−
The code generation tutorial examples are available for download at:
+
== Developer FAQ ==
 +
=== Using Rodin-CVS from eclipse consumes too much memory ===
 +
You can [[#How do I generate a Rodin product from CVS|generate a product]] and use it as if it was a normal release.
  
−
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
+
=== How do I generate a ''Rodin'' product from CVS? ===
 +
In the project ''org.rodinp.platform'', right-click on ''Rodin.platform'' and select {{menu|export}}. Choose {{menu|Plug-in Development > Eclipse product}} and click on {{button|Next}} type <tt>Rodin</tt> for the ''Root directory'', and choose the ''Destination directory''. Then click on {{button|Finish}}.
  
−
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:
+
=== How do I collect debug information from the Rodin platform? ===
 +
You may see the log in the console by appending <tt>-consoleLog</tt> to the rodin executable: <code>rodin -consoleLog</code>
  
−
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
+
You may add specific debug informations by setting specific options: <code>rodin --debug options.file -consoleLog</code> where {{file|options.file}} contains something like:
 +
<pre>
 +
org.pluginname/debug = true
 +
org.pluginname/debug/optionaldebug = true
 +
</pre>
 +
where'' optionaldebug'' may be found in the {{file|org.pluginname/.options}} file in the [http://rodin-b-sharp.cvs.sourceforge.net/rodin-b-sharp/ rodin source repository].
  
−
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
=== How do I submit a patch? ===
 +
Good practises for patch submission are described [[How to Submit Patches|here]].
  
−
== Code Generation Status ==
+
=== How do I track memory leaks? ===
−
=== Latest Developments ===
+
If you suspect that some memory isn't freed, you may find some useful directions on how to track memory leaks [[Tracking Memory Leaks|here]].
−
* Demonstrator plug-in feature version 0.1.0
 
−
** for Rodin 2.1.x version is available.
 
  
−
* The Code Generation feature consists of,
+
[[Category:User FAQ]]
−
** a tasking Development Generator.
+
[[Category:Developer FAQ]]
−
** 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:10, 11 February 2009

General

What is Event-B?

Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. More details are available in http://www.event-b.org/

What is Rodin?

The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.

Where does the Rodin name come from?

General Tool Usage?

How do I install external plug-ins without using Eclipse Update Manager?

Although it is preferred to install additional plug-ins into the Rodin platform using the Update Manager of Eclipse, this might not always be practical. In this case, a manner to install these plug-ins is to emulate either manually or using ad-hoc scripts the operations normally performed by the Update Manager.

This manual installation of plug-ins is described in Installing external plug-ins manually.

The builder takes too long

Generally, the builder spends most of its time attempting to prove POs. There are basically two ways to get it out of the way:

  • the first one is to disable the automated prover in the Preferences panel.
  • the second one is to mark some PO as reviewed when you don't want the auto-prover to attempt them anymore.

Note that if you disable the automated prover, you always can run it later on some files by using the contextual menu in the event-B Explorer.

To disable the automated prover, open Rodin Preferences (menu Window > Preferences...). In the tree in the left-hand panel, select Event-B > Sequent Prover > Auto-tactic. Then, in the right-hand panel ensure that the checkbox labelled Enable auto-tactic for proving is disabled.

To review a proof obligation, just open it in the interactive prover, then click on the review button (this is a round blue button with a R in the proof control toolbar). The proof obligation should now labelled with the same icon in the event-B explorer.

What are the ASCII shortcuts for mathematical operators

The ASCII shortcuts that can be used for entering mathematical operators are described in the help of the event-B keyboard plug-in. In the help system, this page has the following path Event-B Keyboard User Guide > Getting Started > Special Combos.

This page is also available in the dynamic help system. The advantage of using dynamic help is that it allows to display the help page side-by-side with the other views and editors. To start the dynamic help, click Help > Dynamic Help, then click All Topics and select the page in the tree.

Modeling and Proving

Witness for
Xyz
missing. Default witness generated

A parameter as disappeared during a refinement. If this is intentional, you have to add a witness telling how the abstract parameter is refined.

I've added a witness for
Xyz
but it keeps saying "Identifier
Xyz
has not been defined"

As specified in the modelling language manual, the witness must be labelled by the name

Xyz

of the concrete variable being concerned.

How can I do a Proof by Induction?

Induction proof will give you some tips about it.

Labels of proof tree nodes explained

  • ah
    means add hypothesis,
  • eh
    means rewrite with equality from hypothesis from left to right,
  • he
    means rewrite with equality from hypothesis from right to left,
  • rv
    tell us that this goal as been manually reviewed,
  • sl/ds
    means selection/deselection,
  • {ident|PP}} means discharged by the predicate prover
  • ML
    means discharged by the mono lemma prover

Developer FAQ

Using Rodin-CVS from eclipse consumes too much memory

You can generate a product and use it as if it was a normal release.

How do I generate a Rodin product from CVS?

In the project org.rodinp.platform, right-click on Rodin.platform and select export. Choose Plug-in Development > Eclipse product and click on Next type Rodin for the Root directory, and choose the Destination directory. Then click on Finish.

How do I collect debug information from the Rodin platform?

You may see the log in the console by appending -consoleLog to the rodin executable: rodin -consoleLog

You may add specific debug informations by setting specific options: rodin --debug options.file -consoleLog where

options.file

contains something like: 

org.pluginname/debug = true
org.pluginname/debug/optionaldebug = true

where optionaldebug may be found in the

org.pluginname/.options

file in the rodin source repository.

How do I submit a patch?

Good practises for patch submission are described here.

How do I track memory leaks?

If you suspect that some memory isn't freed, you may find some useful directions on how to track memory leaks here.

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