Code Generation Tutorial: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Andy |
imported>Andy |
||
| Line 19: | Line 19: | ||
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, change to the resource perspective. | The new Tasking Development will not be visible in the Event-B perspective, change to the resource perspective, open and inspect the new .tasking file. The Tasking Development contains the machines that we wish to provide implementations for. | ||
Revision as of 16:17, 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, open and inspect the new .tasking file. The Tasking Development contains the machines that we wish to provide implementations for.
