Code Generation Tutorial - Revision history

imported>Andy: /* Tutorial Overview */

2010-12-14T08:25:10Z

Tutorial Overview

← Older revision		Revision as of 08:25, 14 December 2010
Line 16:		Line 16:
	\|-		\|-
	\|SharedBuffer20100819Tutorial		\|SharedBuffer20100819Tutorial
	\|A bare project for step 1 of the tutorial.		\|A bare project for step 1 of the [[Code_Generation_Tutorial#The_Tutorial \|tutorial]].
	\|-		\|-
	\|Sharedbuffer20100819Tutorial2		\|Sharedbuffer20100819Tutorial2
	\|A partially completed tasking development for steps 2 and 3 of the tutorial.		\|A partially completed tasking development for steps 2 and 3 of the [[Code_Generation_Tutorial#The_Tutorial \|tutorial]].
	\|}		\|}

imported>Andy: /* Tutorial Overview */

2010-12-13T11:47:16Z

Tutorial Overview

← Older revision		Revision as of 11:47, 13 December 2010
Line 2:		Line 2:
	=== Tutorial Overview ===		=== Tutorial Overview ===

	The aim of the tutorial is to allow users to explore the approach with a relatively simple example. The example uses a shared buffer with reader and writer processes. The tutorial is presented in three stages, making use of the example projects from the download site. There are two translations performed, one is to a common language model (IL1). The second is to an Event-B project which includes a model of the implementation. There is a PrettyPrinter for Ada source code, which uses the common language model. An overview of Tasking Event-B can be found ~~at http://wiki.event-b.org/index.php/~~Tasking_Event-B_Overview.		The aim of the tutorial is to allow users to explore the approach with a relatively simple example. The example uses a shared buffer with reader and writer processes. The tutorial is presented in three stages, making use of the example projects from the download site. There are two translations performed, one is to a common language model (IL1). The second is to an Event-B project which includes a model of the implementation. There is a PrettyPrinter for Ada source code, which uses the common language model. An overview of Tasking Event-B can be found on the [[Tasking_Event-B_Overview]] page.

	A typical Event-B development may be refined to the point where it is ready for implementation, but the Event-B language is not expressive enough to fully describe the implementation. Tasking Event-B facilitates this final step to implementation, by extending Event-B with the necessary constructs. Event-B machines that are to be implemented (and their seen Contexts) are selected and added to a ''Tasking Development''; the Tasking Development files have the file extension ''.tasking''. The machines in the Tasking Development are then extended with implementation details.		A typical Event-B development may be refined to the point where it is ready for implementation, but the Event-B language is not expressive enough to fully describe the implementation. Tasking Event-B facilitates this final step to implementation, by extending Event-B with the necessary constructs. Event-B machines that are to be implemented (and their seen Contexts) are selected and added to a ''Tasking Development''; the Tasking Development files have the file extension ''.tasking''. The machines in the Tasking Development are then extended with implementation details.

imported>Andy at 11:38, 13 December 2010

2010-12-13T11:38:52Z

← Older revision		Revision as of 11:38, 13 December 2010
Line 167:		Line 167:
	* Repeat for the same errors in the other machines; save and clean again.		* Repeat for the same errors in the other machines; save and clean again.
	* The machines can viewed as normal using the Rodin editors.		* The machines can viewed as normal using the Rodin editors.

			[[Category:User documentation]]

imported>Andy at 10:43, 13 December 2010

2010-12-13T10:43:36Z

← Older revision		Revision as of 10:43, 13 December 2010
Line 1:		Line 1:
	~~'''This Page is Under Construction!!!!'''~~		For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk

	=== Tutorial Overview ===		=== Tutorial Overview ===

imported>Andy: /* Invoking the Translation */

2010-12-13T10:40:43Z

Invoking the Translation

← Older revision		Revision as of 10:40, 13 December 2010
Line 166:		Line 166:
	* Select the original refined machine again.		* Select the original refined machine again.
	* Save and clean the project, and the error should disappear.		* Save and clean the project, and the error should disappear.
	* Repeat for the same errors in the other machines ~~and~~ save and clean again.		* Repeat for the same errors in the other machines; save and clean again.
	* The machines can viewed as normal using the Rodin editors.		* The machines can viewed as normal using the Rodin editors.

imported>Andy: /* Invoking the Translation */

2010-12-13T10:39:47Z

Invoking the Translation

← Older revision		Revision as of 10:39, 13 December 2010
Line 159:		Line 159:
	** The ''sharedbuffer20100819bTasking'' project is generated, it can be opened and inspected.		** The ''sharedbuffer20100819bTasking'' project is generated, it can be opened and inspected.

	There are errors in the generated machines (not investigated the cause yet); these can be fixed in the following way,		There are errors in the generated machines (not investigated the cause yet); these can be fixed in the following way.
	* Open a Machine in the Event-B Machine Editor.		* Open a Machine in the Event-B Machine Editor.
	* Select the Edit tab.		* Select the Edit tab.

imported>Andy: /* Invoking the Translation */

2010-12-13T10:38:49Z

Invoking the Translation

← Older revision		Revision as of 10:38, 13 December 2010
Line 146:		Line 146:

	==== Invoking the Translation ====		==== Invoking the Translation ====

			* To create the IL1 model,
			** Right-Click on the Main node, select ''Epsilon Translation/Translate Task Mch 2 IL1 EMF''.
			** Open the Resource Perspective.
			** Right-click on the ''sharedbuffer20100819Tutorial2'' project folder.
			** Select refresh, the ''.il1'' file should appear in the project.
			** Open and inspect the file, and view the source code by opening the IL1 Pretty Print view if desired.

			* To create the Event-B model of the implementation,
			** Return to the Rodin Modelling Perspective.
			** Right-Click on the Main node, select ''Epsilon Translation/Translate Task Mch 2 Event-B EMF''.
			** The ''sharedbuffer20100819bTasking'' project is generated, it can be opened and inspected.

			There are errors in the generated machines (not investigated the cause yet); these can be fixed in the following way,
			* Open a Machine in the Event-B Machine Editor.
			* Select the Edit tab.
			* Open the REFINES section, the error lies here.
			* The correct machine is refined, but choose a different machine to refine (any one, it doesn't matter).
			* Select the original refined machine again.
			* Save and clean the project, and the error should disappear.
			* Repeat for the same errors in the other machines and save and clean again.
			* The machines can viewed as normal using the Rodin editors.

imported>Andy: /* A summary of steps taken */

2010-12-10T16:42:54Z

A summary of steps taken

← Older revision		Revision as of 16:42, 10 December 2010
Line 129:		Line 129:
	** Go to the ''Parameter Type'' properties view and set the ''Parameter Type'' property to ''formalOut''.		** Go to the ''Parameter Type'' properties view and set the ''Parameter Type'' property to ''formalOut''.

	===== A ~~summary~~ of ~~steps taken~~ =====		===== A Summary of Steps =====

	For a Tasking Machine definition:		For a Tasking Machine definition:

imported>Andy: /* The Shared Machine */

2010-12-10T16:42:05Z

The Shared Machine

← Older revision		Revision as of 16:42, 10 December 2010
Line 129:		Line 129:
	** Go to the ''Parameter Type'' properties view and set the ''Parameter Type'' property to ''formalOut''.		** Go to the ''Parameter Type'' properties view and set the ''Parameter Type'' property to ''formalOut''.

	~~To summarise~~, ~~for~~ a Shared Machine definition:		===== A summary of steps taken =====

			For a Tasking Machine definition:
			# Add the Tasking Machine type (Auto etc).
			# Add the task type (Periodic etc.).
			# Define the task priority.
			# Define the task body.
			# For each event, add the Event Type.
			# For each event parameter, add the Parameter Type.


			For a Shared Machine definition:
	# Add the ''SharedMachine'' Machine type.		# Add the ''SharedMachine'' Machine type.
	# For each event, define the Event Type.		# For each event, define the Event Type.

imported>Andy: /* Invoking the Translators */

2010-12-10T16:35:23Z

Invoking the Translators

← Older revision		Revision as of 16:35, 10 December 2010
Line 134:		Line 134:
	# For each event parameter, define the Parameter Type.		# For each event parameter, define the Parameter Type.

	=== Invoking the ~~Translators~~ ===		==== Invoking the Translation ====