Difference between revisions of "Code Generation Tutorial"

From Event-B
Jump to navigationJump to search
imported>Andy
imported>Andy
Line 10: Line 10:
  
 
==== Creating The Tasking Development ====
 
==== Creating The Tasking Development ====
 +
 +
From the Event-B Perspective,
  
 
Open the SharedBuffer20100819Tutorial Project.  
 
Open the SharedBuffer20100819Tutorial Project.  
 +
 
Select the following Machines: Reader, Writer and Shared.
 
Select the following Machines: Reader, Writer and Shared.
 +
 
Right-click and select Make Tasking Development/Generate Tasking Development.
 
Right-click and select Make Tasking Development/Generate Tasking Development.
  
The new Tasking Development will not be visible in the Event-B perspective, if necessary change to the resource perspective.
+
The new Tasking Development will not be visible in the Event-B perspective, change to the resource perspective.

Revision as of 16:14, 7 December 2010

This Page is Under Construction

Tutorial

The aim of the tutorial is to give a allow users to explore the approach with a relatively simple example. The example uses a shared buffer and reader and writer process.

  • Step 1 - Create the tasking development.
  • Step 2 - Add annotations.
  • Step 3 - Invoke translators.

Creating The Tasking Development

From the Event-B Perspective,

Open the SharedBuffer20100819Tutorial Project.

Select the following Machines: Reader, Writer and Shared.

Right-click and select Make Tasking Development/Generate Tasking Development.

The new Tasking Development will not be visible in the Event-B perspective, change to the resource perspective.