Difference between revisions of "Code Generation Tutorial"
From Event-B
Jump to navigationJump to searchimported>Andy |
imported>Andy |
||
Line 8: | Line 8: | ||
* Step 2 - Add annotations. | * Step 2 - Add annotations. | ||
* Step 3 - Invoke translators. | * Step 3 - Invoke translators. | ||
+ | |||
+ | ==== Creating The Tasking Development ==== | ||
+ | |||
+ | 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, if necessary change to the resource perspective. |
Revision as of 16:13, 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
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, if necessary change to the resource perspective.