Tasking Event-B Tutorial - Revision history

imported>Andy: /* Invoking the Translators */

2013-09-02T12:41:45Z

Invoking the Translators

← Older revision		Revision as of 12:41, 2 September 2013
Line 133:		Line 133:
	== Invoking the Translators ==		== Invoking the Translators ==

	* To generate ~~Ada~~ code,		* To generate code,
	** Right-Click on the composed machine, or any tasking machine in the development, select ''Code Generation/Translate Event-B to ~~Ada~~''.		** Right-Click on the composed machine, or any tasking machine in the development, select ''Code Generation/Translate Event-B to xx'' where ''xx'' is the chosen language.
	** Open the generated ''code'' directory in the project to view the source files~~. A refresh will be necessary to make the code visible. The .gpr file has been provided for AdaCore GPS users~~.		** Open the generated ''code'' directory in the project to view the source files.

	* To create the Event-B model of the implementation,		* To create the Event-B model of the implementation,

imported>Andy: /* A Summary of Steps */

2013-09-02T12:40:43Z

A Summary of Steps

← Older revision		Revision as of 12:40, 2 September 2013
Line 130:		Line 130:

	When saving, the task body text is sent to the parser. If parsing is successful then a builder adds the structure to the underlying EMF tree. If parsing fails then an error panel displays the source of the error.		When saving, the task body text is sent to the parser. If parsing is successful then a builder adds the structure to the underlying EMF tree. If parsing fails then an error panel displays the source of the error.

	~~=== A Summary of Steps ===~~
	~~For a Tasking Machine definition:~~
	~~# Select the Tasking Machine type (Auto etc).~~
	~~# Set the task type (Periodic etc.).~~
	~~# Set the task priority.~~
	~~# Specify the task body.~~
	~~<!-- # For sensing/actuating events, add the Event Type. -->~~

	~~For a Shared Machine definition:~~
	~~# Add the ''SharedMachine'' Machine type.~~

	~~For an Environ Machine definition:~~
	~~# Make the type an Environ Machine type.~~
	~~# Set the task type Periodic; a shorter period than the shortest task period is best for simulation.~~
	~~# Set the task priority.~~
	~~# Specify the task body, it will contain a simulation of changes in the environment.~~
	~~# For each sensing/actuating event, add the Event Type.~~

	== Invoking the Translators ==		== Invoking the Translators ==

imported>Andy: /* The Environ Machine */

2013-09-02T12:40:27Z

The Environ Machine

@@ Line 126: / Line 126: @@
 **Copy and paste the task body from ''Heating_ControllerTutorial2_Completed/Envir1Impl''
 **Save the model.
 In the implementation, ''Environ Tasks'' are declared and defined in the ''Main'' procedure . The ''Envir1Impl'' machine models a task that simulates the environment, and can be used to generate simulation code. For deployment in a non-simulated environment the environ machine's generated code can be ignored. To specify the Environment task's behaviour we add edit the task body.
 When saving, the task body text is sent to the parser. If parsing is successful then a builder adds the structure to the underlying EMF tree. If parsing fails then an error panel displays the source of the error.
 === A Summary of Steps ===

imported>Andy: /* The Environ Machine */

2013-09-02T12:38:36Z

The Environ Machine

@@ Line 115: / Line 115: @@
 *A Machine Type element is created.
 *Select ''Environ Machine'' in the drop down box.
 In the implementation, ''Environ Tasks'' are declared and defined in the ''Main'' procedure . The ''Envir1Impl'' machine models a task that simulates the environment, and can be used to generate simulation code. For deployment in a non-simulated environment the environ machine's generated code can be ignored. To specify the Environment task's behaviour we add edit the task body.

imported>Andy: /* The Temp_Ctrl_TaskImpl Machine */

2013-09-02T12:35:59Z

The Temp_Ctrl_TaskImpl Machine

← Older revision		Revision as of 12:35, 2 September 2013
Line 92:		Line 92:
	**The machine type defaults to ''Auto Task''.		**The machine type defaults to ''Auto Task''.
	**Click on the right-arrow symbol by ''Machine Type''.		**Click on the right-arrow symbol by ''Machine Type''.
	**Add a new Task ~~Body~~ section by clicking on its green + symbol.		**Add a new Task Type section by clicking on its green + symbol.
	**A Machine Type element is added. The task type defaults to ''Periodic''		**A Machine Type element is added. The task type defaults to ''Periodic''
	**Set a period of 250 milliseconds.		**Set a period of 250 milliseconds.
	*'''Add a new TaskBody'''.		*'''Add a new TaskBody'''.
			**Add a new Task Body section by clicking on its green + symbol.
	**Copy and paste the task body from ''Heating_ControllerTutorial2_Completed/Temp_Ctrl_TaskImpl''		**Copy and paste the task body from ''Heating_ControllerTutorial2_Completed/Temp_Ctrl_TaskImpl''
	**Save the model. Ignore the highlighted typing errors, since these annotations will be added by the code generator during pre-processing.		**Save the model. Ignore the highlighted typing errors, since these annotations will be added by the code generator during pre-processing.

imported>Andy: /* The Temp_Ctrl_TaskImpl Machine */

2013-09-02T12:34:41Z

The Temp_Ctrl_TaskImpl Machine

← Older revision		Revision as of 12:34, 2 September 2013
Line 89:		Line 89:
	During this part of the tutorial we will cut and paste from ''Heating_ControllerTutorial2_Completed'' model when, specifying the task bodies, to save typing. We use the 'Event-B Machine Editor' to edit the Tasking Event-B.		During this part of the tutorial we will cut and paste from ''Heating_ControllerTutorial2_Completed'' model when, specifying the task bodies, to save typing. We use the 'Event-B Machine Editor' to edit the Tasking Event-B.

	**In the Tasking section of the Event-B editor, click on + to add a new Machine Type construct.		*In the Tasking section of the Event-B editor, click on + to add a new Machine Type construct.
	*The machine type defaults to ''Auto Task''.		**The machine type defaults to ''Auto Task''.
	**Click on the right-arrow symbol by ''Machine Type''.		**Click on the right-arrow symbol by ''Machine Type''.
	**Add a new Task Body section by clicking on its green + symbol.		**Add a new Task Body section by clicking on its green + symbol.

imported>Andy: /* The Temp_Ctrl_TaskImpl Machine */

2013-09-02T12:34:13Z

The Temp_Ctrl_TaskImpl Machine

← Older revision		Revision as of 12:34, 2 September 2013
Line 89:		Line 89:
	During this part of the tutorial we will cut and paste from ''Heating_ControllerTutorial2_Completed'' model when, specifying the task bodies, to save typing. We use the 'Event-B Machine Editor' to edit the Tasking Event-B.		During this part of the tutorial we will cut and paste from ''Heating_ControllerTutorial2_Completed'' model when, specifying the task bodies, to save typing. We use the 'Event-B Machine Editor' to edit the Tasking Event-B.

	*~~Add a~~ Tasking ~~element by clicking~~ on ~~the green~~ + ~~symbol next~~ to ~~Tasking~~.		**In the Tasking section of the Event-B editor, click on + to add a new Machine Type construct.
	*The machine type defaults to ''Auto Task''.		*The machine type defaults to ''Auto Task''.
			**Click on the right-arrow symbol by ''Machine Type''.
	~~''Auto Tasks'' are tasks that will be declared and defined in~~ the ''~~Main'' procedure of the implementation. The effect of this is that the ''Auto Tasks'' are created when the program first loads, and then activated (made ready to run) before the~~ ''~~Main'' procedure body runs~~.		**Add a new Task Body section by clicking on its green + symbol.
			**A Machine Type element is added. The task type defaults to ''Periodic''
	**~~In the Tasking~~ section ~~of the Event-B editor, click~~ on + ~~to add a new Task Type construct~~.
	**A Machine Type element is added.
	**The task type defaults to ''Periodic'',
	**Set a period of 250 milliseconds.		**Set a period of 250 milliseconds.

	*'''Add a new TaskBody'''.		*'''Add a new TaskBody'''.
	**Add a new Task Body section by clicking on +.
	**Copy and paste the task body from ''Heating_ControllerTutorial2_Completed/Temp_Ctrl_TaskImpl''		**Copy and paste the task body from ''Heating_ControllerTutorial2_Completed/Temp_Ctrl_TaskImpl''
	**Save the model. Ignore the highlighted typing errors, since these annotations will be added by the code generator during pre-processing.		**Save the model. Ignore the highlighted typing errors, since these annotations will be added by the code generator during pre-processing.

			''Auto Tasks'' are tasks that will be declared and defined in the ''Main'' procedure of the implementation. The effect of this is that the ''Auto Tasks'' are created when the program first loads, and then activated (made ready to run) before the ''Main'' procedure body runs.

	==== The Shared Machine ====		==== The Shared Machine ====

imported>Andy: /* The Temp_Ctrl_TaskImpl Machine */

2013-09-02T12:28:17Z

The Temp_Ctrl_TaskImpl Machine

← Older revision		Revision as of 12:28, 2 September 2013
Line 94:		Line 94:
	''Auto Tasks'' are tasks that will be declared and defined in the ''Main'' procedure of the implementation. The effect of this is that the ''Auto Tasks'' are created when the program first loads, and then activated (made ready to run) before the ''Main'' procedure body runs.		''Auto Tasks'' are tasks that will be declared and defined in the ''Main'' procedure of the implementation. The effect of this is that the ''Auto Tasks'' are created when the program first loads, and then activated (made ready to run) before the ''Main'' procedure body runs.

	**~~Open The~~ Tasking section of the Event-B editor.		**In the Tasking section of the Event-B editor, click on + to add a new Task Type construct.
	**Click on + to add a new Task Type construct.		**A Machine Type element is added.
	**~~Open Task Type (click on \|> right arrow) in the~~ Machine Type element.
	**The task type defaults to ''Periodic'',		**The task type defaults to ''Periodic'',
	**Set a period of 250 milliseconds.		**Set a period of 250 milliseconds.

	*'''Add a new TaskBody'''.		*'''Add a new TaskBody'''.
	**Add a new Task Body section.		**Add a new Task Body section by clicking on +.
	**Copy and paste the task body from ''Heating_ControllerTutorial2_Completed/Temp_Ctrl_TaskImpl''		**Copy and paste the task body from ''Heating_ControllerTutorial2_Completed/Temp_Ctrl_TaskImpl''
	**Save the model. Ignore the highlighted typing errors, since these annotations will be added by the code generator during pre-processing.		**Save the model. Ignore the highlighted typing errors, since these annotations will be added by the code generator during pre-processing.

imported>Andy: /* The Environ Machine */

2013-09-02T12:26:54Z

The Environ Machine

← Older revision		Revision as of 12:26, 2 September 2013
Line 115:		Line 115:
	We identify the ''Envir1Impl'' as an ''Environ Machine'',		We identify the ''Envir1Impl'' as an ''Environ Machine'',

	*Click on +, in the Machine Editor, to add a to add a Tasking Section,		*Click on +, in the Machine Editor, to add a to add a Tasking Section.
	* ~~machine type~~.		*A Machine Type element is created.
	*Select ''Environ Machine'' in the drop down box.		*Select ''Environ Machine'' in the drop down box.

imported>Andy: /* The Environ Machine */

2013-09-02T12:25:07Z

The Environ Machine

← Older revision		Revision as of 12:25, 2 September 2013
Line 115:		Line 115:
	We identify the ''Envir1Impl'' as an ''Environ Machine'',		We identify the ''Envir1Impl'' as an ''Environ Machine'',

	*~~Open the Tasking Section~~ in the Machine Editor		*Click on +, in the Machine Editor, to add a to add a Tasking Section,
	* Click on + to add a machine type.		* machine type.
	*Select ''Environ Machine'' in the drop down box.		*Select ''Environ Machine'' in the drop down box.