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
then
activeRegion -> size() = state.region -> size() and
activeRegion -> forAll( ar1, ar2 |
state.region->exists(ar1.region) and (ar1<> ar2 implies ar1.region <> ar2.region))
else
activeRegion -> isEmpty()
endif
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)))