Statemachine Animation Large Screenshot

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.