Statechart Diagram Semantics of AND-Refinements

Freeze

Unfreeze

+/N

-/N

when(Balance < 0)

when(Balance > 0)

H

Withdrawal(b)

/Balance := Balance - b

Balancing

/ Balance := 0

Open

/ Balance := 0

+/F

-/F

when(Balance < 0)

when(Balance > 0)

H*

Deposit(b) / Balance := Balance + b

Freeze

Unfreeze

Previous slide

Next slide

Back to first slide

View graphic version