Difference between revisions of "Refinement of Statemachines"
From Event-B
Jump to navigationJump to searchimported>Colin (New page: == 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 sta...) |
imported>Colin |
||
| Line 2: | Line 2: | ||
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. | ||
| + | |||
| + | [[Image:Atm1.jpg]] | ||
Revision as of 23:01, 17 June 2009
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.
