Statemachine Animation Large Screenshot: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Colin New page: Image:SmAnimScreenshot.png |
imported>Colin No edit summary |
||
| Line 1: | Line 1: | ||
The screenshot below shows a statemachine (top left) and its refinement (top right) being animated in parallel with the nested statemachines (bottom left and right) that are contained in the refined states. Two class instances are currently active; one models an ATM that is not available (e.g. in maintenace) and the other is in the process of validating a card. Transitions that are enabled for one or other of the class instances are emboldened. (The instance to be used when a transition is fired is selected when the transitions is clicked upon). Note that the ancillary views around the diagrams are ProB views which can also be used during the animation. | |||
[[Image:SmAnimScreenshot.png]] | [[Image:SmAnimScreenshot.png]] | ||
Latest revision as of 15:12, 28 January 2010
The screenshot below shows a statemachine (top left) and its refinement (top right) being animated in parallel with the nested statemachines (bottom left and right) that are contained in the refined states. Two class instances are currently active; one models an ATM that is not available (e.g. in maintenace) and the other is in the process of validating a card. Transitions that are enabled for one or other of the class instances are emboldened. (The instance to be used when a transition is fired is selected when the transitions is clicked upon). Note that the ancillary views around the diagrams are ProB views which can also be used during the animation.
