UML meta-model extension for state machine instance specification

This page presents all OCL invariants associated with the UML meta-model extension for managing state machine instances.

1) The active regions and states of an instance belong to the state machine whose instance is described.

A state machine instance is active when all its direct subregions are actives :

context StateMachineInstanceSpecification inv activeStateMachine:
activeRegion -> notEmpty() implies activeRegion -> collect(region) = stateMachine.region

A region is active when one (and only one) of its direct substates is active :

context ActiveRegion inv ownedActiveState:
region.subvertex -> includes(activeSubvertex.state)

An active region belongs either to a history configuration or to an active configuration :

context ActiveRegion inv oneowner:
activeInstance -> notEmpty() xor activeState -> notEmpty() xor historyInstance -> notEmpty()

2) An active composite state has each one of its regions which is active.

context ActiveState inv activeComposite:
if state.isComposite
   activeRegion -> size() = state.region -> size() and
   activeRegion -> forAll( ar1, ar2 |
      state.region->exists(ar1.region) and (ar1<> ar2 implies ar1.region <> ar2.region))
    activeRegion -> isEmpty()

3) An active submachine state owns a state machine instance which is active too and whose state machine is its submachine.

context ActiveState inv activeSubmachine:
state.isSubmachineState implies
   (activeSubmachine -> notEmpty() and activeSubmachine.stateMachine = state.submachine and activeSubmachine.activeRegion -> notEmpty())

4) A state machine only holds regions which own a history state as the root of a history configuration.

context StateMachineInstanceSpecification inv history:
historyConfiguration -> forAll(ar |
   ar.region.subvertex -> exists(v: Vertex |
      v.oclIsTypeOf(Pseudostate) and
      (v.oclAsType(Pseudostate).kind = #deepHistory or v.oclAsType(Pseudostate).kind = #shallowHistory)))