Refinement of Statemachines: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Colin
imported>Colin
Line 6: Line 6:
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.


create a machine called ATM_A, open its class diagram and then add a statemachine called atm_sm to the canvas. Open the state machine and draw the state machine shown in the diagram below.
create a machine called ATM_A
open its class diagram and then add a statemachine called atm_sm to the canvas.  
Open the state machine and draw the state machine shown in the diagram below.  
 
The statemachine models an ATM which has 2 states, ''idle'' (not in use) and ''active''.
The ATM starts off in the state ''idle''. When a card is inserted, represented by the transition ''insertCard'', it becomes ''active''. While it is ''active''  transactions can occur (transition ''transaction''). At some time (after 0 or more transactions) the ATM will return to the ''idle'' state, ejecting the card as it does so (transition ''ejectCard''). The model is accurate but it leaves out many important details.
 


[[Image:Atm1.jpg]]
[[Image:Atm1.jpg]]


Return to the package diagram, select the machine, ATM_M, and click on "Make a refinement of this Machine..."
Return to the package diagram, select the machine, ATM_M, and click on "Make a refinement of this Machine..."
Call the refinement ATM_R.
Name the refinement ATM_R.
 


[[Image:Atm2.jpg]]
[[Image:Atm2.jpg]]




Open the class diagram of ATM_R and you should find a 'refined state machine' which is a clone of 'atm_sm'. Open the state machine.
Open the class diagram of ATM_R and you will find a 'refined state machine' which is a clone of 'atm_sm'. Open the state machine. Notice that the transitions refine their counterparts in the abstract level.
At the moment the refinement is a valid refinement because it is an exact copy but it doesn't make any progress. We will make the refinement more interesting by modifying the state machine and introducing more detail. The detail that we will introduce is that an ATM ''active'' session can result in ejecting the card with or without cash. We will also start to introduce some details of the process involved in a transaction. Firstly, we need to split the transition, ''ejectCard'' into two transitions representing the two outcomes. Change the name of the

Revision as of 09:33, 18 June 2009

Refinement of Statemachines

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.

create a machine called ATM_A
open its class diagram and then add a statemachine called atm_sm to the canvas. 
Open the state machine and draw the state machine shown in the diagram below. 

The statemachine models an ATM which has 2 states, idle (not in use) and active. The ATM starts off in the state idle. When a card is inserted, represented by the transition insertCard, it becomes active. While it is active transactions can occur (transition transaction). At some time (after 0 or more transactions) the ATM will return to the idle state, ejecting the card as it does so (transition ejectCard). The model is accurate but it leaves out many important details.



Return to the package diagram, select the machine, ATM_M, and click on "Make a refinement of this Machine..." Name the refinement ATM_R.



Open the class diagram of ATM_R and you will find a 'refined state machine' which is a clone of 'atm_sm'. Open the state machine. Notice that the transitions refine their counterparts in the abstract level. At the moment the refinement is a valid refinement because it is an exact copy but it doesn't make any progress. We will make the refinement more interesting by modifying the state machine and introducing more detail. The detail that we will introduce is that an ATM active session can result in ejecting the card with or without cash. We will also start to introduce some details of the process involved in a transaction. Firstly, we need to split the transition, ejectCard into two transitions representing the two outcomes. Change the name of the