Signature: transitions_outgoing() : Boolean;
Description: All transitions outgoing a fork vertex must target states in different regions of an orthogonal state.
Expression: (self.kind = #fork) implies self.outgoing->forAll (t1, t2 | t1<>t2 implies (self.stateMachine.LCA(t1.target, t2.target).container.isOrthogonal))

Signature: transitions_incoming() : Boolean;
Description: All transitions incoming a join vertex must originate in different regions of an orthogonal state.
Expression: (self.kind = #join) implies self.incoming->forAll (t1, t2 | t1<>t2 implies (self.stateMachine.LCA(t1.source, t2.source).container.isOrthogonal))

Signature: outgoing_from_initial() : Boolean;
Description: The outgoing transition from and initial vertex may have a behavior, but not a trigger or a guard.
Expression: (self.kind = #initial) implies (self.outgoing.guard->isEmpty() and self.outgoing.trigger->isEmpty())

Signature: junction_vertex() : Boolean;
Description: In a complete statemachine, a junction vertex must have at least one incoming and one outgoing transition.
The OCL used here is not normative.
Editor's notes: size() not size.
Expression:(self.kind = #junction) implies ((self.incoming->size() >= 1) and (self.outgoing->size() >= 1))
Original: (self.kind = #junction) implies ((self.incoming->size >= 1) and (self.outgoing->size >= 1))

Signature: join_vertex() : Boolean;
Description: In a complete statemachine, a join vertex must have at least two incoming transitions and exactly one outgoing transition.
The OCL used here is not normative.
Editor's notes: size() not size.
Expression:(self.kind = #join) implies ((self.outgoing->size() = 1) and (self.incoming->size() >= 2))
Original: (self.kind = #join) implies ((self.outgoing->size = 1) and (self.incoming->size >= 2))

Signature: initial_vertex() : Boolean;
Description: An initial vertex can have at most one outgoing transition.
Expression: (self.kind = #initial) implies (self.outgoing->size <= 1)

Signature: history_vertices() : Boolean;
Description: History vertices can have at most one outgoing transition.
The OCL used here is not normative.
Editor's notes: size() not size.
Expression:((self.kind = #deepHistory) or (self.kind = #shallowHistory)) implies (self.outgoing->size() <= 1)
Original: ((self.kind = #deepHistory) or (self.kind = #shallowHistory)) implies (self.outgoing->size <= 1)

Signature: fork_vertex() : Boolean;
Description: In a complete statemachine, a fork vertex must have at least two outgoing transitions and exactly one incoming transition.
The OCL used here is not normative.
Editor's notes: size() not size.
Expression:(self.kind = #fork) implies ((self.incoming->size() = 1) and (self.outgoing->size() >= 2))
Original: (self.kind = #fork) implies ((self.incoming->size = 1) and (self.outgoing->size >= 2))

Signature: choice_vertex() : Boolean;
Description: In a complete statemachine, a choice vertex must have at least one incoming and one outgoing transition.
The OCL used here is not normative.
Editor's notes: size() not size.
Expression:(self.kind = #choice) implies ((self.incoming->size() >= 1) and (self.outgoing->size() >= 1))
Original: (self.kind = #choice) implies ((self.incoming->size >= 1) and (self.outgoing->size >= 1))

Operations:

No additional operations.

Send questions or comments to [email protected].