Refinement of Statemachines - Revision history

imported>Arran4 at 06:12, 8 September 2011

2011-09-08T06:12:10Z

← Older revision		Revision as of 06:12, 8 September 2011
Line 3:		Line 3:
	This example of an ATM (automated teller machine) shows the techniques used to make a refinement of a state machine. The example uses a machine-level state machine (i.e. not in a class). The state machines use the state-sets translation which, since there are no class instances, results in each state being represented by a boolean variable.		This example of an ATM (automated teller machine) shows the techniques used to make a refinement of a state machine. The example uses a machine-level state machine (i.e. not in a class). The state machines use the state-sets translation which, since there are no class instances, results in each state being represented by a boolean variable.

	a) Create a new UML-B project using the New-UML-B Project Wizard		# Create a new UML-B project using the New-UML-B Project Wizard
	b) Create a machine called ATM_A using the package diagram palette Machine tool		# Create a machine called ATM_A using the package diagram palette Machine tool
	c) Open its class diagram by selecting the machine and then clicking the button in the properties view (or using the pop-up menu).		# Open its class diagram by selecting the machine and then clicking the button in the properties view (or using the pop-up menu).
	d) Add a statemachine called atm_sm to the canvas using the diagram palette Statemachine tool.		# Add a statemachine called atm_sm to the canvas using the diagram palette Statemachine tool.
	c) Open the state machine and draw the state machine model shown in the diagram below using the statemachine diagram palette.		# Open the state machine and draw the state machine model shown in the diagram below using the statemachine diagram palette.

	The statemachine models an ATM which has 2 states, ''idle'' (not in use) and ''active''.		The statemachine models an ATM which has 2 states, ''idle'' (not in use) and ''active''.

imported>Mathieu: Category:User documentation Category:UML-B

2009-08-12T12:13:28Z

Category:User documentation Category:UML-B

← Older revision		Revision as of 12:13, 12 August 2009
Line 60:		Line 60:

	This completes the tutorial. The model should prove all the POs automatically. Examine the generated Event-B machines to see how the model is translated.		This completes the tutorial. The model should prove all the POs automatically. Examine the generated Event-B machines to see how the model is translated.

			[[Category:User documentation]]
			[[Category:UML-B]]

imported>Colin at 13:06, 19 June 2009

2009-06-19T13:06:53Z

← Older revision		Revision as of 13:06, 19 June 2009
Line 50:		Line 50:


	Notice that many of the transitions have the same name as transitions in the parent state machine. These transitions do not represent new events. Instead, they contribute more information about the transitions that have already been introduced to this refinement by the parent state machine. This is specified in the state machine model by an 'elaborates' property on the transition. The elaborates property forces the name of the elaborating transition to match that of the transition it elaborates. The transition must match the entry/exit characteristics of the parent transition it elaborates. For example, a transition that enters the parent state can only be elaborated by a transition from an initial state, an exit transition can only be elaborated by a transition to a final state and a self-loop transition can only be elaborated by a transition between states that are neither initial nor final. These well-formedness criteria are enforced by validation checks built into the drawing tool.		Notice that many of the transitions have the same name as transitions in the parent state machine. These transitions do not represent new events. Instead, they contribute more information about the transitions that have already been introduced to this refinement by the parent state machine. This is specified in the state machine model by an 'elaborates' property on the transition. The elaborates property forces the name of the elaborating transition to match that of the transition it elaborates. The transition must match the entry/exit characteristics of the parent transition it elaborates. For example, a transition that enters the parent state can only be elaborated by a transition from an initial state, an exit transition can only be elaborated by a transition to a final state and a self-loop transition can only be elaborated by a transition between states that are neither initial nor final. (In the last case the elaborating transition can either be another self-loop on one of the nested states, or it can be a transition between two different nested states). These well-formedness criteria are enforced by validation checks built into the drawing tool.

	a) Draw a transition from the initial state to state ''awaitingPin''.		a) Draw a transition from the initial state to state ''awaitingPin''.

imported>Colin at 08:57, 19 June 2009

2009-06-19T08:57:42Z

← Older revision		Revision as of 08:57, 19 June 2009
Line 50:		Line 50:


	Notice that many of the transitions have the same name as transitions in the parent state machine. These transitions do not represent new events. Instead, they contribute more information about the transitions that have already been introduced to this refinement by the parent state machine. This is specified in the state machine model by an 'elaborates' property on the transition. The elaborates property forces the name of the elaborating transition to match that of the transition it elaborates. The transition must match the entry/exit characteristics of the parent transition it elaborates. For example, a transition that enters the parent state can only be elaborated by a transition from an initial state, an exit transition can only be elaborated by a transition to a final state and a self-loop transition can only be elaborated by a transition between states that are neither initial nor final. These well-formedness criteria are enforced by validation ~~chacks~~ built into the drawing tool.		Notice that many of the transitions have the same name as transitions in the parent state machine. These transitions do not represent new events. Instead, they contribute more information about the transitions that have already been introduced to this refinement by the parent state machine. This is specified in the state machine model by an 'elaborates' property on the transition. The elaborates property forces the name of the elaborating transition to match that of the transition it elaborates. The transition must match the entry/exit characteristics of the parent transition it elaborates. For example, a transition that enters the parent state can only be elaborated by a transition from an initial state, an exit transition can only be elaborated by a transition to a final state and a self-loop transition can only be elaborated by a transition between states that are neither initial nor final. These well-formedness criteria are enforced by validation checks built into the drawing tool.

	a) Draw a transition from the initial state to state ''awaitingPin''.		a) Draw a transition from the initial state to state ''awaitingPin''.
	b) Do not name it but instead select the transition called ''insertCard'' from the combo box on its properties view. Its name should automatically become the same as the transition it elaborates.		b) Do not name it but instead select the transition called ''insertCard'' from the combo box on its properties view. Its name should automatically become the same as the transition it elaborates.
	c) Repeat this process for the transitions ''ejectCardWithoutCash'', ''Transaction'' and ''ejectCardWithCash'', making sure they elaborate the transition with the same name from the parent. (Notice that each parent transition can only be elaborated once).		c) Repeat this process for the transitions ''ejectCardWithoutCash'', ''Transaction'' and ''ejectCardWithCash'', making sure they elaborate the transition with the same name from the parent.
			(Notice that each parent transition can only be elaborated once).
	d) The transition ''pinEntered'' is a new transition and does not elaborate anything. Instead, enter its name using the name property text box.		d) The transition ''pinEntered'' is a new transition and does not elaborate anything. Instead, enter its name using the name property text box.


			This completes the tutorial. The model should prove all the POs automatically. Examine the generated Event-B machines to see how the model is translated.

imported>Colin at 18:42, 18 June 2009

2009-06-18T18:42:47Z

← Older revision		Revision as of 18:42, 18 June 2009
Line 1:		Line 1:
			Return to [[UML-B]]

	This example of an ATM (automated teller machine) shows the techniques used to make a refinement of a state machine. The example uses a machine-level state machine (i.e. not in a class). The state machines use the state-sets translation which, since there are no class instances, results in each state being represented by a boolean variable.		This example of an ATM (automated teller machine) shows the techniques used to make a refinement of a state machine. The example uses a machine-level state machine (i.e. not in a class). The state machines use the state-sets translation which, since there are no class instances, results in each state being represented by a boolean variable.

imported>Colin: /* Refinement of Statemachines */

2009-06-18T18:27:09Z

Refinement of Statemachines

← Older revision		Revision as of 18:27, 18 June 2009
Line 1:		Line 1:
	~~== Refinement of Statemachines ==~~



	This example of an ATM (automated teller machine) shows the techniques used to make a refinement of a state machine. The example uses a machine-level state machine (i.e. not in a class). The state machines use the state-sets translation which, since there are no class instances, results in each state being represented by a boolean variable.		This example of an ATM (automated teller machine) shows the techniques used to make a refinement of a state machine. The example uses a machine-level state machine (i.e. not in a class). The state machines use the state-sets translation which, since there are no class instances, results in each state being represented by a boolean variable.

imported>Colin: /* Refinement of Statemachines */

2009-06-18T18:19:00Z

Refinement of Statemachines

← Older revision		Revision as of 18:19, 18 June 2009
Line 2:		Line 2:


	~~INCOMPLETE - UNDER CONSTRUCTION~~

	This example of an ATM (automated teller machine) shows the techniques used to make a refinement of a state machine. The example uses a machine-level state machine (i.e. not in a class). The state machines use the state-sets translation which, since there are no class instances, results in each state being represented by a boolean variable.		This example of an ATM (automated teller machine) shows the techniques used to make a refinement of a state machine. The example uses a machine-level state machine (i.e. not in a class). The state machines use the state-sets translation which, since there are no class instances, results in each state being represented by a boolean variable.
Line 55:		Line 54:
	Notice that many of the transitions have the same name as transitions in the parent state machine. These transitions do not represent new events. Instead, they contribute more information about the transitions that have already been introduced to this refinement by the parent state machine. This is specified in the state machine model by an 'elaborates' property on the transition. The elaborates property forces the name of the elaborating transition to match that of the transition it elaborates. The transition must match the entry/exit characteristics of the parent transition it elaborates. For example, a transition that enters the parent state can only be elaborated by a transition from an initial state, an exit transition can only be elaborated by a transition to a final state and a self-loop transition can only be elaborated by a transition between states that are neither initial nor final. These well-formedness criteria are enforced by validation chacks built into the drawing tool.		Notice that many of the transitions have the same name as transitions in the parent state machine. These transitions do not represent new events. Instead, they contribute more information about the transitions that have already been introduced to this refinement by the parent state machine. This is specified in the state machine model by an 'elaborates' property on the transition. The elaborates property forces the name of the elaborating transition to match that of the transition it elaborates. The transition must match the entry/exit characteristics of the parent transition it elaborates. For example, a transition that enters the parent state can only be elaborated by a transition from an initial state, an exit transition can only be elaborated by a transition to a final state and a self-loop transition can only be elaborated by a transition between states that are neither initial nor final. These well-formedness criteria are enforced by validation chacks built into the drawing tool.

	a) Draw a transition from the initial state to state ''~~validating~~'' ....~~tbd~~		a) Draw a transition from the initial state to state ''awaitingPin''.
			b) Do not name it but instead select the transition called ''insertCard'' from the combo box on its properties view. Its name should automatically become the same as the transition it elaborates.
			c) Repeat this process for the transitions ''ejectCardWithoutCash'', ''Transaction'' and ''ejectCardWithCash'', making sure they elaborate the transition with the same name from the parent. (Notice that each parent transition can only be elaborated once).
			d) The transition ''pinEntered'' is a new transition and does not elaborate anything. Instead, enter its name using the name property text box.

imported>Colin: /* Refinement of Statemachines */

2009-06-18T15:55:14Z

Refinement of Statemachines

← Older revision		Revision as of 15:55, 18 June 2009
Line 46:		Line 46:
	b) In the properties view for the new state machine, set the translation kind to ''state sets''.		b) In the properties view for the new state machine, set the translation kind to ''state sets''.
	c) Open the new state machine's diagram by right-clicking on it and selecting 'open diagram'.		c) Open the new state machine's diagram by right-clicking on it and selecting 'open diagram'.
	d) Draw the state machine model ~~shown~~ below.		d) Draw the state machine states, initial state and final states shown in the model below. (The transitions are discussed in the next step)


	[[Image:Atm4.jpg]]		[[Image:Atm4.jpg]]



			Notice that many of the transitions have the same name as transitions in the parent state machine. These transitions do not represent new events. Instead, they contribute more information about the transitions that have already been introduced to this refinement by the parent state machine. This is specified in the state machine model by an 'elaborates' property on the transition. The elaborates property forces the name of the elaborating transition to match that of the transition it elaborates. The transition must match the entry/exit characteristics of the parent transition it elaborates. For example, a transition that enters the parent state can only be elaborated by a transition from an initial state, an exit transition can only be elaborated by a transition to a final state and a self-loop transition can only be elaborated by a transition between states that are neither initial nor final. These well-formedness criteria are enforced by validation chacks built into the drawing tool.

			a) Draw a transition from the initial state to state ''validating'' ....tbd

imported>Colin: /* Refinement of Statemachines */

2009-06-18T12:31:23Z

Refinement of Statemachines

← Older revision		Revision as of 12:31, 18 June 2009
Line 42:		Line 42:

	Now we need to add some detail to show when each of these two eject card options are taken. We do this by adding a nested statemachine in the next step.		Now we need to add some detail to show when each of these two eject card options are taken. We do this by adding a nested statemachine in the next step.

			a) Using the 'State Features-Statemachine' palette option, add a nested state machine called ''active_sm'' to the state, ''active''.
			b) In the properties view for the new state machine, set the translation kind to ''state sets''.
			c) Open the new state machine's diagram by right-clicking on it and selecting 'open diagram'.
			d) Draw the state machine model shown below.


			[[Image:Atm4.jpg]]

imported>Colin: /* Refinement of Statemachines */

2009-06-18T11:33:52Z

Refinement of Statemachines

← Older revision		Revision as of 11:33, 18 June 2009
Line 32:		Line 32:
	b) Draw a new transition from state ''active'' to state ''idle''.		b) Draw a new transition from state ''active'' to state ''idle''.
	c) With the new transition still selected, enter ''ejectCardWithoutCash'' as its name in the properties view.		c) With the new transition still selected, enter ''ejectCardWithoutCash'' as its name in the properties view.
	d) Using the ~~refines selection box~~ in the properties view, ~~set its refines property to~~ ''ejectCard''.		d) Using the 'Add Refined Event/Transition' button in the 'Refines' tab of the properties view, add ''ejectCard'' as a refined transition.


	The refined state machine should now look something like the one below ~~but without the nested statemachine contained in state ''active''~~. ~~We will add this nested statemachine in~~ the ~~next step~~.		The refined state machine should now look something like the one below. This screen-shot shows step d) where the event refinement relationship is being set.


	[[Image:Atm3.jpg]]		[[Image:Atm3.jpg]]


			Now we need to add some detail to show when each of these two eject card options are taken. We do this by adding a nested statemachine in the next step.