Example

A typical situation for using sub-asms is given, when the specification can be split up naturally into several sub-specifications each of which modeling a certain aspect of the overall specification.

In this case, the specification introduces the notion of a mode which can be used to structure the formalization. In the example, it is assumed, that the sub-asms update the value of the mode function to some value.