Name: maximum_one_parameter_node
Related element: Activity
Description: A Parameter with direction other than inout must have exactly one ActivityParameterNode in an Activity.
Language: OCL
Formal wording:
ownedParameter->forAll(p |
p.direction <> ParameterDirectionKind::inout implies node->select(
oclIsKindOf(ActivityParameterNode) and oclAsType(ActivityParameterNode).parameter = p)->size()= 1)
Name: maximum_two_parameter_nodes
Related element: Activity
Description: A Parameter with direction inout must have exactly two ActivityParameterNodes in an Activity, at most one with incoming ActivityEdges and at most one with outgoing ActivityEdges.
Language: OCL
Formal wording:
ownedParameter->forAll(p |
p.direction = ParameterDirectionKind::inout implies
let associatedNodes : Set(ActivityNode) = node->select(
oclIsKindOf(ActivityParameterNode) and oclAsType(ActivityParameterNode).parameter = p) in
associatedNodes->size()=2 and
associatedNodes->select(incoming->notEmpty())->size()<=1 and
associatedNodes->select(outgoing->notEmpty())->size()<=1
)
Name: source_and_target
Related element: ActivityEdge
Description: If an ActivityEdge is directly owned by an Activity, then its source and target must be directly or indirectly contained in the same Activity.
Language: OCL
Formal wording:
activity<>null implies source.containingActivity() = activity and target.containingActivity() = activity
Name: spec
Related element: ActivityEdge-isConsistentWith
Language: OCL
Formal wording:
result = (redefiningElement.oclIsKindOf(ActivityEdge))
Name: nodes_and_edges
Related element: ActivityGroup
Description: All containedNodes and containeEdges of an ActivityGroup must be in the same Activity as the group.
Language: OCL
Formal wording:
containedNode->forAll(activity = self.containingActivity()) and containedEdge->forAll(activity = self.containingActivity())
Name: not_contained
Related element: ActivityGroup
Description: No containedNode or containedEdge of an ActivityGroup may be contained by its subgroups or its superGroups, transitively.
Language: OCL
Formal wording:
subgroup->closure(subgroup).containedNode->excludesAll(containedNode) and superGroup->closure(superGroup).containedNode->excludesAll(containedNode) and subgroup->closure(subgroup).containedEdge->excludesAll(containedEdge) and superGroup->closure(superGroup).containedEdge->excludesAll(containedEdge)
Name: spec
Related element: ActivityGroup-containingActivity
Language: OCL
Formal wording:
result = (if superGroup<>null then superGroup.containingActivity() else inActivity endif)
Name: spec
Related element: ActivityNode-containingActivity
Language: OCL
Formal wording:
result = (if inStructuredNode<>null then inStructuredNode.containingActivity() else activity endif)
Name: spec
Related element: ActivityNode-isConsistentWith
Language: OCL
Formal wording:
result = (redefiningElement.oclIsKindOf(ActivityNode))
Name: no_outgoing_edges
Related element: ActivityParameterNode
Description: An ActivityParameterNode with no outgoing ActivityEdges and one or more incoming ActivityEdges must have a parameter with direction out, inout, or return.
Language: OCL
Formal wording:
(incoming->notEmpty() and outgoing->isEmpty()) implies (parameter.direction = ParameterDirectionKind::out or parameter.direction = ParameterDirectionKind::inout or parameter.direction = ParameterDirectionKind::return)
Name: has_parameters
Related element: ActivityParameterNode
Description: The parameter of an ActivityParameterNode must be from the containing Activity.
Language: OCL
Formal wording:
activity.ownedParameter->includes(parameter)
Name: same_type
Related element: ActivityParameterNode
Description: The type of an ActivityParameterNode is the same as the type of its parameter.
Language: OCL
Formal wording:
type = parameter.type
Name: no_incoming_edges
Related element: ActivityParameterNode
Description: An ActivityParameterNode with no incoming ActivityEdges and one or more outgoing ActivityEdges must have a parameter with direction in or inout.
Language: OCL
Formal wording:
(outgoing->notEmpty() and incoming->isEmpty()) implies (parameter.direction = ParameterDirectionKind::_'in' or parameter.direction = ParameterDirectionKind::inout)
Name: no_edges
Related element: ActivityParameterNode
Description: An ActivityParameterNode may have all incoming ActivityEdges or all outgoing ActivityEdges, but it must not have both incoming and outgoing ActivityEdges.
Language: OCL
Formal wording:
incoming->isEmpty() or outgoing->isEmpty()
Name: represents_classifier
Related element: ActivityPartition
Description: If a non-external ActivityPartition represents a Classifier and has a superPartition, then the superPartition must represent a Classifier, and the Classifier of the subpartition must be nested (nestedClassifier or ownedBehavior) in the Classifier represented by the superPartition, or be at the contained end of a composition Association with the Classifier represented by the superPartition.
Language: OCL
Formal wording:
(not isExternal and represents.oclIsKindOf(Classifier) and superPartition->notEmpty()) implies
(
let representedClassifier : Classifier = represents.oclAsType(Classifier) in
superPartition.represents.oclIsKindOf(Classifier) and
let representedSuperClassifier : Classifier = superPartition.represents.oclAsType(Classifier) in
(representedSuperClassifier.oclIsKindOf(BehavioredClassifier) and representedClassifier.oclIsKindOf(Behavior) and
representedSuperClassifier.oclAsType(BehavioredClassifier).ownedBehavior->includes(representedClassifier.oclAsType(Behavior)))
or
(representedSuperClassifier.oclIsKindOf(Class) and representedSuperClassifier.oclAsType(Class).nestedClassifier->includes(representedClassifier))
or
(Association.allInstances()->exists(a | a.memberEnd->exists(end1 | end1.isComposite and end1.type = representedClassifier and
a.memberEnd->exists(end2 | end1<>end2 and end2.type = representedSuperClassifier))))
)
Name: represents_property_and_is_contained
Related element: ActivityPartition
Description: If an ActivityPartition represents a Property and has a superPartition, then the Property must be of a Classifier represented by the superPartition, or of a Classifier that is the type of a Property represented by the superPartition.
Language: OCL
Formal wording:
(represents.oclIsKindOf(Property) and superPartition->notEmpty()) implies ( (superPartition.represents.oclIsKindOf(Classifier) and represents.owner = superPartition.represents) or (superPartition.represents.oclIsKindOf(Property) and represents.owner = superPartition.represents.oclAsType(Property).type) )
Name: represents_property
Related element: ActivityPartition
Description: If an ActivityPartition represents a Property and has a superPartition representing a Classifier, then all the other non-external subpartitions of the superPartition must represent Properties directly owned by the same Classifier.
Language: OCL
Formal wording:
(represents.oclIsKindOf(Property) and superPartition->notEmpty() and superPartition.represents.oclIsKindOf(Classifier)) implies
(
let representedClassifier : Classifier = superPartition.represents.oclAsType(Classifier)
in
superPartition.subpartition->reject(isExternal)->forAll(p |
p.represents.oclIsKindOf(Property) and p.owner=representedClassifier)
)
Name: dimension_not_contained
Related element: ActivityPartition
Description: An ActvivityPartition with isDimension = true may not be contained by another ActivityPartition.
Language: OCL
Formal wording:
isDimension implies superPartition->isEmpty()
Name: object_nodes
Related element: ControlFlow
Description: ControlFlows may not have ObjectNodes at either end, except for ObjectNodes with control type.
Language: OCL
Formal wording:
(source.oclIsKindOf(ObjectNode) implies source.oclAsType(ObjectNode).isControlType) and (target.oclIsKindOf(ObjectNode) implies target.oclAsType(ObjectNode).isControlType)
Name: zero_input_parameters
Related element: DecisionNode
Description: If the DecisionNode has no decisionInputFlow and an incoming ControlFlow, then any decisionInput Behavior has no in parameters.
Language: OCL
Formal wording:
(decisionInput<>null and decisionInputFlow=null and incoming->exists(oclIsKindOf(ControlFlow))) implies decisionInput.inputParameters()->isEmpty()
Name: edges
Related element: DecisionNode
Description: The ActivityEdges incoming to and outgoing from a DecisionNode, other than the decisionInputFlow (if any), must be either all ObjectFlows or all ControlFlows.
Language: OCL
Formal wording:
let allEdges: Set(ActivityEdge) = incoming->union(outgoing) in let allRelevantEdges: Set(ActivityEdge) = if decisionInputFlow->notEmpty() then allEdges->excluding(decisionInputFlow) else allEdges endif in allRelevantEdges->forAll(oclIsKindOf(ControlFlow)) or allRelevantEdges->forAll(oclIsKindOf(ObjectFlow))
Name: decision_input_flow_incoming
Related element: DecisionNode
Description: The decisionInputFlow of a DecisionNode must be an incoming ActivityEdge of the DecisionNode.
Language: OCL
Formal wording:
incoming->includes(decisionInputFlow)
Name: two_input_parameters
Related element: DecisionNode
Description: If the DecisionNode has a decisionInputFlow and an second incoming ObjectFlow, then any decisionInput has two in Parameters, the first of which has a type that is the same as or a supertype of the type of object tokens offered on the non-decisionInputFlow and the second of which has a type that is the same as or a supertype of the type of object tokens offered on the decisionInputFlow.
Language: OCL
Formal wording:
(decisionInput<>null and decisionInputFlow<>null and incoming->forAll(oclIsKindOf(ObjectFlow))) implies decisionInput.inputParameters()->size()=2
Name: incoming_outgoing_edges
Related element: DecisionNode
Description: A DecisionNode has one or two incoming ActivityEdges and at least one outgoing ActivityEdge.
Language: OCL
Formal wording:
(incoming->size() = 1 or incoming->size() = 2) and outgoing->size() > 0
Name: incoming_control_one_input_parameter
Related element: DecisionNode
Description: If the DecisionNode has a decisionInputFlow and an incoming ControlFlow, then any decisionInput Behavior has one in Parameter whose type is the same as or a supertype of the type of object tokens offered on the decisionInputFlow.
Language: OCL
Formal wording:
(decisionInput<>null and decisionInputFlow<>null and incoming->exists(oclIsKindOf(ControlFlow))) implies decisionInput.inputParameters()->size()=1
Name: parameters
Related element: DecisionNode
Description: A decisionInput Behavior has no out parameters, no inout parameters, and one return parameter.
Language: OCL
Formal wording:
decisionInput<>null implies
(decisionInput.ownedParameter->forAll(par |
par.direction <> ParameterDirectionKind::out and
par.direction <> ParameterDirectionKind::inout ) and
decisionInput.ownedParameter->one(par |
par.direction <> ParameterDirectionKind::return))
Name: incoming_object_one_input_parameter
Related element: DecisionNode
Description: If the DecisionNode has no decisionInputFlow and an incoming ObjectFlow, then any decisionInput Behavior has one in Parameter whose type is the same as or a supertype of the type of object tokens offered on the incoming ObjectFlow.
Language: OCL
Formal wording:
(decisionInput<>null and decisionInputFlow=null and incoming->forAll(oclIsKindOf(ObjectFlow))) implies decisionInput.inputParameters()->size()=1
Name: handler_body_edges
Related element: ExceptionHandler
Description: The handlerBody has no incoming or outgoing ActivityEdges and the exceptionInput has no incoming ActivityEdges.
Language: OCL
Formal wording:
handlerBody.incoming->isEmpty() and handlerBody.outgoing->isEmpty() and exceptionInput.incoming->isEmpty()
Name: output_pins
Related element: ExceptionHandler
Description: If the protectedNode is an Action with OutputPins, then the handlerBody must also be an Action with the same number of OutputPins, which are compatible in type, ordering, and multiplicity to those of the protectedNode.
Language: OCL
Formal wording:
(protectedNode.oclIsKindOf(Action) and protectedNode.oclAsType(Action).output->notEmpty()) implies
(
handlerBody.oclIsKindOf(Action) and
let protectedNodeOutput : OrderedSet(OutputPin) = protectedNode.oclAsType(Action).output,
handlerBodyOutput : OrderedSet(OutputPin) = handlerBody.oclAsType(Action).output in
protectedNodeOutput->size() = handlerBodyOutput->size() and
Sequence{1..protectedNodeOutput->size()}->forAll(i |
handlerBodyOutput->at(i).type.conformsTo(protectedNodeOutput->at(i).type) and
handlerBodyOutput->at(i).isOrdered=protectedNodeOutput->at(i).isOrdered and
handlerBodyOutput->at(i).compatibleWith(protectedNodeOutput->at(i)))
)
Name: one_input
Related element: ExceptionHandler
Description: The handlerBody is an Action with one InputPin, and that InputPin is the same as the exceptionInput.
Language: OCL
Formal wording:
handlerBody.oclIsKindOf(Action) and let inputs: OrderedSet(InputPin) = handlerBody.oclAsType(Action).input in inputs->size()=1 and inputs->first()=exceptionInput
Name: edge_source_target
Related element: ExceptionHandler
Description: An ActivityEdge that has a source within the handlerBody of an ExceptionHandler must have its target in the handlerBody also, and vice versa.
Language: OCL
Formal wording:
let nodes:Set(ActivityNode) = handlerBody.oclAsType(Action).allOwnedNodes() in nodes.outgoing->forAll(nodes->includes(target)) and nodes.incoming->forAll(nodes->includes(source))
Name: handler_body_owner
Related element: ExceptionHandler
Description: The handlerBody must have the same owner as the protectedNode.
Language: OCL
Formal wording:
handlerBody.owner=protectedNode.owner
Name: exception_input_type
Related element: ExceptionHandler
Description: The exceptionInput must either have no type or every exceptionType must conform to the exceptionInput type.
Language: OCL
Formal wording:
exceptionInput.type=null or exceptionType->forAll(conformsTo(exceptionInput.type.oclAsType(Classifier)))
Name: no_outgoing_edges
Related element: FinalNode
Description: A FinalNode has no outgoing ActivityEdges.
Language: OCL
Formal wording:
outgoing->isEmpty()
Name: edges
Related element: ForkNode
Description: The ActivityEdges incoming to and outgoing from a ForkNode must be either all ObjectFlows or all ControlFlows.
Language: OCL
Formal wording:
let allEdges : Set(ActivityEdge) = incoming->union(outgoing) in allEdges->forAll(oclIsKindOf(ControlFlow)) or allEdges->forAll(oclIsKindOf(ObjectFlow))
Name: one_incoming_edge
Related element: ForkNode
Description: A ForkNode has one incoming ActivityEdge.
Language: OCL
Formal wording:
incoming->size()=1
Name: no_incoming_edges
Related element: InitialNode
Description: An InitialNode has no incoming ActivityEdges.
Language: OCL
Formal wording:
incoming->isEmpty()
Name: control_edges
Related element: InitialNode
Description: All the outgoing ActivityEdges from an InitialNode must be ControlFlows.
Language: OCL
Formal wording:
outgoing->forAll(oclIsKindOf(ControlFlow))
Name: interrupting_edges
Related element: InterruptibleActivityRegion
Description: The interruptingEdges of an InterruptibleActivityRegion must have their source in the region and their target outside the region, but within the same Activity containing the region.
Language: OCL
Formal wording:
interruptingEdge->forAll(edge | node->includes(edge.source) and node->excludes(edge.target) and edge.target.containingActivity() = inActivity)
Name: one_outgoing_edge
Related element: JoinNode
Description: A JoinNode has one outgoing ActivityEdge.
Language: OCL
Formal wording:
outgoing->size() = 1
Name: incoming_object_flow
Related element: JoinNode
Description: If one of the incoming ActivityEdges of a JoinNode is an ObjectFlow, then its outgoing ActivityEdge must be an ObjectFlow. Otherwise its outgoing ActivityEdge must be a ControlFlow.
Language: OCL
Formal wording:
if incoming->exists(oclIsKindOf(ObjectFlow)) then outgoing->forAll(oclIsKindOf(ObjectFlow)) else outgoing->forAll(oclIsKindOf(ControlFlow)) endif
Name: one_outgoing_edge
Related element: MergeNode
Description: A MergeNode has one outgoing ActivityEdge.
Language: OCL
Formal wording:
outgoing->size()=1
Name: edges
Related element: MergeNode
Description: The ActivityEdges incoming to and outgoing from a MergeNode must be either all ObjectFlows or all ControlFlows.
Language: OCL
Formal wording:
let allEdges : Set(ActivityEdge) = incoming->union(outgoing) in allEdges->forAll(oclIsKindOf(ControlFlow)) or allEdges->forAll(oclIsKindOf(ObjectFlow))
Name: input_and_output_parameter
Related element: ObjectFlow
Description: A selection Behavior has one input Parameter and one output Parameter. The input Parameter must have the same as or a supertype of the type of the source ObjectNode, be non-unique and have multiplicity 0..*. The output Parameter must be the same or a subtype of the type of source ObjectNode. The Behavior cannot have side effects.
Language: OCL
Formal wording:
selection<>null implies selection.inputParameters()->size()=1 and selection.inputParameters()->forAll(not isUnique and is(0,*)) and selection.outputParameters()->size()=1
Name: no_executable_nodes
Related element: ObjectFlow
Description: ObjectFlows may not have ExecutableNodes at either end.
Language: OCL
Formal wording:
not (source.oclIsKindOf(ExecutableNode) or target.oclIsKindOf(ExecutableNode))
Name: transformation_behavior
Related element: ObjectFlow
Description: A transformation Behavior has one input Parameter and one output Parameter. The input Parameter must be the same as or a supertype of the type of object token coming from the source end. The output Parameter must be the same or a subtype of the type of object token expected downstream. The Behavior cannot have side effects.
Language: OCL
Formal wording:
transformation<>null implies transformation.inputParameters()->size()=1 and transformation.outputParameters()->size()=1
Name: selection_behavior
Related element: ObjectFlow
Description: An ObjectFlow may have a selection Behavior only if it has an ObjectNode as its source.
Language: OCL
Formal wording:
selection<>null implies source.oclIsKindOf(ObjectNode)
Name: compatible_types
Related element: ObjectFlow
Description: ObjectNodes connected by an ObjectFlow, with optionally intervening ControlNodes, must have compatible types. In particular, the downstream ObjectNode type must be the same or a supertype of the upstream ObjectNode type.
Name: same_upper_bounds
Related element: ObjectFlow
Description: ObjectNodes connected by an ObjectFlow, with optionally intervening ControlNodes, must have the same upperBounds.
Name: target
Related element: ObjectFlow
Description: An ObjectFlow with a constant weight may not target an ObjectNode, with optionally intervening ControlNodes, that has an upper bound less than the weight.
Name: is_multicast_or_is_multireceive
Related element: ObjectFlow
Description: isMulticast and isMultireceive cannot both be true.
Language: OCL
Formal wording:
not (isMulticast and isMultireceive)
Name: input_output_parameter
Related element: ObjectNode
Description: A selection Behavior has one input Parameter and one output Parameter. The input Parameter must have the same type as or a supertype of the type of ObjectNode, be non-unique, and have multiplicity 0..*. The output Parameter must be the same or a subtype of the type of ObjectNode. The Behavior cannot have side effects.
Language: OCL
Formal wording:
selection<>null implies selection.inputParameters()->size()=1 and selection.inputParameters()->forAll(p | not p.isUnique and p.is(0,*) and self.type.conformsTo(p.type)) and selection.outputParameters()->size()=1 and selection.inputParameters()->forAll(p | self.type.conformsTo(p.type))
Name: selection_behavior
Related element: ObjectNode
Description: If an ObjectNode has a selection Behavior, then the ordering of the object node is ordered, and vice versa.
Language: OCL
Formal wording:
(selection<>null) = (ordering=ObjectNodeOrderingKind::ordered)
Name: object_flow_edges
Related element: ObjectNode
Description: If isControlType=false, the ActivityEdges incoming to or outgoing from an ObjectNode must all be ObjectFlows.
Language: OCL
Formal wording:
(not isControlType) implies incoming->union(outgoing)->forAll(oclIsKindOf(ObjectFlow))
Name: spec
Related element: Variable-isAccessibleBy
Language: OCL
Formal wording:
result = (if scope<>null then scope.allOwnedNodes()->includes(a) else a.containingActivity()=activityScope endif)
Name: no_expr_requires_observation
Related element: Duration
Description: If a Duration has no expr, then it must have a single observation that is a DurationObservation.
Language: OCL
Formal wording:
expr = null implies (observation->size() = 1 and observation->forAll(oclIsKindOf(DurationObservation)))
Name: first_event_multiplicity
Related element: DurationConstraint
Description: The multiplicity of firstEvent must be 2 if the multiplicity of constrainedElement is 2. Otherwise the multiplicity of firstEvent is 0.
Language: OCL
Formal wording:
if (constrainedElement->size() = 2) then (firstEvent->size() = 2) else (firstEvent->size() = 0) endif
Name: has_one_or_two_constrainedElements
Related element: DurationConstraint
Description: A DurationConstraint has either one or two constrainedElements.
Language: OCL
Formal wording:
constrainedElement->size() = 1 or constrainedElement->size()=2
Name: first_event_multiplicity
Related element: DurationObservation
Description: The multiplicity of firstEvent must be 2 if the multiplicity of event is 2. Otherwise the multiplicity of firstEvent is 0.
Language: OCL
Formal wording:
if (event->size() = 2) then (firstEvent->size() = 2) else (firstEvent->size() = 0) endif
Name: spec
Related element: LiteralBoolean-booleanValue
Language: OCL
Formal wording:
result = (value)
Name: spec
Related element: LiteralBoolean-isComputable
Language: OCL
Formal wording:
result = (true)
Name: spec
Related element: LiteralInteger-integerValue
Language: OCL
Formal wording:
result = (value)
Name: spec
Related element: LiteralInteger-isComputable
Language: OCL
Formal wording:
result = (true)
Name: spec
Related element: LiteralNull-isComputable
Language: OCL
Formal wording:
result = (true)
Name: spec
Related element: LiteralNull-isNull
Language: OCL
Formal wording:
result = (true)
Name: spec
Related element: LiteralReal-isComputable
Language: OCL
Formal wording:
result = (true)
Name: spec
Related element: LiteralReal-realValue
Language: OCL
Formal wording:
result = (value)
Name: spec
Related element: LiteralString-isComputable
Language: OCL
Formal wording:
result = (true)
Name: spec
Related element: LiteralString-stringValue
Language: OCL
Formal wording:
result = (value)
Name: spec
Related element: LiteralUnlimitedNatural-isComputable
Language: OCL
Formal wording:
result = (true)
Name: spec
Related element: LiteralUnlimitedNatural-unlimitedValue
Language: OCL
Formal wording:
result = (value)
Name: language_body_size
Related element: OpaqueExpression
Description: If the language attribute is not empty, then the size of the body and language arrays must be the same.
Language: OCL
Formal wording:
language->notEmpty() implies (_'body'->size() = language->size())
Name: one_return_result_parameter
Related element: OpaqueExpression
Description: The behavior must have exactly one return result parameter.
Language: OCL
Formal wording:
behavior <> null implies behavior.ownedParameter->select(direction=ParameterDirectionKind::return)->size() = 1
Name: only_return_result_parameters
Related element: OpaqueExpression
Description: The behavior may only have return result parameters.
Language: OCL
Formal wording:
behavior <> null implies behavior.ownedParameter->select(direction<>ParameterDirectionKind::return)->isEmpty()
Name: spec
Related element: OpaqueExpression-isIntegral
Language: OCL
Formal wording:
result = (false)
Name: pre
Related element: OpaqueExpression-isNonNegative
Language: OCL
Formal wording:
self.isIntegral()
Name: spec
Related element: OpaqueExpression-isNonNegative
Language: OCL
Formal wording:
result = (false)
Name: spec
Related element: OpaqueExpression-isPositive
Language: OCL
Formal wording:
result = (false)
Name: pre
Related element: OpaqueExpression-isPositive
Language: OCL
Formal wording:
self.isIntegral()
Name: spec
Related element: OpaqueExpression-result.1 OpaqueExpression-result
Language: OCL
Formal wording:
result = (if behavior = null then null else behavior.ownedParameter->first() endif)
Name: pre
Related element: OpaqueExpression-value
Language: OCL
Formal wording:
self.isIntegral()
Name: spec
Related element: OpaqueExpression-value
Language: OCL
Formal wording:
result = (0)
Name: operands
Related element: StringExpression
Description: All the operands of a StringExpression must be LiteralStrings
Language: OCL
Formal wording:
operand->forAll (oclIsKindOf (LiteralString))
Name: subexpressions
Related element: StringExpression
Description: If a StringExpression has sub-expressions, it cannot have operands and vice versa (this avoids the problem of having to define a collating sequence between operands and subexpressions).
Language: OCL
Formal wording:
if subExpression->notEmpty() then operand->isEmpty() else operand->notEmpty() endif
Name: spec
Related element: StringExpression-stringValue
Language: OCL
Formal wording:
result = (if subExpression->notEmpty() then subExpression->iterate(se; stringValue: String = '' | stringValue.concat(se.stringValue())) else operand->iterate(op; stringValue: String = '' | stringValue.concat(op.stringValue())) endif)
Name: has_one_constrainedElement
Related element: TimeConstraint
Description: A TimeConstraint has one constrainedElement.
Language: OCL
Formal wording:
constrainedElement->size() = 1
Name: no_expr_requires_observation
Related element: TimeExpression
Description: If a TimeExpression has no expr, then it must have a single observation that is a TimeObservation.
Language: OCL
Formal wording:
expr = null implies (observation->size() = 1 and observation->forAll(oclIsKindOf(TimeObservation)))
Name: spec
Related element: ValueSpecification-booleanValue
Language: OCL
Formal wording:
result = (null)
Name: spec
Related element: ValueSpecification-integerValue
Language: OCL
Formal wording:
result = (null)
Name: spec
Related element: ValueSpecification-isCompatibleWith
Language: OCL
Formal wording:
result = (self.oclIsKindOf(p.oclType()) and (p.oclIsKindOf(TypedElement) implies self.type.conformsTo(p.oclAsType(TypedElement).type)))
Name: spec
Related element: ValueSpecification-isComputable
Language: OCL
Formal wording:
result = (false)
Name: spec
Related element: ValueSpecification-isNull
Language: OCL
Formal wording:
result = (false)
Name: spec
Related element: ValueSpecification-realValue
Language: OCL
Formal wording:
result = (null)
Name: spec
Related element: ValueSpecification-stringValue
Language: OCL
Formal wording:
result = (null)
Name: spec
Related element: ValueSpecification-unlimitedValue
Language: OCL
Formal wording:
result = (null)
Name: associations
Related element: Actor
Description: An Actor can only have Associations to UseCases, Components, and Classes. Furthermore these Associations must be binary.
Language: OCL
Formal wording:
Association.allInstances()->forAll( a |
a.memberEnd->collect(type)->includes(self) implies
(
a.memberEnd->size() = 2 and
let actorEnd : Property = a.memberEnd->any(type = self) in
actorEnd.opposite.class.oclIsKindOf(UseCase) or
( actorEnd.opposite.class.oclIsKindOf(Class) and not
actorEnd.opposite.class.oclIsKindOf(Behavior))
)
)
Name: must_have_name
Related element: Actor
Description: An Actor must have a name.
Language: OCL
Formal wording:
name->notEmpty()
Name: extension_points
Related element: Extend
Description: The ExtensionPoints referenced by the Extend relationship must belong to the UseCase that is being extended.
Language: OCL
Formal wording:
extensionLocation->forAll (xp | extendedCase.extensionPoint->includes(xp))
Name: must_have_name
Related element: ExtensionPoint
Description: An ExtensionPoint must have a name.
Language: OCL
Formal wording:
name->notEmpty ()
Name: binary_associations
Related element: UseCase
Description: UseCases can only be involved in binary Associations.
Language: OCL
Formal wording:
Association.allInstances()->forAll(a | a.memberEnd.type->includes(self) implies a.memberEnd->size() = 2)
Name: no_association_to_use_case
Related element: UseCase
Description: UseCases cannot have Associations to UseCases specifying the same subject.
Language: OCL
Formal wording:
Association.allInstances()->forAll(a | a.memberEnd.type->includes(self) implies ( let usecases: Set(UseCase) = a.memberEnd.type->select(oclIsKindOf(UseCase))->collect(oclAsType(UseCase))->asSet() in usecases->size() > 1 implies usecases->collect(subject)->size() > 1 ) )
Name: cannot_include_self
Related element: UseCase
Description: A UseCase cannot include UseCases that directly or indirectly include it.
Language: OCL
Formal wording:
not allIncludedUseCases()->includes(self)
Name: must_have_name
Related element: UseCase
Description: A UseCase must have a name.
Language: OCL
Formal wording:
name -> notEmpty ()
Name: spec
Related element: UseCase-allIncludedUseCases
Language: OCL
Formal wording:
result = (self.include.addition->union(self.include.addition->collect(uc | uc.allIncludedUseCases()))->asSet())
Name: specialized_end_number
Related element: Association
Description: An Association specializing another Association has the same number of ends as the other Association.
Language: OCL
Formal wording:
parents()->select(oclIsKindOf(Association)).oclAsType(Association)->forAll(p | p.memberEnd->size() = self.memberEnd->size())
Name: specialized_end_types
Related element: Association
Description: When an Association specializes another Association, every end of the specific Association corresponds to an end of the general Association, and the specific end reaches the same type or a subtype of the corresponding general end.
Language: OCL
Formal wording:
Sequence{1..memberEnd->size()}->
forAll(i | general->select(oclIsKindOf(Association)).oclAsType(Association)->
forAll(ga | self.memberEnd->at(i).type.conformsTo(ga.memberEnd->at(i).type)))
Name: binary_associations
Related element: Association
Description: Only binary Associations can be aggregations.
Language: OCL
Formal wording:
memberEnd->exists(aggregation <> AggregationKind::none) implies (memberEnd->size() = 2 and memberEnd->exists(aggregation = AggregationKind::none))
Name: association_ends
Related element: Association
Description: Ends of Associations with more than two ends must be owned by the Association itself.
Language: OCL
Formal wording:
memberEnd->size() > 2 implies ownedEnd->includesAll(memberEnd)
Name: ends_must_be_typed
Related element: Association
Language: OCL
Formal wording:
memberEnd->forAll(type->notEmpty())
Name: spec
Related element: Association-endType.1 Association-endType
Language: OCL
Formal wording:
result = (memberEnd->collect(type)->asSet())
Name: cannot_be_defined
Related element: AssociationClass
Description: An AssociationClass cannot be defined between itself and something else.
Language: OCL
Formal wording:
self.endType()->excludes(self) and self.endType()->collect(et|et.oclAsType(Classifier).allParents())->flatten()->excludes(self)
Name: disjoint_attributes_ends
Related element: AssociationClass
Description: The owned attributes and owned ends of an AssociationClass are disjoint.
Language: OCL
Formal wording:
ownedAttribute->intersection(ownedEnd)->isEmpty()
Name: passive_class
Related element: Class
Description: Only an active Class may own Receptions and have a classifierBehavior.
Language: OCL
Formal wording:
not isActive implies (ownedReception->isEmpty() and classifierBehavior = null)
Name: spec
Related element: Class-extension.1 Class-extension
Language: OCL
Formal wording:
result = (Extension.allInstances()->select(ext | let endTypes : Sequence(Classifier) = ext.memberEnd->collect(type.oclAsType(Classifier)) in endTypes->includes(self) or endTypes.allParents()->includes(self) ))
Name: spec
Related element: Class-superClass.1 Class-superClass
Language: OCL
Formal wording:
result = (self.general()->select(oclIsKindOf(Class))->collect(oclAsType(Class))->asSet())
Name: client_elements
Related element: CollaborationUse
Description: All the client elements of a roleBinding are in one Classifier and all supplier elements of a roleBinding are in one Collaboration.
Language: OCL
Formal wording:
roleBinding->collect(client)->forAll(ne1, ne2 |
ne1.oclIsKindOf(ConnectableElement) and ne2.oclIsKindOf(ConnectableElement) and
let ce1 : ConnectableElement = ne1.oclAsType(ConnectableElement), ce2 : ConnectableElement = ne2.oclAsType(ConnectableElement) in
ce1.structuredClassifier = ce2.structuredClassifier)
and
roleBinding->collect(supplier)->forAll(ne1, ne2 |
ne1.oclIsKindOf(ConnectableElement) and ne2.oclIsKindOf(ConnectableElement) and
let ce1 : ConnectableElement = ne1.oclAsType(ConnectableElement), ce2 : ConnectableElement = ne2.oclAsType(ConnectableElement) in
ce1.collaboration = ce2.collaboration)
Name: every_role
Related element: CollaborationUse
Description: Every collaborationRole in the Collaboration is bound within the CollaborationUse.
Language: OCL
Formal wording:
type.collaborationRole->forAll(role | roleBinding->exists(rb | rb.supplier->includes(role)))
Name: connectors
Related element: CollaborationUse
Description: Connectors in a Collaboration typing a CollaborationUse must have corresponding Connectors between elements bound in the context Classifier, and these corresponding Connectors must have the same or more general type than the Collaboration Connectors.
Language: OCL
Formal wording:
type.ownedConnector->forAll(connector |
let rolesConnectedInCollab : Set(ConnectableElement) = connector.end.role->asSet(),
relevantBindings : Set(Dependency) = roleBinding->select(rb | rb.supplier->intersection(rolesConnectedInCollab)->notEmpty()),
boundRoles : Set(ConnectableElement) = relevantBindings->collect(client.oclAsType(ConnectableElement))->asSet(),
contextClassifier : StructuredClassifier = boundRoles->any(true).structuredClassifier->any(true) in
contextClassifier.ownedConnector->exists( correspondingConnector |
correspondingConnector.end.role->forAll( role | boundRoles->includes(role) )
and (connector.type->notEmpty() and correspondingConnector.type->notEmpty()) implies connector.type->forAll(conformsTo(correspondingConnector.type)) )
)
Name: no_nested_classifiers
Related element: Component
Description: A Component cannot nest Classifiers.
Language: OCL
Formal wording:
nestedClassifier->isEmpty()
Name: no_packaged_elements
Related element: Component
Description: A Component nested in a Class cannot have any packaged elements.
Language: OCL
Formal wording:
nestingClass <> null implies packagedElement->isEmpty()
Name: spec
Related element: Component-provided.1 Component-provided
Language: OCL
Formal wording:
result = (let ris : Set(Interface) = allRealizedInterfaces(),
realizingClassifiers : Set(Classifier) = self.realization.realizingClassifier->union(self.allParents()->collect(realization.realizingClassifier))->asSet(),
allRealizingClassifiers : Set(Classifier) = realizingClassifiers->union(realizingClassifiers.allParents())->asSet(),
realizingClassifierInterfaces : Set(Interface) = allRealizingClassifiers->iterate(c; rci : Set(Interface) = Set{} | rci->union(c.allRealizedInterfaces())),
ports : Set(Port) = self.ownedPort->union(allParents()->collect(ownedPort))->asSet(),
providedByPorts : Set(Interface) = ports.provided->asSet()
in ris->union(realizingClassifierInterfaces) ->union(providedByPorts)->asSet())
Name: spec
Related element: Component-required.1 Component-required
Language: OCL
Formal wording:
result = (let uis : Set(Interface) = allUsedInterfaces(),
realizingClassifiers : Set(Classifier) = self.realization.realizingClassifier->union(self.allParents()->collect(realization.realizingClassifier))->asSet(),
allRealizingClassifiers : Set(Classifier) = realizingClassifiers->union(realizingClassifiers.allParents())->asSet(),
realizingClassifierInterfaces : Set(Interface) = allRealizingClassifiers->iterate(c; rci : Set(Interface) = Set{} | rci->union(c.allUsedInterfaces())),
ports : Set(Port) = self.ownedPort->union(allParents()->collect(ownedPort))->asSet(),
usedByPorts : Set(Interface) = ports.required->asSet()
in uis->union(realizingClassifierInterfaces)->union(usedByPorts)->asSet()
)
Name: spec
Related element: ConnectableElement-end.1 ConnectableElement-end
Language: OCL
Formal wording:
result = (ConnectorEnd.allInstances()->select(role = self))
Name: types
Related element: Connector
Description: The types of the ConnectableElements that the ends of a Connector are attached to must conform to the types of the ends of the Association that types the Connector, if any.
Language: OCL
Formal wording:
type<>null implies
let noOfEnds : Integer = end->size() in
(type.memberEnd->size() = noOfEnds) and Sequence{1..noOfEnds}->forAll(i | end->at(i).role.type.conformsTo(type.memberEnd->at(i).type))
Name: roles
Related element: Connector
Description: The ConnectableElements attached as roles to each ConnectorEnd owned by a Connector must be owned or inherited roles of the Classifier that owned the Connector, or they must be Ports of such roles.
Language: OCL
Formal wording:
structuredClassifier <> null and end->forAll( e | structuredClassifier.allRoles()->includes(e.role) or e.role.oclIsKindOf(Port) and structuredClassifier.allRoles()->includes(e.partWithPort))
Name: spec
Related element: Connector-kind.1 Connector-kind
Language: OCL
Formal wording:
result = (if end->exists( role.oclIsKindOf(Port) and partWithPort->isEmpty() and not role.oclAsType(Port).isBehavior) then ConnectorKind::delegation else ConnectorKind::assembly endif)
Name: role_and_part_with_port
Related element: ConnectorEnd
Description: If a ConnectorEnd references a partWithPort, then the role must be a Port that is defined or inherited by the type of the partWithPort.
Language: OCL
Formal wording:
partWithPort->notEmpty() implies (role.oclIsKindOf(Port) and partWithPort.type.oclAsType(Namespace).member->includes(role))
Name: part_with_port_empty
Related element: ConnectorEnd
Description: If a ConnectorEnd is attached to a Port of the containing Classifier, partWithPort will be empty.
Language: OCL
Formal wording:
(role.oclIsKindOf(Port) and role.owner = connector.owner) implies partWithPort->isEmpty()
Name: multiplicity
Related element: ConnectorEnd
Description: The multiplicity of the ConnectorEnd may not be more general than the multiplicity of the corresponding end of the Association typing the owning Connector, if any.
Language: OCL
Formal wording:
self.compatibleWith(definingEnd)
Name: self_part_with_port
Related element: ConnectorEnd
Description: The Property held in self.partWithPort must not be a Port.
Language: OCL
Formal wording:
partWithPort->notEmpty() implies not partWithPort.oclIsKindOf(Port)
Name: spec
Related element: ConnectorEnd-definingEnd.1 ConnectorEnd-definingEnd
Language: OCL
Formal wording:
result = (if connector.type = null
then
null
else
let index : Integer = connector.end->indexOf(self) in
connector.type.memberEnd->at(index)
endif)
Name: spec
Related element: EncapsulatedClassifier-ownedPort.1 EncapsulatedClassifier-ownedPort
Language: OCL
Formal wording:
result = (ownedAttribute->select(oclIsKindOf(Port))->collect(oclAsType(Port))->asOrderedSet())
Name: port_aggregation
Related element: Port
Description: Port.aggregation must be composite.
Language: OCL
Formal wording:
aggregation = AggregationKind::composite
Name: default_value
Related element: Port
Description: A defaultValue for port cannot be specified when the type of the Port is an Interface.
Language: OCL
Formal wording:
type.oclIsKindOf(Interface) implies defaultValue->isEmpty()
Name: encapsulated_owner
Related element: Port
Description: All Ports are owned by an EncapsulatedClassifier.
Language: OCL
Formal wording:
owner = encapsulatedClassifier
Name: spec
Related element: Port-provided.1 Port-provided
Language: OCL
Formal wording:
result = (if isConjugated then basicRequired() else basicProvided() endif)
Name: spec
Related element: Port-required.1 Port-required
Language: OCL
Formal wording:
result = (if isConjugated then basicProvided() else basicRequired() endif)
Name: spec
Related element: Port-basicProvided
Language: OCL
Formal wording:
result = (if type.oclIsKindOf(Interface) then type.oclAsType(Interface)->asSet() else type.oclAsType(Classifier).allRealizedInterfaces() endif)
Name: spec
Related element: Port-basicRequired
Language: OCL
Formal wording:
result = ( type.oclAsType(Classifier).allUsedInterfaces() )
Name: spec
Related element: StructuredClassifier-part.1 StructuredClassifier-part
Language: OCL
Formal wording:
result = (ownedAttribute->select(isComposite))
Name: spec
Related element: StructuredClassifier-allRoles
Language: OCL
Formal wording:
result = (allFeatures()->select(oclIsKindOf(ConnectableElement))->collect(oclAsType(ConnectableElement))->asSet())
Name: exit_pseudostates
Related element: ConnectionPointReference
Description: The exit Pseudostates must be Pseudostates with kind exitPoint.
Language: OCL
Formal wording:
exit->forAll(kind = PseudostateKind::exitPoint)
Name: entry_pseudostates
Related element: ConnectionPointReference
Description: The entry Pseudostates must be Pseudostates with kind entryPoint.
Language: OCL
Formal wording:
entry->forAll(kind = PseudostateKind::entryPoint)
Name: no_exit_behavior
Related element: FinalState
Description: A FinalState has no exit Behavior.
Language: OCL
Formal wording:
exit->isEmpty()
Name: no_outgoing_transitions
Related element: FinalState
Description: A FinalState cannot have any outgoing Transitions.
Language: OCL
Formal wording:
outgoing->size() = 0
Name: no_regions
Related element: FinalState
Description: A FinalState cannot have Regions.
Language: OCL
Formal wording:
region->size() = 0
Name: cannot_reference_submachine
Related element: FinalState
Description: A FinalState cannot reference a submachine.
Language: OCL
Formal wording:
submachine->isEmpty()
Name: no_entry_behavior
Related element: FinalState
Description: A FinalState has no entry Behavior.
Language: OCL
Formal wording:
entry->isEmpty()
Name: no_state_behavior
Related element: FinalState
Description: A FinalState has no state (doActivity) Behavior.
Language: OCL
Formal wording:
doActivity->isEmpty()
Name: classifier_context
Related element: ProtocolStateMachine
Description: A ProtocolStateMachine must only have a Classifier context, not a BehavioralFeature context.
Language: OCL
Formal wording:
_'context' <> null and specification = null
Name: deep_or_shallow_history
Related element: ProtocolStateMachine
Description: ProtocolStateMachines cannot have deep or shallow history Pseudostates.
Language: OCL
Formal wording:
region->forAll (r | r.subvertex->forAll (v | v.oclIsKindOf(Pseudostate) implies ((v.oclAsType(Pseudostate).kind <> PseudostateKind::deepHistory) and (v.oclAsType(Pseudostate).kind <> PseudostateKind::shallowHistory))))
Name: entry_exit_do
Related element: ProtocolStateMachine
Description: The states of a ProtocolStateMachine cannot have entry, exit, or do activity Behaviors.
Language: OCL
Formal wording:
region->forAll(r | r.subvertex->forAll(v | v.oclIsKindOf(State) implies (v.oclAsType(State).entry->isEmpty() and v.oclAsType(State).exit->isEmpty() and v.oclAsType(State).doActivity->isEmpty())))
Name: protocol_transitions
Related element: ProtocolStateMachine
Description: All Transitions of a ProtocolStateMachine must be ProtocolTransitions.
Language: OCL
Formal wording:
region->forAll(r | r.transition->forAll(t | t.oclIsTypeOf(ProtocolTransition)))
Name: refers_to_operation
Related element: ProtocolTransition
Description: If a ProtocolTransition refers to an Operation (i.e., has a CallEvent trigger corresponding to an Operation), then that Operation should apply to the context Classifier of the StateMachine of the ProtocolTransition.
Language: OCL
Formal wording:
if (referred()->notEmpty() and containingStateMachine()._'context'->notEmpty()) then
containingStateMachine()._'context'.oclAsType(BehavioredClassifier).allFeatures()->includesAll(referred())
else true endif
Name: associated_actions
Related element: ProtocolTransition
Description: A ProtocolTransition never has associated Behaviors.
Language: OCL
Formal wording:
effect = null
Name: belongs_to_psm
Related element: ProtocolTransition
Description: A ProtocolTransition always belongs to a ProtocolStateMachine.
Language: OCL
Formal wording:
container.belongsToPSM()
Name: spec
Related element: ProtocolTransition-referred.1 ProtocolTransition-referred
Language: OCL
Formal wording:
result = (trigger->collect(event)->select(oclIsKindOf(CallEvent))->collect(oclAsType(CallEvent).operation)->asSet())
Name: transitions_outgoing
Related element: Pseudostate
Description: All transitions outgoing a fork vertex must target states in different regions of an orthogonal state.
Language: OCL
Formal wording:
(kind = PseudostateKind::fork) implies -- for any pair of outgoing transitions there exists an orthogonal state which contains the targets of these transitions -- such that these targets belong to different regions of that orthogonal state outgoing->forAll(t1:Transition, t2:Transition | let contState:State = containingStateMachine().LCAState(t1.target, t2.target) in ((contState <> null) and (contState.region ->exists(r1:Region, r2: Region | (r1 <> r2) and t1.target.isContainedInRegion(r1) and t2.target.isContainedInRegion(r2)))))
Name: choice_vertex
Related element: Pseudostate
Description: In a complete statemachine, a choice Vertex must have at least one incoming and one outgoing Transition.
Language: OCL
Formal wording:
(kind = PseudostateKind::choice) implies (incoming->size() >= 1 and outgoing->size() >= 1)
Name: outgoing_from_initial
Related element: Pseudostate
Description: The outgoing Transition from an initial vertex may have a behavior, but not a trigger or a guard.
Language: OCL
Formal wording:
(kind = PseudostateKind::initial) implies (outgoing.guard = null and outgoing.trigger->isEmpty())
Name: join_vertex
Related element: Pseudostate
Description: In a complete StateMachine, a join Vertex must have at least two incoming Transitions and exactly one outgoing Transition.
Language: OCL
Formal wording:
(kind = PseudostateKind::join) implies (outgoing->size() = 1 and incoming->size() >= 2)
Name: junction_vertex
Related element: Pseudostate
Description: In a complete StateMachine, a junction Vertex must have at least one incoming and one outgoing Transition.
Language: OCL
Formal wording:
(kind = PseudostateKind::junction) implies (incoming->size() >= 1 and outgoing->size() >= 1)
Name: history_vertices
Related element: Pseudostate
Description: History Vertices can have at most one outgoing Transition.
Language: OCL
Formal wording:
((kind = PseudostateKind::deepHistory) or (kind = PseudostateKind::shallowHistory)) implies (outgoing->size() <= 1)
Name: initial_vertex
Related element: Pseudostate
Description: An initial Vertex can have at most one outgoing Transition.
Language: OCL
Formal wording:
(kind = PseudostateKind::initial) implies (outgoing->size() <= 1)
Name: fork_vertex
Related element: Pseudostate
Description: In a complete StateMachine, a fork Vertex must have at least two outgoing Transitions and exactly one incoming Transition.
Language: OCL
Formal wording:
(kind = PseudostateKind::fork) implies (incoming->size() = 1 and outgoing->size() >= 2)
Name: transitions_incoming
Related element: Pseudostate
Description: All Transitions incoming a join Vertex must originate in different Regions of an orthogonal State.
Language: OCL
Formal wording:
(kind = PseudostateKind::join) implies -- for any pair of incoming transitions there exists an orthogonal state which contains the source vetices of these transitions -- such that these source vertices belong to different regions of that orthogonal state incoming->forAll(t1:Transition, t2:Transition | let contState:State = containingStateMachine().LCAState(t1.source, t2.source) in ((contState <> null) and (contState.region ->exists(r1:Region, r2: Region | (r1 <> r2) and t1.source.isContainedInRegion(r1) and t2.source.isContainedInRegion(r2)))))
Name: deep_history_vertex
Related element: Region
Description: A Region can have at most one deep history Vertex.
Language: OCL
Formal wording:
self.subvertex->select (oclIsKindOf(Pseudostate))->collect(oclAsType(Pseudostate))-> select(kind = PseudostateKind::deepHistory)->size() <= 1
Name: shallow_history_vertex
Related element: Region
Description: A Region can have at most one shallow history Vertex.
Language: OCL
Formal wording:
subvertex->select(oclIsKindOf(Pseudostate))->collect(oclAsType(Pseudostate))-> select(kind = PseudostateKind::shallowHistory)->size() <= 1
Name: owned
Related element: Region
Description: If a Region is owned by a StateMachine, then it cannot also be owned by a State and vice versa.
Language: OCL
Formal wording:
(stateMachine <> null implies state = null) and (state <> null implies stateMachine = null)
Name: initial_vertex
Related element: Region
Description: A Region can have at most one initial Vertex.
Language: OCL
Formal wording:
self.subvertex->select (oclIsKindOf(Pseudostate))->collect(oclAsType(Pseudostate))-> select(kind = PseudostateKind::initial)->size() <= 1
Name: spec
Related element: Region-belongsToPSM
Language: OCL
Formal wording:
result = (if stateMachine <> null then stateMachine.oclIsKindOf(ProtocolStateMachine) else state <> null implies state.container.belongsToPSM() endif )
Name: spec
Related element: Region-containingStateMachine
Language: OCL
Formal wording:
result = (if stateMachine = null then state.containingStateMachine() else stateMachine endif)
Name: spec
Related element: Region-isConsistentWith
Language: OCL
Formal wording:
result = (-- the following is merely a default body; it is expected that the specific form of this constraint will be specified by profiles true)
Name: pre
Related element: Region-isConsistentWith
Language: OCL
Formal wording:
redefiningElement.isRedefinitionContextValid(self)
Name: spec
Related element: Region-isRedefinitionContextValid
Language: OCL
Formal wording:
result = (if redefinedElement.oclIsKindOf(Region) then
let redefinedRegion : Region = redefinedElement.oclAsType(Region) in
if stateMachine->isEmpty() then
-- the Region is owned by a State
(state.redefinedState->notEmpty() and state.redefinedState.region->includes(redefinedRegion))
else -- the region is owned by a StateMachine
(stateMachine.extendedStateMachine->notEmpty() and
stateMachine.extendedStateMachine->exists(sm : StateMachine |
sm.region->includes(redefinedRegion)))
endif
else
false
endif)
Name: spec
Related element: Region-redefinitionContext.1 Region-redefinitionContext
Language: OCL
Formal wording:
result = (let sm : StateMachine = containingStateMachine() in if sm._'context' = null or sm.general->notEmpty() then sm else sm._'context' endif)
Name: entry_or_exit
Related element: State
Description: Only entry or exit Pseudostates can serve as connection points.
Language: OCL
Formal wording:
connectionPoint->forAll(kind = PseudostateKind::entryPoint or kind = PseudostateKind::exitPoint)
Name: submachine_states
Related element: State
Description: Only submachine States can have connection point references.
Language: OCL
Formal wording:
isSubmachineState implies connection->notEmpty( )
Name: composite_states
Related element: State
Description: Only composite States can have entry or exit Pseudostates defined.
Language: OCL
Formal wording:
connectionPoint->notEmpty() implies isComposite
Name: destinations_or_sources_of_transitions
Related element: State
Description: The connection point references used as destinations/sources of Transitions associated with a submachine State must be defined as entry/exit points in the submachine StateMachine.
Language: OCL
Formal wording:
self.isSubmachineState implies (self.connection->forAll (cp | cp.entry->forAll (ps | ps.stateMachine = self.submachine) and cp.exit->forAll (ps | ps.stateMachine = self.submachine)))
Name: submachine_or_regions
Related element: State
Description: A State is not allowed to have both a submachine and Regions.
Language: OCL
Formal wording:
isComposite implies not isSubmachineState
Name: spec
Related element: State-containingStateMachine
Language: OCL
Formal wording:
result = (container.containingStateMachine())
Name: spec
Related element: State-isComposite.1 State-isComposite
Language: OCL
Formal wording:
result = (region->notEmpty())
Name: spec
Related element: State-isConsistentWith
Language: OCL
Formal wording:
result = (-- the following is merely a default body; it is expected that the specific form of this constraint will be specified by profiles true)
Name: pre
Related element: State-isConsistentWith
Language: OCL
Formal wording:
redefiningElement.isRedefinitionContextValid(self)
Name: spec
Related element: State-isOrthogonal.1 State-isOrthogonal
Language: OCL
Formal wording:
result = (region->size () > 1)
Name: spec
Related element: State-isRedefinitionContextValid
Language: OCL
Formal wording:
result = (if redefinedElement.oclIsKindOf(State) then
let redefinedState : State = redefinedElement.oclAsType(State) in
container.redefinedElement.oclAsType(Region)->exists(r:Region |
r.subvertex->includes(redefinedState))
else
false
endif)
Name: spec
Related element: State-isSimple.1 State-isSimple
Language: OCL
Formal wording:
result = ((region->isEmpty()) and not isSubmachineState())
Name: spec
Related element: State-isSubmachineState.1 State-isSubmachineState
Language: OCL
Formal wording:
result = (submachine <> null)
Name: spec
Related element: State-redefinitionContext.1 State-redefinitionContext
Language: OCL
Formal wording:
result = (let sm : StateMachine = containingStateMachine() in if sm._'context' = null or sm.general->notEmpty() then sm else sm._'context' endif)
Name: connection_points
Related element: StateMachine
Description: The connection points of a StateMachine are Pseudostates of kind entry point or exit point.
Language: OCL
Formal wording:
connectionPoint->forAll (kind = PseudostateKind::entryPoint or kind = PseudostateKind::exitPoint)
Name: classifier_context
Related element: StateMachine
Description: The Classifier context of a StateMachine cannot be an Interface.
Language: OCL
Formal wording:
_'context' <> null implies not _'context'.oclIsKindOf(Interface)
Name: method
Related element: StateMachine
Description: A StateMachine as the method for a BehavioralFeature cannot have entry/exit connection points.
Language: OCL
Formal wording:
specification <> null implies connectionPoint->isEmpty()
Name: context_classifier
Related element: StateMachine
Description: The context Classifier of the method StateMachine of a BehavioralFeature must be the Classifier that owns the BehavioralFeature.
Language: OCL
Formal wording:
specification <> null implies ( _'context' <> null and specification.featuringClassifier->exists(c | c = _'context'))
Name: spec
Related element: StateMachine-LCA
Language: OCL
Formal wording:
result = (if ancestor(s1, s2) then
s2.container
else
if ancestor(s2, s1) then
s1.container
else
LCA(s1.container.state, s2.container.state)
endif
endif)
Name: spec
Related element: StateMachine-ancestor
Language: OCL
Formal wording:
result = (if (s2 = s1) then true else if s1.container.stateMachine->notEmpty() then true else if s2.container.stateMachine->notEmpty() then false else ancestor(s1, s2.container.state) endif endif endif )
Name: spec
Related element: StateMachine-isConsistentWith
Language: OCL
Formal wording:
result = (-- the following is merely a default body; it is expected that the specific form of this constraint will be specified by profiles true)
Name: spec
Related element: StateMachine-isRedefinitionContextValid
Language: OCL
Formal wording:
result = (if redefinedElement.oclIsKindOf(StateMachine) then
let redefinedStateMachine : StateMachine = redefinedElement.oclAsType(StateMachine) in
self._'context'().oclAsType(BehavioredClassifier).redefinedClassifier->
includes(redefinedStateMachine._'context'())
else
false
endif)
Name: spec
Related element: StateMachine-LCAState
Language: OCL
Formal wording:
result = (if v2.oclIsTypeOf(State) and ancestor(v1, v2) then v2.oclAsType(State) else if v1.oclIsTypeOf(State) and ancestor(v2, v1) then v1.oclAsType(State) else if (v1.container.state->isEmpty() or v2.container.state->isEmpty()) then null.oclAsType(State) else LCAState(v1.container.state, v2.container.state) endif endif endif)
Name: state_is_external
Related element: Transition
Description: A Transition with kind external can source any Vertex except entry points.
Language: OCL
Formal wording:
(kind = TransitionKind::external) implies not (source.oclIsKindOf(Pseudostate) and source.oclAsType(Pseudostate).kind = PseudostateKind::entryPoint)
Name: join_segment_guards
Related element: Transition
Description: A join segment must not have Guards or Triggers.
Language: OCL
Formal wording:
(target.oclIsKindOf(Pseudostate) and target.oclAsType(Pseudostate).kind = PseudostateKind::join) implies (guard = null and trigger->isEmpty())
Name: state_is_internal
Related element: Transition
Description: A Transition with kind internal must have a State as its source, and its source and target must be equal.
Language: OCL
Formal wording:
(kind = TransitionKind::internal) implies (source.oclIsKindOf (State) and source = target)
Name: outgoing_pseudostates
Related element: Transition
Description: Transitions outgoing Pseudostates may not have a Trigger.
Language: OCL
Formal wording:
source.oclIsKindOf(Pseudostate) and (source.oclAsType(Pseudostate).kind <> PseudostateKind::initial) implies trigger->isEmpty()
Name: join_segment_state
Related element: Transition
Description: A join segment must always originate from a State.
Language: OCL
Formal wording:
(target.oclIsKindOf(Pseudostate) and target.oclAsType(Pseudostate).kind = PseudostateKind::join) implies (source.oclIsKindOf(State))
Name: fork_segment_state
Related element: Transition
Description: A fork segment must always target a State.
Language: OCL
Formal wording:
(source.oclIsKindOf(Pseudostate) and source.oclAsType(Pseudostate).kind = PseudostateKind::fork) implies (target.oclIsKindOf(State))
Name: state_is_local
Related element: Transition
Description: A Transition with kind local must have a composite State or an entry point as its source.
Language: OCL
Formal wording:
(kind = TransitionKind::local) implies ((source.oclIsKindOf (State) and source.oclAsType(State).isComposite) or (source.oclIsKindOf (Pseudostate) and source.oclAsType(Pseudostate).kind = PseudostateKind::entryPoint))
Name: initial_transition
Related element: Transition
Description: An initial Transition at the topmost level Region of a StateMachine that has no Trigger.
Language: OCL
Formal wording:
(source.oclIsKindOf(Pseudostate) and container.stateMachine->notEmpty()) implies trigger->isEmpty()
Name: fork_segment_guards
Related element: Transition
Description: A fork segment must not have Guards or Triggers.
Language: OCL
Formal wording:
(source.oclIsKindOf(Pseudostate) and source.oclAsType(Pseudostate).kind = PseudostateKind::fork) implies (guard = null and trigger->isEmpty())
Name: spec
Related element: Transition-containingStateMachine
Language: OCL
Formal wording:
result = (container.containingStateMachine())
Name: spec
Related element: Transition-isConsistentWith
Language: OCL
Formal wording:
result = (-- the following is merely a default body; it is expected that the specific form of this constraint will be specified by profiles true)
Name: pre
Related element: Transition-isConsistentWith
Language: OCL
Formal wording:
redefiningElement.isRedefinitionContextValid(self)
Name: spec
Related element: Transition-redefinitionContext.1 Transition-redefinitionContext
Language: OCL
Formal wording:
result = (let sm : StateMachine = containingStateMachine() in if sm._'context' = null or sm.general->notEmpty() then sm else sm._'context' endif)
Name: spec
Related element: Vertex-containingStateMachine
Language: OCL
Formal wording:
result = (if container <> null
then
-- the container is a region
container.containingStateMachine()
else
if (self.oclIsKindOf(Pseudostate)) and ((self.oclAsType(Pseudostate).kind = PseudostateKind::entryPoint) or (self.oclAsType(Pseudostate).kind = PseudostateKind::exitPoint)) then
self.oclAsType(Pseudostate).stateMachine
else
if (self.oclIsKindOf(ConnectionPointReference)) then
self.oclAsType(ConnectionPointReference).state.containingStateMachine() -- no other valid cases possible
else
null
endif
endif
endif
)
Name: spec
Related element: Vertex-incoming.1 Vertex-incoming
Language: OCL
Formal wording:
result = (Transition.allInstances()->select(target=self))
Name: spec
Related element: Vertex-outgoing.1 Vertex-outgoing
Language: OCL
Formal wording:
result = (Transition.allInstances()->select(source=self))
Name: spec
Related element: Vertex-isContainedInState
Language: OCL
Formal wording:
result = (if not s.isComposite() or container->isEmpty() then false else if container.state = s then true else container.state.isContainedInState(s) endif endif)
Name: spec
Related element: Vertex-isContainedInRegion
Language: OCL
Formal wording:
result = (if (container = r) then true else if (r.state->isEmpty()) then false else container.state.isContainedInRegion(r) endif endif)
Name: class_behavior
Related element: BehavioredClassifier
Description: If a behavior is classifier behavior, it does not have a specification.
Language: OCL
Formal wording:
classifierBehavior->notEmpty() implies classifierBehavior.specification->isEmpty()
Name: immutable
Related element: Enumeration
Language: OCL
Formal wording:
ownedAttribute->forAll(isReadOnly)
Name: spec
Related element: EnumerationLiteral-classifier.1 EnumerationLiteral-classifier
Language: OCL
Formal wording:
result = (enumeration)
Name: visibility
Related element: Interface
Description: The visibility of all Features owned by an Interface must be public.
Language: OCL
Formal wording:
feature->forAll(visibility = VisibilityKind::public)
Name: same_name_as_signal
Related element: Reception
Description: A Reception has the same name as its signal
Language: OCL
Formal wording:
name = signal.name
Name: same_structure_as_signal
Related element: Reception
Description: A Reception's parameters match the ownedAttributes of its signal by name, type, and multiplicity
Language: OCL
Formal wording:
signal.ownedAttribute->size() = ownedParameter->size() and
Sequence{1..signal.ownedAttribute->size()}->forAll( i |
ownedParameter->at(i).direction = ParameterDirectionKind::_'in' and
ownedParameter->at(i).name = signal.ownedAttribute->at(i).name and
ownedParameter->at(i).type = signal.ownedAttribute->at(i).type and
ownedParameter->at(i).lowerBound() = signal.ownedAttribute->at(i).lowerBound() and
ownedParameter->at(i).upperBound() = signal.ownedAttribute->at(i).upperBound()
)
Name: non_owned_end
Related element: Extension
Description: The non-owned end of an Extension is typed by a Class.
Language: OCL
Formal wording:
metaclassEnd()->notEmpty() and metaclassEnd().type.oclIsKindOf(Class)
Name: is_binary
Related element: Extension
Description: An Extension is binary, i.e., it has only two memberEnds.
Language: OCL
Formal wording:
memberEnd->size() = 2
Name: spec
Related element: Extension-isRequired.1 Extension-isRequired
Language: OCL
Formal wording:
result = (ownedEnd.lowerBound() = 1)
Name: spec
Related element: Extension-metaclass.1 Extension-metaclass
Language: OCL
Formal wording:
result = (metaclassEnd().type.oclAsType(Class))
Name: spec
Related element: Extension-metaclassEnd
Language: OCL
Formal wording:
result = (memberEnd->reject(p | ownedEnd->includes(p.oclAsType(ExtensionEnd)))->any(true))
Name: multiplicity
Related element: ExtensionEnd
Description: The multiplicity of ExtensionEnd is 0..1 or 1.
Language: OCL
Formal wording:
(lowerBound() = 0 or lowerBound() = 1) and upperBound() = 1
Name: aggregation
Related element: ExtensionEnd
Description: The aggregation of an ExtensionEnd is composite.
Language: OCL
Formal wording:
self.aggregation = AggregationKind::composite
Name: spec
Related element: ExtensionEnd-lowerBound
Language: OCL
Formal wording:
result = (if lowerValue=null then 0 else lowerValue.integerValue() endif)
Name: elements_public_or_private
Related element: Package
Description: If an element that is owned by a package has visibility, it is public or private.
Language: OCL
Formal wording:
packagedElement->forAll(e | e.visibility<> null implies e.visibility = VisibilityKind::public or e.visibility = VisibilityKind::private)
Name: spec
Related element: Package-allApplicableStereotypes
Language: OCL
Formal wording:
result = (let ownedPackages : Bag(Package) = ownedMember->select(oclIsKindOf(Package))->collect(oclAsType(Package)) in ownedStereotype->union(ownedPackages.allApplicableStereotypes())->flatten()->asSet() )
Name: spec
Related element: Package-containingProfile
Language: OCL
Formal wording:
result = (if self.oclIsKindOf(Profile) then self.oclAsType(Profile) else self.namespace.oclAsType(Package).containingProfile() endif)
Name: pre
Related element: Package-makesVisible
Language: OCL
Formal wording:
member->includes(el)
Name: spec
Related element: Package-makesVisible
Language: OCL
Formal wording:
result = (ownedMember->includes(el) or (elementImport->select(ei|ei.importedElement = VisibilityKind::public)->collect(importedElement.oclAsType(NamedElement))->includes(el)) or (packageImport->select(visibility = VisibilityKind::public)->collect(importedPackage.member->includes(el))->notEmpty()))
Name: spec
Related element: Package-mustBeOwned
Language: OCL
Formal wording:
result = (false)
Name: spec
Related element: Package-nestedPackage.1 Package-nestedPackage
Language: OCL
Formal wording:
result = (packagedElement->select(oclIsKindOf(Package))->collect(oclAsType(Package))->asSet())
Name: spec
Related element: Package-ownedStereotype.1 Package-ownedStereotype
Language: OCL
Formal wording:
result = (packagedElement->select(oclIsKindOf(Stereotype))->collect(oclAsType(Stereotype))->asSet())
Name: spec
Related element: Package-ownedType.1 Package-ownedType
Language: OCL
Formal wording:
result = (packagedElement->select(oclIsKindOf(Type))->collect(oclAsType(Type))->asSet())
Name: spec
Related element: Package-visibleMembers
Language: OCL
Formal wording:
result = (member->select( m | m.oclIsKindOf(PackageableElement) and self.makesVisible(m))->collect(oclAsType(PackageableElement))->asSet())
Name: metaclass_reference_not_specialized
Related element: Profile
Description: An element imported as a metaclassReference is not specialized or generalized in a Profile.
Language: OCL
Formal wording:
metaclassReference.importedElement->
select(c | c.oclIsKindOf(Classifier) and
(c.oclAsType(Classifier).allParents()->collect(namespace)->includes(self)))->isEmpty()
and
packagedElement->
select(oclIsKindOf(Classifier))->collect(oclAsType(Classifier).allParents())->
intersection(metaclassReference.importedElement->select(oclIsKindOf(Classifier))->collect(oclAsType(Classifier)))->isEmpty()
Name: references_same_metamodel
Related element: Profile
Description: All elements imported either as metaclassReferences or through metamodelReferences are members of the same base reference metamodel.
Language: OCL
Formal wording:
metamodelReference.importedPackage.elementImport.importedElement.allOwningPackages()-> union(metaclassReference.importedElement.allOwningPackages() )->notEmpty()
Name: binaryAssociationsOnly
Related element: Stereotype
Description: Stereotypes may only participate in binary associations.
Language: OCL
Formal wording:
ownedAttribute.association->forAll(memberEnd->size()=2)
Name: generalize
Related element: Stereotype
Description: A Stereotype may only generalize or specialize another Stereotype.
Language: OCL
Formal wording:
allParents()->forAll(oclIsKindOf(Stereotype)) and Classifier.allInstances()->forAll(c | c.allParents()->exists(oclIsKindOf(Stereotype)) implies c.oclIsKindOf(Stereotype))
Name: name_not_clash
Related element: Stereotype
Description: Stereotype names should not clash with keyword names for the extended model element.
Name: associationEndOwnership
Related element: Stereotype
Description: Where a stereotype’s property is an association end for an association other than a kind of extension, and the other end is not a stereotype, the other end must be owned by the association itself.
Language: OCL
Formal wording:
ownedAttribute ->select(association->notEmpty() and not association.oclIsKindOf(Extension) and not type.oclIsKindOf(Stereotype)) ->forAll(opposite.owner = association)
Name: base_property_upper_bound
Related element: Stereotype
Description: The upper bound of base-properties is exactly 1.
Name: base_property_multiplicity_single_extension
Related element: Stereotype
Description: If a Stereotype extends only one metaclass, the multiplicity of the corresponding base-property shall be 1..1.
Name: base_property_multiplicity_multiple_extension
Related element: Stereotype
Description: If a Stereotype extends more than one metaclass, the multiplicity of the corresponding base-properties shall be [0..1]. At any point in time, only one of these base-properties can contain a metaclass instance during runtime.
Name: spec
Related element: Stereotype-containingProfile
Language: OCL
Formal wording:
result = (self.namespace.oclAsType(Package).containingProfile())
Name: spec
Related element: Stereotype-profile.1 Stereotype-profile
Language: OCL
Formal wording:
result = (self.containingProfile())
Name: action_referenced
Related element: ActionExecutionSpecification
Description: The Action referenced by the ActionExecutionSpecification must be owned by the Interaction owning that ActionExecutionSpecification.
Language: OCL
Formal wording:
(enclosingInteraction->notEmpty() or enclosingOperand.combinedFragment->notEmpty()) and let parentInteraction : Set(Interaction) = enclosingInteraction.oclAsType(Interaction)->asSet()->union( enclosingOperand.combinedFragment->closure(enclosingOperand.combinedFragment)-> collect(enclosingInteraction).oclAsType(Interaction)->asSet()) in (parentInteraction->size() = 1) and self.action.interaction->asSet() = parentInteraction
Name: break
Related element: CombinedFragment
Description: If the interactionOperator is break, the corresponding InteractionOperand must cover all Lifelines covered by the enclosing InteractionFragment.
Language: OCL
Formal wording:
interactionOperator=InteractionOperatorKind::break implies enclosingInteraction.oclAsType(InteractionFragment)->asSet()->union( enclosingOperand.oclAsType(InteractionFragment)->asSet()).covered->asSet() = self.covered->asSet()
Name: consider_and_ignore
Related element: CombinedFragment
Description: The interaction operators 'consider' and 'ignore' can only be used for the ConsiderIgnoreFragment subtype of CombinedFragment
Language: OCL
Formal wording:
((interactionOperator = InteractionOperatorKind::consider) or (interactionOperator = InteractionOperatorKind::ignore)) implies oclIsKindOf(ConsiderIgnoreFragment)
Name: opt_loop_break_neg
Related element: CombinedFragment
Description: If the interactionOperator is opt, loop, break, assert or neg, there must be exactly one operand.
Language: OCL
Formal wording:
(interactionOperator = InteractionOperatorKind::opt or interactionOperator = InteractionOperatorKind::loop or interactionOperator = InteractionOperatorKind::break or interactionOperator = InteractionOperatorKind::assert or interactionOperator = InteractionOperatorKind::neg) implies operand->size()=1
Name: consider_or_ignore
Related element: ConsiderIgnoreFragment
Description: The interaction operator of a ConsiderIgnoreFragment must be either 'consider' or 'ignore'.
Language: OCL
Formal wording:
(interactionOperator = InteractionOperatorKind::consider) or (interactionOperator = InteractionOperatorKind::ignore)
Name: type
Related element: ConsiderIgnoreFragment
Description: The NamedElements must be of a type of element that can be a signature for a message (i.e.., an Operation, or a Signal).
Language: OCL
Formal wording:
message->forAll(m | m.oclIsKindOf(Operation) or m.oclIsKindOf(Signal))
Name: first_or_last_interaction_fragment
Related element: Continuation
Description: Continuations always occur as the very first InteractionFragment or the very last InteractionFragment of the enclosing InteractionOperand.
Language: OCL
Formal wording:
enclosingOperand->notEmpty() and let peerFragments : OrderedSet(InteractionFragment) = enclosingOperand.fragment in ( peerFragments->notEmpty() and ((peerFragments->first() = self) or (peerFragments->last() = self)))
Name: same_name
Related element: Continuation
Description: Across all Interaction instances having the same context value, every Lifeline instance covered by a Continuation (self) must be common with one covered Lifeline instance of all other Continuation instances with the same name as self, and every Lifeline instance covered by a Continuation instance with the same name as self must be common with one covered Lifeline instance of self. Lifeline instances are common if they have the same selector and represents associationEnd values.
Language: OCL
Formal wording:
enclosingOperand.combinedFragment->notEmpty() and let parentInteraction : Set(Interaction) = enclosingOperand.combinedFragment->closure(enclosingOperand.combinedFragment)-> collect(enclosingInteraction).oclAsType(Interaction)->asSet() in (parentInteraction->size() = 1) and let peerInteractions : Set(Interaction) = (parentInteraction->union(parentInteraction->collect(_'context')->collect(behavior)-> select(oclIsKindOf(Interaction)).oclAsType(Interaction)->asSet())->asSet()) in (peerInteractions->notEmpty()) and let combinedFragments1 : Set(CombinedFragment) = peerInteractions.fragment-> select(oclIsKindOf(CombinedFragment)).oclAsType(CombinedFragment)->asSet() in combinedFragments1->notEmpty() and combinedFragments1->closure(operand.fragment-> select(oclIsKindOf(CombinedFragment)).oclAsType(CombinedFragment))->asSet().operand.fragment-> select(oclIsKindOf(Continuation)).oclAsType(Continuation)->asSet()-> forAll(c : Continuation | (c.name = self.name) implies (c.covered->asSet()->forAll(cl : Lifeline | -- cl must be common to one lifeline covered by self self.covered->asSet()-> select(represents = cl.represents and selector = cl.selector)->asSet()->size()=1)) and (self.covered->asSet()->forAll(cl : Lifeline | -- cl must be common to one lifeline covered by c c.covered->asSet()-> select(represents = cl.represents and selector = cl.selector)->asSet()->size()=1)) )
Name: global
Related element: Continuation
Description: Continuations are always global in the enclosing InteractionFragment e.g., it always covers all Lifelines covered by the enclosing InteractionOperator.
Language: OCL
Formal wording:
enclosingOperand->notEmpty() and
let operandLifelines : Set(Lifeline) = enclosingOperand.covered in
(operandLifelines->notEmpty() and
operandLifelines->forAll(ol :Lifeline |self.covered->includes(ol)))
Name: no_occurrence_specifications_below
Related element: DestructionOccurrenceSpecification
Description: No other OccurrenceSpecifications on a given Lifeline in an InteractionOperand may appear below a DestructionOccurrenceSpecification.
Language: OCL
Formal wording:
let o : InteractionOperand = enclosingOperand in o->notEmpty() and let peerEvents : OrderedSet(OccurrenceSpecification) = covered.events->select(enclosingOperand = o) in peerEvents->last() = self
Name: same_lifeline
Related element: ExecutionSpecification
Description: The startEvent and the finishEvent must be on the same Lifeline.
Language: OCL
Formal wording:
start.covered = finish.covered
Name: actual_gate_matched
Related element: Gate
Description: If this Gate is an actualGate, it must have exactly one matching formalGate within the referred Interaction.
Language: OCL
Formal wording:
interactionUse->notEmpty() implies interactionUse.refersTo.formalGate->select(matches(self))->size()=1
Name: inside_cf_matched
Related element: Gate
Description: If this Gate is inside a CombinedFragment, it must have exactly one matching Gate which is outside of that CombinedFragment.
Language: OCL
Formal wording:
isInsideCF() implies combinedFragment.cfragmentGate->select(isOutsideCF() and matches(self))->size()=1
Name: outside_cf_matched
Related element: Gate
Description: If this Gate is outside an 'alt' CombinedFragment, for every InteractionOperator inside that CombinedFragment there must be exactly one matching Gate inside the CombindedFragment with its opposing end enclosed by that InteractionOperator. If this Gate is outside CombinedFragment with operator other than 'alt', there must be exactly one matching Gate inside that CombinedFragment.
Language: OCL
Formal wording:
isOutsideCF() implies if self.combinedFragment.interactionOperator->asOrderedSet()->first() = InteractionOperatorKind::alt then self.combinedFragment.operand->forAll(op : InteractionOperand | self.combinedFragment.cfragmentGate->select(isInsideCF() and oppositeEnd().enclosingFragment()->includes(self.combinedFragment) and matches(self))->size()=1) else self.combinedFragment.cfragmentGate->select(isInsideCF() and matches(self))->size()=1 endif
Name: formal_gate_distinguishable
Related element: Gate
Description: isFormal() implies that no other formalGate of the parent Interaction returns the same getName() as returned for self
Language: OCL
Formal wording:
isFormal() implies interaction.formalGate->select(getName() = self.getName())->size()=1
Name: actual_gate_distinguishable
Related element: Gate
Description: isActual() implies that no other actualGate of the parent InteractionUse returns the same getName() as returned for self
Language: OCL
Formal wording:
isActual() implies interactionUse.actualGate->select(getName() = self.getName())->size()=1
Name: outside_cf_gate_distinguishable
Related element: Gate
Description: isOutsideCF() implies that no other outside cfragmentGate of the parent CombinedFragment returns the same getName() as returned for self
Language: OCL
Formal wording:
isOutsideCF() implies combinedFragment.cfragmentGate->select(getName() = self.getName())->size()=1
Name: inside_cf_gate_distinguishable
Related element: Gate
Description: isInsideCF() implies that no other inside cfragmentGate attached to a message with its other end in the same InteractionOperator as self, returns the same getName() as returned for self
Language: OCL
Formal wording:
isInsideCF() implies let selfOperand : InteractionOperand = self.getOperand() in combinedFragment.cfragmentGate->select(isInsideCF() and getName() = self.getName())->select(getOperand() = selfOperand)->size()=1
Name: spec
Related element: Gate-isOutsideCF
Language: OCL
Formal wording:
result = (self.oppositeEnd()-> notEmpty() and combinedFragment->notEmpty() implies
let oppEnd : MessageEnd = self.oppositeEnd()->asOrderedSet()->first() in
if oppEnd.oclIsKindOf(MessageOccurrenceSpecification)
then let oppMOS : MessageOccurrenceSpecification = oppEnd.oclAsType(MessageOccurrenceSpecification)
in self.combinedFragment.enclosingInteraction.oclAsType(InteractionFragment)->asSet()->
union(self.combinedFragment.enclosingOperand.oclAsType(InteractionFragment)->asSet()) =
oppMOS.enclosingInteraction.oclAsType(InteractionFragment)->asSet()->
union(oppMOS.enclosingOperand.oclAsType(InteractionFragment)->asSet())
else let oppGate : Gate = oppEnd.oclAsType(Gate)
in self.combinedFragment.enclosingInteraction.oclAsType(InteractionFragment)->asSet()->
union(self.combinedFragment.enclosingOperand.oclAsType(InteractionFragment)->asSet()) =
oppGate.combinedFragment.enclosingInteraction.oclAsType(InteractionFragment)->asSet()->
union(oppGate.combinedFragment.enclosingOperand.oclAsType(InteractionFragment)->asSet())
endif)
Name: spec
Related element: Gate-isInsideCF
Language: OCL
Formal wording:
result = (self.oppositeEnd()-> notEmpty() and combinedFragment->notEmpty() implies let oppEnd : MessageEnd = self.oppositeEnd()->asOrderedSet()->first() in if oppEnd.oclIsKindOf(MessageOccurrenceSpecification) then let oppMOS : MessageOccurrenceSpecification = oppEnd.oclAsType(MessageOccurrenceSpecification) in combinedFragment = oppMOS.enclosingOperand.combinedFragment else let oppGate : Gate = oppEnd.oclAsType(Gate) in combinedFragment = oppGate.combinedFragment.enclosingOperand.combinedFragment endif)
Name: spec
Related element: Gate-isActual
Language: OCL
Formal wording:
result = (interactionUse->notEmpty())
Name: spec
Related element: Gate-isFormal
Description: <p>interaction->notEmpty()</p>
Language: OCL
Formal wording:
result = (interaction->notEmpty())
Name: spec
Related element: Gate-getName
Language: OCL
Formal wording:
result = (if name->notEmpty() then name->asOrderedSet()->first()
else if isActual() or isOutsideCF()
then if isSend()
then 'out_'.concat(self.message.name->asOrderedSet()->first())
else 'in_'.concat(self.message.name->asOrderedSet()->first())
endif
else if isSend()
then 'in_'.concat(self.message.name->asOrderedSet()->first())
else 'out_'.concat(self.message.name->asOrderedSet()->first())
endif
endif
endif)
Name: spec
Related element: Gate-matches
Language: OCL
Formal wording:
result = (self.getName() = gateToMatch.getName() and self.message.messageSort = gateToMatch.message.messageSort and self.message.name = gateToMatch.message.name and self.message.sendEvent->includes(self) implies gateToMatch.message.receiveEvent->includes(gateToMatch) and self.message.receiveEvent->includes(self) implies gateToMatch.message.sendEvent->includes(gateToMatch) and self.message.signature = gateToMatch.message.signature)
Name: spec
Related element: Gate-isDistinguishableFrom
Language: OCL
Formal wording:
result = (true)
Name: spec
Related element: Gate-getOperand
Language: OCL
Formal wording:
result = (if isInsideCF() then
let oppEnd : MessageEnd = self.oppositeEnd()->asOrderedSet()->first() in
if oppEnd.oclIsKindOf(MessageOccurrenceSpecification)
then let oppMOS : MessageOccurrenceSpecification = oppEnd.oclAsType(MessageOccurrenceSpecification)
in oppMOS.enclosingOperand->asOrderedSet()->first()
else let oppGate : Gate = oppEnd.oclAsType(Gate)
in oppGate.combinedFragment.enclosingOperand->asOrderedSet()->first()
endif
else null
endif)
Name: irreflexive_transitive_closure
Related element: GeneralOrdering
Description: An occurrence specification must not be ordered relative to itself through a series of general orderings. (In other words, the transitive closure of the general orderings is irreflexive.)
Language: OCL
Formal wording:
after->closure(toAfter.after)->excludes(before)
Name: not_contained
Related element: Interaction
Description: An Interaction instance must not be contained within another Interaction instance.
Language: OCL
Formal wording:
enclosingInteraction->isEmpty()
Name: minint_maxint
Related element: InteractionConstraint
Description: Minint/maxint can only be present if the InteractionConstraint is associated with the operand of a loop CombinedFragment.
Language: OCL
Formal wording:
maxint->notEmpty() or minint->notEmpty() implies interactionOperand.combinedFragment.interactionOperator = InteractionOperatorKind::loop
Name: minint_non_negative
Related element: InteractionConstraint
Description: If minint is specified, then the expression must evaluate to a non-negative integer.
Language: OCL
Formal wording:
minint->notEmpty() implies minint->asSequence()->first().integerValue() >= 0
Name: maxint_positive
Related element: InteractionConstraint
Description: If maxint is specified, then the expression must evaluate to a positive integer.
Language: OCL
Formal wording:
maxint->notEmpty() implies maxint->asSequence()->first().integerValue() > 0
Name: dynamic_variables
Related element: InteractionConstraint
Description: The dynamic variables that take part in the constraint must be owned by the ConnectableElement corresponding to the covered Lifeline.
Name: global_data
Related element: InteractionConstraint
Description: The constraint may contain references to global data or write-once data.
Name: maxint_greater_equal_minint
Related element: InteractionConstraint
Description: If maxint is specified, then minint must be specified and the evaluation of maxint must be >= the evaluation of minint.
Language: OCL
Formal wording:
maxint->notEmpty() implies (minint->notEmpty() and maxint->asSequence()->first().integerValue() >= minint->asSequence()->first().integerValue() )
Name: guard_contain_references
Related element: InteractionOperand
Description: The guard must contain only references to values local to the Lifeline on which it resides, or values global to the whole Interaction.
Name: guard_directly_prior
Related element: InteractionOperand
Description: The guard must be placed directly prior to (above) the OccurrenceSpecification that will become the first OccurrenceSpecification within this InteractionOperand.
Name: gates_match
Related element: InteractionUse
Description: Actual Gates of the InteractionUse must match Formal Gates of the referred Interaction. Gates match when their names are equal and their messages correspond.
Language: OCL
Formal wording:
actualGate->notEmpty() implies refersTo.formalGate->forAll( fg : Gate | self.actualGate->select(matches(fg))->size()=1) and self.actualGate->forAll(ag : Gate | refersTo.formalGate->select(matches(ag))->size()=1)
Name: arguments_are_constants
Related element: InteractionUse
Description: The arguments must only be constants, parameters of the enclosing Interaction or attributes of the classifier owning the enclosing Interaction.
Name: returnValueRecipient_coverage
Related element: InteractionUse
Description: The returnValueRecipient must be a Property of a ConnectableElement that is represented by a Lifeline covered by this InteractionUse.
Language: OCL
Formal wording:
returnValueRecipient->asSet()->notEmpty() implies let covCE : Set(ConnectableElement) = covered.represents->asSet() in covCE->notEmpty() and let classes:Set(Classifier) = covCE.type.oclIsKindOf(Classifier).oclAsType(Classifier)->asSet() in let allProps : Set(Property) = classes.attribute->union(classes.allParents().attribute)->asSet() in allProps->includes(returnValueRecipient)
Name: arguments_correspond_to_parameters
Related element: InteractionUse
Description: The arguments of the InteractionUse must correspond to parameters of the referred Interaction.
Name: returnValue_type_recipient_correspondence
Related element: InteractionUse
Description: The type of the returnValue must correspond to the type of the returnValueRecipient.
Language: OCL
Formal wording:
returnValue.type->asSequence()->notEmpty() implies returnValue.type->asSequence()->first() = returnValueRecipient.type->asSequence()->first()
Name: all_lifelines
Related element: InteractionUse
Description: The InteractionUse must cover all Lifelines of the enclosing Interaction that are common with the lifelines covered by the referred Interaction. Lifelines are common if they have the same selector and represents associationEnd values.
Language: OCL
Formal wording:
let parentInteraction : Set(Interaction) = enclosingInteraction->asSet()-> union(enclosingOperand.combinedFragment->closure(enclosingOperand.combinedFragment)-> collect(enclosingInteraction).oclAsType(Interaction)->asSet()) in parentInteraction->size()=1 and let refInteraction : Interaction = refersTo in parentInteraction.covered-> forAll(intLifeline : Lifeline | refInteraction.covered-> forAll( refLifeline : Lifeline | refLifeline.represents = intLifeline.represents and ( ( refLifeline.selector.oclIsKindOf(LiteralString) implies intLifeline.selector.oclIsKindOf(LiteralString) and refLifeline.selector.oclAsType(LiteralString).value = intLifeline.selector.oclAsType(LiteralString).value ) and ( refLifeline.selector.oclIsKindOf(LiteralInteger) implies intLifeline.selector.oclIsKindOf(LiteralInteger) and refLifeline.selector.oclAsType(LiteralInteger).value = intLifeline.selector.oclAsType(LiteralInteger).value ) ) implies self.covered->asSet()->includes(intLifeline)))
Name: selector_specified
Related element: Lifeline
Description: The selector for a Lifeline must only be specified if the referenced Part is multivalued.
Language: OCL
Formal wording:
self.selector->notEmpty() = (self.represents.oclIsKindOf(MultiplicityElement) and self.represents.oclAsType(MultiplicityElement).isMultivalued())
Name: interaction_uses_share_lifeline
Related element: Lifeline
Description: If a lifeline is in an Interaction referred to by an InteractionUse in an enclosing Interaction, and that lifeline is common with another lifeline in an Interaction referred to by another InteractonUse within that same enclosing Interaction, it must be common to a lifeline within that enclosing Interaction. By common Lifelines we mean Lifelines with the same selector and represents associations.
Language: OCL
Formal wording:
let intUses : Set(InteractionUse) = interaction.interactionUse in
intUses->forAll
( iuse : InteractionUse |
let usingInteraction : Set(Interaction) = iuse.enclosingInteraction->asSet()
->union(
iuse.enclosingOperand.combinedFragment->asSet()->closure(enclosingOperand.combinedFragment).enclosingInteraction->asSet()
)
in
let peerUses : Set(InteractionUse) = usingInteraction.fragment->select(oclIsKindOf(InteractionUse)).oclAsType(InteractionUse)->asSet()
->union(
usingInteraction.fragment->select(oclIsKindOf(CombinedFragment)).oclAsType(CombinedFragment)->asSet()
->closure(operand.fragment->select(oclIsKindOf(CombinedFragment)).oclAsType(CombinedFragment)).operand.fragment->
select(oclIsKindOf(InteractionUse)).oclAsType(InteractionUse)->asSet()
)->excluding(iuse)
in
peerUses->forAll( peerUse : InteractionUse |
peerUse.refersTo.lifeline->forAll( l : Lifeline | (l.represents = self.represents and
( self.selector.oclIsKindOf(LiteralString) implies
l.selector.oclIsKindOf(LiteralString) and
self.selector.oclAsType(LiteralString).value = l.selector.oclAsType(LiteralString).value )
and
( self.selector.oclIsKindOf(LiteralInteger) implies
l.selector.oclIsKindOf(LiteralInteger) and
self.selector.oclAsType(LiteralInteger).value = l.selector.oclAsType(LiteralInteger).value )
)
implies
usingInteraction.lifeline->select(represents = self.represents and
( self.selector.oclIsKindOf(LiteralString) implies
l.selector.oclIsKindOf(LiteralString) and
self.selector.oclAsType(LiteralString).value = l.selector.oclAsType(LiteralString).value )
and
( self.selector.oclIsKindOf(LiteralInteger) implies
l.selector.oclIsKindOf(LiteralInteger) and
self.selector.oclAsType(LiteralInteger).value = l.selector.oclAsType(LiteralInteger).value )
)
)
)
)
Name: same_classifier
Related element: Lifeline
Description: The classifier containing the referenced ConnectableElement must be the same classifier, or an ancestor, of the classifier that contains the interaction enclosing this lifeline.
Language: OCL
Formal wording:
represents.namespace->closure(namespace)->includes(interaction._'context')
Name: selector_int_or_string
Related element: Lifeline
Description: The selector value, if present, must be a LiteralString or a LiteralInteger
Language: OCL
Formal wording:
self.selector->notEmpty() implies self.selector.oclIsKindOf(LiteralInteger) or self.selector.oclIsKindOf(LiteralString)
Name: sending_receiving_message_event
Related element: Message
Description: If the sendEvent and the receiveEvent of the same Message are on the same Lifeline, the sendEvent must be ordered before the receiveEvent.
Language: OCL
Formal wording:
receiveEvent.oclIsKindOf(MessageOccurrenceSpecification) implies let f : Lifeline = sendEvent->select(oclIsKindOf(MessageOccurrenceSpecification)).oclAsType(MessageOccurrenceSpecification)->asOrderedSet()->first().covered in f = receiveEvent->select(oclIsKindOf(MessageOccurrenceSpecification)).oclAsType(MessageOccurrenceSpecification)->asOrderedSet()->first().covered implies f.events->indexOf(sendEvent.oclAsType(MessageOccurrenceSpecification)->asOrderedSet()->first() ) < f.events->indexOf(receiveEvent.oclAsType(MessageOccurrenceSpecification)->asOrderedSet()->first() )
Name: arguments
Related element: Message
Description: Arguments of a Message must only be: i) attributes of the sending lifeline, ii) constants, iii) symbolic values (which are wildcard values representing any legal value), iv) explicit parameters of the enclosing Interaction, v) attributes of the class owning the Interaction.
Name: cannot_cross_boundaries
Related element: Message
Description: Messages cannot cross boundaries of CombinedFragments or their operands. This is true if and only if both MessageEnds are enclosed within the same InteractionFragment (i.e., an InteractionOperand or an Interaction).
Language: OCL
Formal wording:
sendEvent->notEmpty() and receiveEvent->notEmpty() implies let sendEnclosingFrag : Set(InteractionFragment) = sendEvent->asOrderedSet()->first().enclosingFragment() in let receiveEnclosingFrag : Set(InteractionFragment) = receiveEvent->asOrderedSet()->first().enclosingFragment() in sendEnclosingFrag = receiveEnclosingFrag
Name: signature_is_signal
Related element: Message
Description: In the case when the Message signature is a Signal, the arguments of the Message must correspond to the attributes of the Signal. A Message Argument corresponds to a Signal Attribute if the Argument is of the same Class or a specialization of that of the Attribute.
Language: OCL
Formal wording:
(messageSort = MessageSort::asynchSignal ) and signature.oclIsKindOf(Signal) implies
let signalAttributes : OrderedSet(Property) = signature.oclAsType(Signal).inheritedMember()->
select(n:NamedElement | n.oclIsTypeOf(Property))->collect(oclAsType(Property))->asOrderedSet()
in signalAttributes->size() = self.argument->size()
and self.argument->forAll( o: ValueSpecification |
not (o.oclIsKindOf(Expression)
and o.oclAsType(Expression).symbol->size()=0
and o.oclAsType(Expression).operand->isEmpty() ) implies
let p : Property = signalAttributes->at(self.argument->indexOf(o))
in o.type.oclAsType(Classifier).conformsTo(p.type.oclAsType(Classifier)))
Name: occurrence_specifications
Related element: Message
Description: If the MessageEnds are both OccurrenceSpecifications, then the connector must go between the Parts represented by the Lifelines of the two MessageEnds.
Name: signature_refer_to
Related element: Message
Description: The signature must either refer an Operation (in which case messageSort is either synchCall or asynchCall or reply) or a Signal (in which case messageSort is asynchSignal). The name of the NamedElement referenced by signature must be the same as that of the Message.
Language: OCL
Formal wording:
signature->notEmpty() implies ((signature.oclIsKindOf(Operation) and (messageSort = MessageSort::asynchCall or messageSort = MessageSort::synchCall or messageSort = MessageSort::reply) ) or (signature.oclIsKindOf(Signal) and messageSort = MessageSort::asynchSignal ) ) and name = signature.name
Name: signature_is_operation_request
Related element: Message
Description: In the case when a Message with messageSort synchCall or asynchCall has a non empty Operation signature, the arguments of the Message must correspond to the in and inout parameters of the Operation. A Parameter corresponds to an Argument if the Argument is of the same Class or a specialization of that of the Parameter.
Language: OCL
Formal wording:
(messageSort = MessageSort::asynchCall or messageSort = MessageSort::synchCall) and signature.oclIsKindOf(Operation) implies let requestParms : OrderedSet(Parameter) = signature.oclAsType(Operation).ownedParameter-> select(direction = ParameterDirectionKind::inout or direction = ParameterDirectionKind::_'in' ) in requestParms->size() = self.argument->size() and self.argument->forAll( o: ValueSpecification | not (o.oclIsKindOf(Expression) and o.oclAsType(Expression).symbol->size()=0 and o.oclAsType(Expression).operand->isEmpty() ) implies let p : Parameter = requestParms->at(self.argument->indexOf(o)) in o.type.oclAsType(Classifier).conformsTo(p.type.oclAsType(Classifier)) )
Name: signature_is_operation_reply
Related element: Message
Description: In the case when a Message with messageSort reply has a non empty Operation signature, the arguments of the Message must correspond to the out, inout, and return parameters of the Operation. A Parameter corresponds to an Argument if the Argument is of the same Class or a specialization of that of the Parameter.
Language: OCL
Formal wording:
(messageSort = MessageSort::reply) and signature.oclIsKindOf(Operation) implies let replyParms : OrderedSet(Parameter) = signature.oclAsType(Operation).ownedParameter-> select(direction = ParameterDirectionKind::inout or direction = ParameterDirectionKind::out or direction = ParameterDirectionKind::return) in replyParms->size() = self.argument->size() and self.argument->forAll( o: ValueSpecification | o.oclIsKindOf(Expression) and let e : Expression = o.oclAsType(Expression) in e.operand->notEmpty() implies let p : Parameter = replyParms->at(self.argument->indexOf(o)) in e.operand->asSequence()->first().type.oclAsType(Classifier).conformsTo(p.type.oclAsType(Classifier)) )
Name: spec
Related element: Message-messageKind.1 Message-messageKind
Language: OCL
Formal wording:
result = (messageKind)
Name: spec
Related element: Message-isDistinguishableFrom
Language: OCL
Formal wording:
result = (true)
Name: spec
Related element: MessageEnd-oppositeEnd
Language: OCL
Formal wording:
result = (message->asSet().messageEnd->asSet()->excluding(self))
Name: pre
Related element: MessageEnd-oppositeEnd
Language: OCL
Formal wording:
message->notEmpty()
Name: pre
Related element: MessageEnd-isSend
Language: OCL
Formal wording:
message->notEmpty()
Name: spec
Related element: MessageEnd-isSend
Language: OCL
Formal wording:
result = (message.sendEvent->asSet()->includes(self))
Name: pre
Related element: MessageEnd-isReceive
Description: <p>message->notEmpty()</p>
Language: OCL
Formal wording:
message->notEmpty()
Name: spec
Related element: MessageEnd-isReceive
Language: OCL
Formal wording:
result = (message.receiveEvent->asSet()->includes(self))
Name: spec
Related element: MessageEnd-enclosingFragment
Language: OCL
Formal wording:
result = (if self->select(oclIsKindOf(Gate))->notEmpty()
then -- it is a Gate
let endGate : Gate =
self->select(oclIsKindOf(Gate)).oclAsType(Gate)->asOrderedSet()->first()
in
if endGate.isOutsideCF()
then endGate.combinedFragment.enclosingInteraction.oclAsType(InteractionFragment)->asSet()->
union(endGate.combinedFragment.enclosingOperand.oclAsType(InteractionFragment)->asSet())
else if endGate.isInsideCF()
then endGate.combinedFragment.oclAsType(InteractionFragment)->asSet()
else if endGate.isFormal()
then endGate.interaction.oclAsType(InteractionFragment)->asSet()
else if endGate.isActual()
then endGate.interactionUse.enclosingInteraction.oclAsType(InteractionFragment)->asSet()->
union(endGate.interactionUse.enclosingOperand.oclAsType(InteractionFragment)->asSet())
else null
endif
endif
endif
endif
else -- it is a MessageOccurrenceSpecification
let endMOS : MessageOccurrenceSpecification =
self->select(oclIsKindOf(MessageOccurrenceSpecification)).oclAsType(MessageOccurrenceSpecification)->asOrderedSet()->first()
in
if endMOS.enclosingInteraction->notEmpty()
then endMOS.enclosingInteraction.oclAsType(InteractionFragment)->asSet()
else endMOS.enclosingOperand.oclAsType(InteractionFragment)->asSet()
endif
endif)
Name: commutativity_of_decomposition
Related element: PartDecomposition
Description: Assume that within Interaction X, Lifeline L is of class C and decomposed to D. Assume also that there is within X an InteractionUse (say) U that covers L. According to the constraint above U will have a counterpart CU within D. Within the Interaction referenced by U, L should also be decomposed, and the decomposition should reference CU. (This rule is called commutativity of decomposition.)
Name: assume
Related element: PartDecomposition
Description: Assume that within Interaction X, Lifeline L is of class C and decomposed to D. Within X there is a sequence of constructs along L (such constructs are CombinedFragments, InteractionUse and (plain) OccurrenceSpecifications). Then a corresponding sequence of constructs must appear within D, matched one-to-one in the same order. i) CombinedFragment covering L are matched with an extra-global CombinedFragment in D. ii) An InteractionUse covering L is matched with a global (i.e., covering all Lifelines) InteractionUse in D. iii) A plain OccurrenceSpecification on L is considered an actualGate that must be matched by a formalGate of D.
Name: parts_of_internal_structures
Related element: PartDecomposition
Description: PartDecompositions apply only to Parts that are Parts of Internal Structures not to Parts of Collaborations.
Name: must_conform
Related element: InformationFlow
Description: The sources and targets of the information flow must conform to the sources and targets or conversely the targets and sources of the realization relationships.
Name: sources_and_targets_kind
Related element: InformationFlow
Description: The sources and targets of the information flow can only be one of the following kind: Actor, Node, UseCase, Artifact, Class, Component, Port, Property, Interface, Package, ActivityNode, ActivityPartition, Behavior and InstanceSpecification except when its classifier is a relationship (i.e. it represents a link).
Language: OCL
Formal wording:
(self.informationSource->forAll( sis | oclIsKindOf(Actor) or oclIsKindOf(Node) or oclIsKindOf(UseCase) or oclIsKindOf(Artifact) or oclIsKindOf(Class) or oclIsKindOf(Component) or oclIsKindOf(Port) or oclIsKindOf(Property) or oclIsKindOf(Interface) or oclIsKindOf(Package) or oclIsKindOf(ActivityNode) or oclIsKindOf(ActivityPartition) or (oclIsKindOf(InstanceSpecification) and not sis.oclAsType(InstanceSpecification).classifier->exists(oclIsKindOf(Relationship))))) and (self.informationTarget->forAll( sit | oclIsKindOf(Actor) or oclIsKindOf(Node) or oclIsKindOf(UseCase) or oclIsKindOf(Artifact) or oclIsKindOf(Class) or oclIsKindOf(Component) or oclIsKindOf(Port) or oclIsKindOf(Property) or oclIsKindOf(Interface) or oclIsKindOf(Package) or oclIsKindOf(ActivityNode) or oclIsKindOf(ActivityPartition) or (oclIsKindOf(InstanceSpecification) and not sit.oclAsType(InstanceSpecification).classifier->exists(oclIsKindOf(Relationship)))))
Name: convey_classifiers
Related element: InformationFlow
Description: An information flow can only convey classifiers that are allowed to represent an information item.
Language: OCL
Formal wording:
self.conveyed->forAll(oclIsKindOf(Class) or oclIsKindOf(Interface) or oclIsKindOf(InformationItem) or oclIsKindOf(Signal) or oclIsKindOf(Component))
Name: sources_and_targets
Related element: InformationItem
Description: The sources and targets of an information item (its related information flows) must designate subsets of the sources and targets of the representation information item, if any. The Classifiers that can realize an information item can only be of the following kind: Class, Interface, InformationItem, Signal, Component.
Language: OCL
Formal wording:
(self.represented->select(oclIsKindOf(InformationItem))->forAll(p |
p.conveyingFlow.source->forAll(q | self.conveyingFlow.source->includes(q)) and
p.conveyingFlow.target->forAll(q | self.conveyingFlow.target->includes(q)))) and
(self.represented->forAll(oclIsKindOf(Class) or oclIsKindOf(Interface) or
oclIsKindOf(InformationItem) or oclIsKindOf(Signal) or oclIsKindOf(Component)))
Name: has_no
Related element: InformationItem
Description: An informationItem has no feature, no generalization, and no associations.
Language: OCL
Formal wording:
self.generalization->isEmpty() and self.feature->isEmpty()
Name: not_instantiable
Related element: InformationItem
Description: It is not instantiable.
Language: OCL
Formal wording:
isAbstract
Name: association_ends
Related element: CommunicationPath
Description: The association ends of a CommunicationPath are typed by DeploymentTargets.
Language: OCL
Formal wording:
endType->forAll (oclIsKindOf(DeploymentTarget))
Name: deployment_target
Related element: DeploymentSpecification
Description: The DeploymentTarget of a DeploymentSpecification is a kind of ExecutionEnvironment.
Language: OCL
Formal wording:
deployment->forAll (location.oclIsKindOf(ExecutionEnvironment))
Name: deployed_elements
Related element: DeploymentSpecification
Description: The deployedElements of a DeploymentTarget that are involved in a Deployment that has an associated Deployment-Specification is a kind of Component (i.e., the configured components).
Language: OCL
Formal wording:
deployment->forAll (location.deployedElement->forAll (oclIsKindOf(Component)))
Name: spec
Related element: DeploymentTarget-deployedElement.1 DeploymentTarget-deployedElement
Language: OCL
Formal wording:
result = (deployment.deployedArtifact->select(oclIsKindOf(Artifact))->collect(oclAsType(Artifact).manifestation)->collect(utilizedElement)->asSet())
Name: internal_structure
Related element: Node
Description: The internal structure of a Node (if defined) consists solely of parts of type Node.
Language: OCL
Formal wording:
part->forAll(oclIsKindOf(Node))
Name: boolean_value
Related element: Constraint
Description: The ValueSpecification for a Constraint must evaluate to a Boolean value.
Name: no_side_effects
Related element: Constraint
Description: Evaluating the ValueSpecification for a Constraint must not have side effects.
Name: not_apply_to_self
Related element: Constraint
Description: A Constraint cannot be applied to itself.
Language: OCL
Formal wording:
not constrainedElement->includes(self)
Name: has_owner
Related element: Element
Description: Elements that must be owned must have an owner.
Language: OCL
Formal wording:
mustBeOwned() implies owner->notEmpty()
Name: not_own_self
Related element: Element
Description: An element may not directly or indirectly own itself.
Language: OCL
Formal wording:
not allOwnedElements()->includes(self)
Name: spec
Related element: Element-allOwnedElements
Language: OCL
Formal wording:
result = (ownedElement->union(ownedElement->collect(e | e.allOwnedElements()))->asSet())
Name: spec
Related element: Element-mustBeOwned
Language: OCL
Formal wording:
result = (true)
Name: imported_element_is_public
Related element: ElementImport
Description: An importedElement has either public visibility or no visibility at all.
Language: OCL
Formal wording:
importedElement.visibility <> null implies importedElement.visibility = VisibilityKind::public
Name: visibility_public_or_private
Related element: ElementImport
Description: The visibility of an ElementImport is either public or private.
Language: OCL
Formal wording:
visibility = VisibilityKind::public or visibility = VisibilityKind::private
Name: spec
Related element: ElementImport-getName
Language: OCL
Formal wording:
result = (if alias->notEmpty() then alias else importedElement.name endif)
Name: upper_ge_lower
Related element: MultiplicityElement
Description: The upper bound must be greater than or equal to the lower bound.
Language: OCL
Formal wording:
upperBound() >= lowerBound()
Name: lower_ge_0
Related element: MultiplicityElement
Description: The lower bound must be a non-negative integer literal.
Language: OCL
Formal wording:
lowerBound() >= 0
Name: value_specification_no_side_effects
Related element: MultiplicityElement
Description: If a non-literal ValueSpecification is used for lowerValue or upperValue, then evaluating that specification must not have side effects.
Name: value_specification_constant
Related element: MultiplicityElement
Description: If a non-literal ValueSpecification is used for lowerValue or upperValue, then that specification must be a constant expression.
Name: lower_is_integer
Related element: MultiplicityElement
Description: If it is not empty, then lowerValue must have an Integer value.
Language: OCL
Formal wording:
lowerValue <> null implies lowerValue.integerValue() <> null
Name: upper_is_unlimitedNatural
Related element: MultiplicityElement
Description: If it is not empty, then upperValue must have an UnlimitedNatural value.
Language: OCL
Formal wording:
upperValue <> null implies upperValue.unlimitedValue() <> null
Name: spec
Related element: MultiplicityElement-compatibleWith
Language: OCL
Formal wording:
result = ((other.lowerBound() <= self.lowerBound()) and ((other.upperBound() = *) or (self.upperBound() <= other.upperBound())))
Name: pre
Related element: MultiplicityElement-includesMultiplicity
Language: OCL
Formal wording:
self.upperBound()->notEmpty() and self.lowerBound()->notEmpty() and M.upperBound()->notEmpty() and M.lowerBound()->notEmpty()
Name: spec
Related element: MultiplicityElement-includesMultiplicity
Language: OCL
Formal wording:
result = ((self.lowerBound() <= M.lowerBound()) and (self.upperBound() >= M.upperBound()))
Name: spec
Related element: MultiplicityElement-is
Language: OCL
Formal wording:
result = (lowerbound = self.lowerBound() and upperbound = self.upperBound())
Name: pre
Related element: MultiplicityElement-isMultivalued
Language: OCL
Formal wording:
upperBound()->notEmpty()
Name: spec
Related element: MultiplicityElement-isMultivalued
Language: OCL
Formal wording:
result = (upperBound() > 1)
Name: spec
Related element: MultiplicityElement-lower.1 MultiplicityElement-lower
Language: OCL
Formal wording:
result = (lowerBound())
Name: spec
Related element: MultiplicityElement-lowerBound
Language: OCL
Formal wording:
result = (if (lowerValue=null or lowerValue.integerValue()=null) then 1 else lowerValue.integerValue() endif)
Name: spec
Related element: MultiplicityElement-upper.1 MultiplicityElement-upper
Language: OCL
Formal wording:
result = (upperBound())
Name: spec
Related element: MultiplicityElement-upperBound
Language: OCL
Formal wording:
result = (if (upperValue=null or upperValue.unlimitedValue()=null) then 1 else upperValue.unlimitedValue() endif)
Name: visibility_needs_ownership
Related element: NamedElement
Description: If a NamedElement is owned by something other than a Namespace, it does not have a visibility. One that is not owned by anything (and hence must be a Package, as this is the only kind of NamedElement that overrides mustBeOwned()) may have a visibility.
Language: OCL
Formal wording:
(namespace = null and owner <> null) implies visibility = null
Name: has_qualified_name
Related element: NamedElement
Description: When there is a name, and all of the containing Namespaces have a name, the qualifiedName is constructed from the name of the NamedElement and the names of the containing Namespaces.
Language: OCL
Formal wording:
(name <> null and allNamespaces()->select(ns | ns.name = null)->isEmpty()) implies qualifiedName = allNamespaces()->iterate( ns : Namespace; agg: String = name | ns.name.concat(self.separator()).concat(agg))
Name: has_no_qualified_name
Related element: NamedElement
Description: If there is no name, or one of the containing Namespaces has no name, there is no qualifiedName.
Language: OCL
Formal wording:
name=null or allNamespaces()->select( ns | ns.name=null )->notEmpty() implies qualifiedName = null
Name: spec
Related element: NamedElement-allNamespaces
Language: OCL
Formal wording:
result = (if owner.oclIsKindOf(TemplateParameter) and
owner.oclAsType(TemplateParameter).signature.template.oclIsKindOf(Namespace) then
let enclosingNamespace : Namespace =
owner.oclAsType(TemplateParameter).signature.template.oclAsType(Namespace) in
enclosingNamespace.allNamespaces()->prepend(enclosingNamespace)
else
if namespace->isEmpty()
then OrderedSet{}
else
namespace.allNamespaces()->prepend(namespace)
endif
endif)
Name: spec
Related element: NamedElement-allOwningPackages
Language: OCL
Formal wording:
result = (if namespace.oclIsKindOf(Package)
then
let owningPackage : Package = namespace.oclAsType(Package) in
owningPackage->union(owningPackage.allOwningPackages())
else
null
endif)
Name: spec
Related element: NamedElement-isDistinguishableFrom
Language: OCL
Formal wording:
result = ((self.oclIsKindOf(n.oclType()) or n.oclIsKindOf(self.oclType())) implies
ns.getNamesOfMember(self)->intersection(ns.getNamesOfMember(n))->isEmpty()
)
Name: spec
Related element: NamedElement-qualifiedName.1 NamedElement-qualifiedName
Language: OCL
Formal wording:
result = (if self.name <> null and self.allNamespaces()->select( ns | ns.name=null )->isEmpty()
then
self.allNamespaces()->iterate( ns : Namespace; agg: String = self.name | ns.name.concat(self.separator()).concat(agg))
else
null
endif)
Name: spec
Related element: NamedElement-separator
Language: OCL
Formal wording:
result = ('::')
Name: spec
Related element: NamedElement-clientDependency.1 NamedElement-clientDependency
Language: OCL
Formal wording:
result = (Dependency.allInstances()->select(d | d.client->includes(self)))
Name: members_distinguishable
Related element: Namespace
Description: All the members of a Namespace are distinguishable within it.
Language: OCL
Formal wording:
membersAreDistinguishable()
Name: cannot_import_self
Related element: Namespace
Description: A Namespace cannot have a PackageImport to itself.
Language: OCL
Formal wording:
packageImport.importedPackage.oclAsType(Namespace)->excludes(self)
Name: cannot_import_ownedMembers
Related element: Namespace
Description: A Namespace cannot have an ElementImport to one of its ownedMembers.
Language: OCL
Formal wording:
elementImport.importedElement.oclAsType(Element)->excludesAll(ownedMember)
Name: spec
Related element: Namespace-excludeCollisions
Language: OCL
Formal wording:
result = (imps->reject(imp1 | imps->exists(imp2 | not imp1.isDistinguishableFrom(imp2, self))))
Name: spec
Related element: Namespace-getNamesOfMember
Language: OCL
Formal wording:
result = (if self.ownedMember ->includes(element)
then Set{element.name}
else let elementImports : Set(ElementImport) = self.elementImport->select(ei | ei.importedElement = element) in
if elementImports->notEmpty()
then
elementImports->collect(el | el.getName())->asSet()
else
self.packageImport->select(pi | pi.importedPackage.visibleMembers().oclAsType(NamedElement)->includes(element))-> collect(pi | pi.importedPackage.getNamesOfMember(element))->asSet()
endif
endif)
Name: spec
Related element: Namespace-importMembers
Language: OCL
Formal wording:
result = (self.excludeCollisions(imps)->select(imp | self.ownedMember->forAll(mem | imp.isDistinguishableFrom(mem, self))))
Name: spec
Related element: Namespace-importedMember.1 Namespace-importedMember
Language: OCL
Formal wording:
result = (self.importMembers(elementImport.importedElement->asSet()->union(packageImport.importedPackage->collect(p | p.visibleMembers()))->asSet()))
Name: spec
Related element: Namespace-membersAreDistinguishable
Language: OCL
Formal wording:
result = (member->forAll( memb |
member->excluding(memb)->forAll(other |
memb.isDistinguishableFrom(other, self))))
Name: namespace_needs_visibility
Related element: PackageableElement
Description: A PackageableElement owned by a Namespace must have a visibility.
Language: OCL
Formal wording:
visibility = null implies namespace = null
Name: public_or_private
Related element: PackageImport
Description: The visibility of a PackageImport is either public or private.
Language: OCL
Formal wording:
visibility = VisibilityKind::public or visibility = VisibilityKind::private
Name: spec
Related element: ParameterableElement-isCompatibleWith
Language: OCL
Formal wording:
result = (self.oclIsKindOf(p.oclType()))
Name: spec
Related element: ParameterableElement-isTemplateParameter
Language: OCL
Formal wording:
result = (templateParameter->notEmpty())
Name: spec
Related element: TemplateableElement-isTemplate
Language: OCL
Formal wording:
result = (ownedTemplateSignature <> null)
Name: spec
Related element: TemplateableElement-parameterableElements
Language: OCL
Formal wording:
result = (self.allOwnedElements()->select(oclIsKindOf(ParameterableElement)).oclAsType(ParameterableElement)->asSet())
Name: parameter_substitution_formal
Related element: TemplateBinding
Description: Each parameterSubstitution must refer to a formal TemplateParameter of the target TemplateSignature.
Language: OCL
Formal wording:
parameterSubstitution->forAll(b | signature.parameter->includes(b.formal))
Name: one_parameter_substitution
Related element: TemplateBinding
Description: A TemplateBiinding contains at most one TemplateParameterSubstitution for each formal TemplateParameter of the target TemplateSignature.
Language: OCL
Formal wording:
signature.parameter->forAll(p | parameterSubstitution->select(b | b.formal = p)->size() <= 1)
Name: must_be_compatible
Related element: TemplateParameter
Description: The default must be compatible with the formal TemplateParameter.
Language: OCL
Formal wording:
default <> null implies default.isCompatibleWith(parameteredElement)
Name: must_be_compatible
Related element: TemplateParameterSubstitution
Description: The actual ParameterableElement must be compatible with the formal TemplateParameter, e.g., the actual ParameterableElement for a Class TemplateParameter must be a Class.
Language: OCL
Formal wording:
actual->forAll(a | a.isCompatibleWith(formal.parameteredElement))
Name: own_elements
Related element: TemplateSignature
Description: Parameters must own the ParameterableElements they parameter or those ParameterableElements must be owned by the TemplateableElement being templated.
Language: OCL
Formal wording:
template.ownedElement->includesAll(parameter.parameteredElement->asSet() - parameter.ownedParameteredElement->asSet())
Name: unique_parameters
Related element: TemplateSignature
Description: The names of the parameters of a TemplateSignature are unique.
Language: OCL
Formal wording:
parameter->forAll( p1, p2 | (p1 <> p2 and p1.parameteredElement.oclIsKindOf(NamedElement) and p2.parameteredElement.oclIsKindOf(NamedElement) ) implies p1.parameteredElement.oclAsType(NamedElement).name <> p2.parameteredElement.oclAsType(NamedElement).name)
Name: spec
Related element: Type-conformsTo
Language: OCL
Formal wording:
result = (false)
Name: most_one_behavior
Related element: Behavior
Description: There may be at most one Behavior for a given pairing of BehavioredClassifier (as owner of the Behavior) and BehavioralFeature (as specification of the Behavior).
Language: OCL
Formal wording:
specification <> null implies _'context'.ownedBehavior->select(specification=self.specification)->size() = 1
Name: parameters_match
Related element: Behavior
Description: If a Behavior has a specification BehavioralFeature, then it must have the same number of ownedParameters as its specification. The Behavior Parameters must also "match" the BehavioralParameter Parameters, but the exact requirements for this matching are not formalized.
Language: OCL
Formal wording:
specification <> null implies ownedParameter->size() = specification.ownedParameter->size()
Name: feature_of_context_classifier
Related element: Behavior
Description: The specification BehavioralFeature must be a feature (possibly inherited) of the context BehavioredClassifier of the Behavior.
Language: OCL
Formal wording:
_'context'.feature->includes(specification)
Name: spec
Related element: Behavior-context.1 Behavior-context
Language: OCL
Formal wording:
result = (if nestingClass <> null then
null
else
let b:BehavioredClassifier = self.behavioredClassifier(self.owner) in
if b.oclIsKindOf(Behavior) and b.oclAsType(Behavior)._'context' <> null then
b.oclAsType(Behavior)._'context'
else
b
endif
endif
)
Name: spec
Related element: Behavior-behavioredClassifier
Language: OCL
Formal wording:
if from.oclIsKindOf(BehavioredClassifier) then
from.oclAsType(BehavioredClassifier)
else if from.owner = null then
null
else
self.behavioredClassifier(from.owner)
endif
endif
Name: spec
Related element: Behavior-inputParameters
Language: OCL
Formal wording:
result = (ownedParameter->select(direction=ParameterDirectionKind::_'in' or direction=ParameterDirectionKind::inout))
Name: spec
Related element: Behavior-outputParameters
Language: OCL
Formal wording:
result = (ownedParameter->select(direction=ParameterDirectionKind::out or direction=ParameterDirectionKind::inout or direction=ParameterDirectionKind::return))
Name: one_output_parameter
Related element: FunctionBehavior
Description: A FunctionBehavior has at least one output Parameter.
Language: OCL
Formal wording:
self.ownedParameter-> select(p | p.direction = ParameterDirectionKind::out or p.direction= ParameterDirectionKind::inout or p.direction= ParameterDirectionKind::return)->size() >= 1
Name: types_of_parameters
Related element: FunctionBehavior
Description: The types of the ownedParameters are all DataTypes, which may not nest anything but other DataTypes.
Language: OCL
Formal wording:
ownedParameter->forAll(p | p.type <> null and p.type.oclIsTypeOf(DataType) and hasAllDataTypeAttributes(p.type.oclAsType(DataType)))
Name: spec
Related element: FunctionBehavior-hasAllDataTypeAttributes
Language: OCL
Formal wording:
result = (d.ownedAttribute->forAll(a |
a.type.oclIsKindOf(DataType) and
hasAllDataTypeAttributes(a.type.oclAsType(DataType))))
Name: when_non_negative
Related element: TimeEvent
Description: The ValueSpecification when must return a non-negative Integer.
Language: OCL
Formal wording:
when.integerValue() >= 0
Name: trigger_with_ports
Related element: Trigger
Description: If a Trigger specifies one or more ports, the event of the Trigger must be a MessageEvent.
Language: OCL
Formal wording:
port->notEmpty() implies event.oclIsKindOf(MessageEvent)
Name: abstract_no_method
Related element: BehavioralFeature
Description: When isAbstract is true there are no methods.
Language: OCL
Formal wording:
isAbstract implies method->isEmpty()
Name: spec
Related element: BehavioralFeature-isDistinguishableFrom
Language: OCL
Formal wording:
result = ((n.oclIsKindOf(BehavioralFeature) and ns.getNamesOfMember(self)->intersection(ns.getNamesOfMember(n))->notEmpty()) implies
Set{self}->including(n.oclAsType(BehavioralFeature))->isUnique(ownedParameter->collect(p|
Tuple { name=p.name, type=p.type,effect=p.effect,direction=p.direction,isException=p.isException,
isStream=p.isStream,isOrdered=p.isOrdered,isUnique=p.isUnique,lower=p.lower, upper=p.upper }))
)
Name: spec
Related element: BehavioralFeature-inputParameters
Language: OCL
Formal wording:
result = (ownedParameter->select(direction=ParameterDirectionKind::_'in' or direction=ParameterDirectionKind::inout))
Name: spec
Related element: BehavioralFeature-outputParameters
Language: OCL
Formal wording:
result = (ownedParameter->select(direction=ParameterDirectionKind::out or direction=ParameterDirectionKind::inout or direction=ParameterDirectionKind::return))
Name: specialize_type
Related element: Classifier
Description: A Classifier may only specialize Classifiers of a valid type.
Language: OCL
Formal wording:
parents()->forAll(c | self.maySpecializeType(c))
Name: maps_to_generalization_set
Related element: Classifier
Description: The Classifier that maps to a GeneralizationSet may neither be a specific nor a general Classifier in any of the Generalization relationships defined for that GeneralizationSet. In other words, a power type may not be an instance of itself nor may its instances also be its subclasses.
Language: OCL
Formal wording:
powertypeExtent->forAll( gs |
gs.generalization->forAll( gen |
not (gen.general = self) and not gen.general.allParents()->includes(self) and not (gen.specific = self) and not self.allParents()->includes(gen.specific)
))
Name: non_final_parents
Related element: Classifier
Description: The parents of a Classifier must be non-final.
Language: OCL
Formal wording:
parents()->forAll(not isFinalSpecialization)
Name: no_cycles_in_generalization
Related element: Classifier
Description: Generalization hierarchies must be directed and acyclical. A Classifier can not be both a transitively general and transitively specific Classifier of the same Classifier.
Language: OCL
Formal wording:
not allParents()->includes(self)
Name: spec
Related element: Classifier-allFeatures
Language: OCL
Formal wording:
result = (member->select(oclIsKindOf(Feature))->collect(oclAsType(Feature))->asSet())
Name: spec
Related element: Classifier-allParents
Language: OCL
Formal wording:
result = (parents()->union(parents()->collect(allParents())->asSet()))
Name: spec
Related element: Classifier-conformsTo
Language: OCL
Formal wording:
result = (if other.oclIsKindOf(Classifier) then
let otherClassifier : Classifier = other.oclAsType(Classifier) in
self = otherClassifier or allParents()->includes(otherClassifier)
else
false
endif)
Name: spec
Related element: Classifier-general.1 Classifier-general
Language: OCL
Formal wording:
result = (parents())
Name: pre
Related element: Classifier-hasVisibilityOf
Language: OCL
Formal wording:
allParents()->including(self)->collect(member)->includes(n)
Name: spec
Related element: Classifier-hasVisibilityOf
Language: OCL
Formal wording:
result = (n.visibility <> VisibilityKind::private)
Name: spec
Related element: Classifier-inherit
Language: OCL
Formal wording:
result = (inhs->reject(inh |
inh.oclIsKindOf(RedefinableElement) and
ownedMember->select(oclIsKindOf(RedefinableElement))->
select(redefinedElement->includes(inh.oclAsType(RedefinableElement)))
->notEmpty()))
Name: pre
Related element: Classifier-inheritableMembers
Language: OCL
Formal wording:
c.allParents()->includes(self)
Name: spec
Related element: Classifier-inheritableMembers
Language: OCL
Formal wording:
result = (member->select(m | c.hasVisibilityOf(m)))
Name: spec
Related element: Classifier-inheritedMember.1 Classifier-inheritedMember
Language: OCL
Formal wording:
result = (inherit(parents()->collect(inheritableMembers(self))->asSet()))
Name: spec
Related element: Classifier-isTemplate
Language: OCL
Formal wording:
result = (ownedTemplateSignature <> null or general->exists(g | g.isTemplate()))
Name: spec
Related element: Classifier-maySpecializeType
Language: OCL
Formal wording:
result = (self.oclIsKindOf(c.oclType()))
Name: spec
Related element: Classifier-parents
Language: OCL
Formal wording:
result = (generalization.general->asSet())
Name: spec
Related element: Classifier-directlyRealizedInterfaces
Language: OCL
Formal wording:
result = ((clientDependency->
select(oclIsKindOf(Realization) and supplier->forAll(oclIsKindOf(Interface))))->
collect(supplier.oclAsType(Interface))->asSet())
Name: spec
Related element: Classifier-directlyUsedInterfaces
Language: OCL
Formal wording:
result = ((supplierDependency->
select(oclIsKindOf(Usage) and client->forAll(oclIsKindOf(Interface))))->
collect(client.oclAsType(Interface))->asSet())
Name: spec
Related element: Classifier-allRealizedInterfaces
Language: OCL
Formal wording:
result = (directlyRealizedInterfaces()->union(self.allParents()->collect(directlyRealizedInterfaces()))->asSet())
Name: spec
Related element: Classifier-allUsedInterfaces
Language: OCL
Formal wording:
result = (directlyUsedInterfaces()->union(self.allParents()->collect(directlyUsedInterfaces()))->asSet())
Name: spec
Related element: Classifier-isSubstitutableFor
Language: OCL
Formal wording:
result = (substitution.contract->includes(contract))
Name: spec
Related element: Classifier-allAttributes
Language: OCL
Formal wording:
result = (attribute->asSequence()->union(parents()->asSequence().allAttributes())->select(p | member->includes(p))->asOrderedSet())
Name: spec
Related element: Classifier-allSlottableFeatures
Language: OCL
Formal wording:
result = (member->select(oclIsKindOf(StructuralFeature))->
collect(oclAsType(StructuralFeature))->
union(self.inherit(self.allParents()->collect(p | p.attribute)->asSet())->
collect(oclAsType(StructuralFeature)))->asSet())
Name: has_constraining_classifier
Related element: ClassifierTemplateParameter
Description: If allowSubstitutable is true, then there must be a constrainingClassifier.
Language: OCL
Formal wording:
allowSubstitutable implies constrainingClassifier->notEmpty()
Name: parametered_element_no_features
Related element: ClassifierTemplateParameter
Description: The parameteredElement has no direct features, and if constrainedElement is empty it has no generalizations.
Language: OCL
Formal wording:
parameteredElement.feature->isEmpty() and (constrainingClassifier->isEmpty() implies parameteredElement.allParents()->isEmpty())
Name: matching_abstract
Related element: ClassifierTemplateParameter
Description: If the parameteredElement is not abstract, then the Classifier used as an argument shall not be abstract.
Language: OCL
Formal wording:
(not parameteredElement.isAbstract) implies templateParameterSubstitution.actual->forAll(a | not a.oclAsType(Classifier).isAbstract)
Name: actual_is_classifier
Related element: ClassifierTemplateParameter
Description: The argument to a ClassifierTemplateParameter is a Classifier.
Language: OCL
Formal wording:
templateParameterSubstitution.actual->forAll(a | a.oclIsKindOf(Classifier))
Name: constraining_classifiers_constrain_args
Related element: ClassifierTemplateParameter
Description: If there are any constrainingClassifiers, then every argument must be the same as or a specialization of them, or if allowSubstitutable is true, then it can also be substitutable.
Language: OCL
Formal wording:
templateParameterSubstitution.actual->forAll( a |
let arg : Classifier = a.oclAsType(Classifier) in
constrainingClassifier->forAll(
cc |
arg = cc or arg.conformsTo(cc) or (allowSubstitutable and arg.isSubstitutableFor(cc))
)
)
Name: constraining_classifiers_constrain_parametered_element
Related element: ClassifierTemplateParameter
Description: If there are any constrainingClassifiers, then the parameteredElement must be the same as or a specialization of them, or if allowSubstitutable is true, then it can also be substitutable.
Language: OCL
Formal wording:
constrainingClassifier->forAll(
cc | parameteredElement = cc or parameteredElement.conformsTo(cc) or (allowSubstitutable and parameteredElement.isSubstitutableFor(cc))
)
Name: generalization_same_classifier
Related element: GeneralizationSet
Description: Every Generalization associated with a particular GeneralizationSet must have the same general Classifier.
Language: OCL
Formal wording:
generalization->collect(general)->asSet()->size() <= 1
Name: maps_to_generalization_set
Related element: GeneralizationSet
Description: The Classifier that maps to a GeneralizationSet may neither be a specific nor a general Classifier in any of the Generalization relationships defined for that GeneralizationSet. In other words, a power type may not be an instance of itself nor may its instances be its subclasses.
Language: OCL
Formal wording:
powertype <> null implies generalization->forAll( gen |
not (gen.general = powertype) and not gen.general.allParents()->includes(powertype) and not (gen.specific = powertype) and not powertype.allParents()->includes(gen.specific)
)
Name: deployment_artifact
Related element: InstanceSpecification
Description: An InstanceSpecification can act as a DeployedArtifact if it represents an instance of an Artifact.
Language: OCL
Formal wording:
deploymentForArtifact->notEmpty() implies classifier->exists(oclIsKindOf(Artifact))
Name: structural_feature
Related element: InstanceSpecification
Description: No more than one slot in an InstanceSpecification may have the same definingFeature.
Language: OCL
Formal wording:
classifier->forAll(c | (c.allSlottableFeatures()->forAll(f | slot->select(s | s.definingFeature = f)->size() <= 1)))
Name: defining_feature
Related element: InstanceSpecification
Description: The definingFeature of each slot is a StructuralFeature related to a classifier of the InstanceSpecification, including direct attributes, inherited attributes, private attributes in generalizations, and memberEnds of Associations, but excluding redefined StructuralFeatures.
Language: OCL
Formal wording:
slot->forAll(s | classifier->exists (c | c.allSlottableFeatures()->includes (s.definingFeature)))
Name: deployment_target
Related element: InstanceSpecification
Description: An InstanceSpecification can act as a DeploymentTarget if it represents an instance of a Node and functions as a part in the internal structure of an encompassing Node.
Language: OCL
Formal wording:
deployment->notEmpty() implies classifier->exists(node | node.oclIsKindOf(Node) and Node.allInstances()->exists(n | n.part->exists(p | p.type = node)))
Name: at_most_one_return
Related element: Operation
Description: An Operation can have at most one return parameter; i.e., an owned parameter with the direction set to 'return.'
Language: OCL
Formal wording:
self.ownedParameter->select(direction = ParameterDirectionKind::return)->size() <= 1
Name: only_body_for_query
Related element: Operation
Description: A bodyCondition can only be specified for a query Operation.
Language: OCL
Formal wording:
bodyCondition <> null implies isQuery
Name: spec
Related element: Operation-isConsistentWith
Language: OCL
Formal wording:
result = (redefiningElement.oclIsKindOf(Operation) and
let op : Operation = redefiningElement.oclAsType(Operation) in
self.ownedParameter->size() = op.ownedParameter->size() and
Sequence{1..self.ownedParameter->size()}->
forAll(i |
let redefiningParam : Parameter = op.ownedParameter->at(i),
redefinedParam : Parameter = self.ownedParameter->at(i) in
(redefiningParam.isUnique = redefinedParam.isUnique) and
(redefiningParam.isOrdered = redefinedParam. isOrdered) and
(redefiningParam.direction = redefinedParam.direction) and
(redefiningParam.type.conformsTo(redefinedParam.type) or
redefinedParam.type.conformsTo(redefiningParam.type)) and
(redefiningParam.direction = ParameterDirectionKind::inout implies
(redefinedParam.compatibleWith(redefiningParam) and
redefiningParam.compatibleWith(redefinedParam))) and
(redefiningParam.direction = ParameterDirectionKind::_'in' implies
redefinedParam.compatibleWith(redefiningParam)) and
((redefiningParam.direction = ParameterDirectionKind::out or
redefiningParam.direction = ParameterDirectionKind::return) implies
redefiningParam.compatibleWith(redefinedParam))
))
Name: pre
Related element: Operation-isConsistentWith
Language: OCL
Formal wording:
redefiningElement.isRedefinitionContextValid(self)
Name: spec
Related element: Operation-isOrdered.1 Operation-isOrdered
Language: OCL
Formal wording:
result = (if returnResult()->notEmpty() then returnResult()-> exists(isOrdered) else false endif)
Name: spec
Related element: Operation-isUnique.1 Operation-isUnique
Language: OCL
Formal wording:
result = (if returnResult()->notEmpty() then returnResult()->exists(isUnique) else true endif)
Name: spec
Related element: Operation-lower.1 Operation-lower
Language: OCL
Formal wording:
result = (if returnResult()->notEmpty() then returnResult()->any(true).lower else null endif)
Name: spec
Related element: Operation-returnResult
Language: OCL
Formal wording:
result = (ownedParameter->select (direction = ParameterDirectionKind::return))
Name: spec
Related element: Operation-type.1 Operation-type
Language: OCL
Formal wording:
result = (if returnResult()->notEmpty() then returnResult()->any(true).type else null endif)
Name: spec
Related element: Operation-upper.1 Operation-upper
Language: OCL
Formal wording:
result = (if returnResult()->notEmpty() then returnResult()->any(true).upper else null endif)
Name: match_default_signature
Related element: OperationTemplateParameter
Language: OCL
Formal wording:
default->notEmpty() implies (default.oclIsKindOf(Operation) and (let defaultOp : Operation = default.oclAsType(Operation) in
defaultOp.ownedParameter->size() = parameteredElement.ownedParameter->size() and
Sequence{1.. defaultOp.ownedParameter->size()}->forAll( ix |
let p1: Parameter = defaultOp.ownedParameter->at(ix), p2 : Parameter = parameteredElement.ownedParameter->at(ix) in
p1.type = p2.type and p1.upper = p2.upper and p1.lower = p2.lower and p1.direction = p2.direction and p1.isOrdered = p2.isOrdered and p1.isUnique = p2.isUnique)))
Name: in_and_out
Related element: Parameter
Description: Only in and inout Parameters may have a delete effect. Only out, inout, and return Parameters may have a create effect.
Language: OCL
Formal wording:
(effect = ParameterEffectKind::delete implies (direction = ParameterDirectionKind::_'in' or direction = ParameterDirectionKind::inout)) and (effect = ParameterEffectKind::create implies (direction = ParameterDirectionKind::out or direction = ParameterDirectionKind::inout or direction = ParameterDirectionKind::return))
Name: not_exception
Related element: Parameter
Description: An input Parameter cannot be an exception.
Language: OCL
Formal wording:
isException implies (direction <> ParameterDirectionKind::_'in' and direction <> ParameterDirectionKind::inout)
Name: connector_end
Related element: Parameter
Description: A Parameter may only be associated with a Connector end within the context of a Collaboration.
Language: OCL
Formal wording:
end->notEmpty() implies collaboration->notEmpty()
Name: reentrant_behaviors
Related element: Parameter
Description: Reentrant behaviors cannot have stream Parameters.
Language: OCL
Formal wording:
(isStream and behavior <> null) implies not behavior.isReentrant
Name: stream_and_exception
Related element: Parameter
Description: A Parameter cannot be a stream and exception at the same time.
Language: OCL
Formal wording:
not (isException and isStream)
Name: object_effect
Related element: Parameter
Description: Parameters typed by DataTypes cannot have an effect.
Language: OCL
Formal wording:
(type.oclIsKindOf(DataType)) implies (effect = null)
Name: spec
Related element: Parameter-default.1 Parameter-default
Language: OCL
Formal wording:
result = (if self.type = String then defaultValue.stringValue() else null endif)
Name: same_parameterized_entity
Related element: ParameterSet
Description: The Parameters in a ParameterSet must all be inputs or all be outputs of the same parameterized entity, and the ParameterSet is owned by that entity.
Language: OCL
Formal wording:
parameter->forAll(p1, p2 | self.owner = p1.owner and self.owner = p2.owner and p1.direction = p2.direction)
Name: input
Related element: ParameterSet
Description: If a parameterized entity has input Parameters that are in a ParameterSet, then any inputs that are not in a ParameterSet must be streaming. Same for output Parameters.
Language: OCL
Formal wording:
((parameter->exists(direction = ParameterDirectionKind::_'in')) implies
behavioralFeature.ownedParameter->select(p | p.direction = ParameterDirectionKind::_'in' and p.parameterSet->isEmpty())->forAll(isStream))
and
((parameter->exists(direction = ParameterDirectionKind::out)) implies
behavioralFeature.ownedParameter->select(p | p.direction = ParameterDirectionKind::out and p.parameterSet->isEmpty())->forAll(isStream))
Name: two_parameter_sets
Related element: ParameterSet
Description: Two ParameterSets cannot have exactly the same set of Parameters.
Language: OCL
Formal wording:
parameter->forAll(parameterSet->forAll(s1, s2 | s1->size() = s2->size() implies s1.parameter->exists(p | not s2.parameter->includes(p))))
Name: subsetting_context_conforms
Related element: Property
Description: Subsetting may only occur when the context of the subsetting property conforms to the context of the subsetted property.
Language: OCL
Formal wording:
subsettedProperty->notEmpty() implies
(subsettingContext()->notEmpty() and subsettingContext()->forAll (sc |
subsettedProperty->forAll(sp |
sp.subsettingContext()->exists(c | sc.conformsTo(c)))))
Name: derived_union_is_read_only
Related element: Property
Description: A derived union is read only.
Language: OCL
Formal wording:
isDerivedUnion implies isReadOnly
Name: multiplicity_of_composite
Related element: Property
Description: A multiplicity on the composing end of a composite aggregation must not have an upper bound greater than 1.
Language: OCL
Formal wording:
isComposite and association <> null implies opposite.upperBound() <= 1
Name: redefined_property_inherited
Related element: Property
Description: A redefined Property must be inherited from a more general Classifier.
Language: OCL
Formal wording:
(redefinedProperty->notEmpty()) implies
(redefinitionContext->notEmpty() and
redefinedProperty->forAll(rp|
((redefinitionContext->collect(fc|
fc.allParents()))->asSet())->collect(c| c.allFeatures())->asSet()->includes(rp)))
Name: subsetting_rules
Related element: Property
Description: A subsetting Property may strengthen the type of the subsetted Property, and its upper bound may be less.
Language: OCL
Formal wording:
subsettedProperty->forAll(sp |
self.type.conformsTo(sp.type) and
((self.upperBound()->notEmpty() and sp.upperBound()->notEmpty()) implies
self.upperBound() <= sp.upperBound() ))
Name: binding_to_attribute
Related element: Property
Description: A binding of a PropertyTemplateParameter representing an attribute must be to an attribute.
Language: OCL
Formal wording:
(self.isAttribute()
and (templateParameterSubstitution->notEmpty())
implies (templateParameterSubstitution->forAll(ts |
ts.formal.oclIsKindOf(Property)
and ts.formal.oclAsType(Property).isAttribute())))
Name: derived_union_is_derived
Related element: Property
Description: A derived union is derived.
Language: OCL
Formal wording:
isDerivedUnion implies isDerived
Name: deployment_target
Related element: Property
Description: A Property can be a DeploymentTarget if it is a kind of Node and functions as a part in the internal structure of an encompassing Node.
Language: OCL
Formal wording:
deployment->notEmpty() implies owner.oclIsKindOf(Node) and Node.allInstances()->exists(n | n.part->exists(p | p = self))
Name: subsetted_property_names
Related element: Property
Description: A Property may not subset a Property with the same name.
Language: OCL
Formal wording:
subsettedProperty->forAll(sp | sp.name <> name)
Name: type_of_opposite_end
Related element: Property
Description: If a Property is a classifier-owned end of a binary Association, its owner must be the type of the opposite end.
Language: OCL
Formal wording:
(opposite->notEmpty() and owningAssociation->isEmpty()) implies classifier = opposite.type
Name: qualified_is_association_end
Related element: Property
Description: All qualified Properties must be Association ends
Language: OCL
Formal wording:
qualifier->notEmpty() implies association->notEmpty()
Name: spec
Related element: Property-isAttribute
Language: OCL
Formal wording:
result = (not classifier->isEmpty())
Name: spec
Related element: Property-isCompatibleWith
Language: OCL
Formal wording:
result = (self.oclIsKindOf(p.oclType()) and (p.oclIsKindOf(TypeElement) implies self.type.conformsTo(p.oclAsType(TypedElement).type)))
Name: spec
Related element: Property-isComposite.1 Property-isComposite
Language: OCL
Formal wording:
result = (aggregation = AggregationKind::composite)
Name: pre
Related element: Property-isConsistentWith
Language: OCL
Formal wording:
redefiningElement.isRedefinitionContextValid(self)
Name: spec
Related element: Property-isConsistentWith
Language: OCL
Formal wording:
result = (redefiningElement.oclIsKindOf(Property) and let prop : Property = redefiningElement.oclAsType(Property) in (prop.type.conformsTo(self.type) and ((prop.lowerBound()->notEmpty() and self.lowerBound()->notEmpty()) implies prop.lowerBound() >= self.lowerBound()) and ((prop.upperBound()->notEmpty() and self.upperBound()->notEmpty()) implies prop.lowerBound() <= self.lowerBound()) and (self.isComposite implies prop.isComposite)))
Name: spec
Related element: Property-isNavigable
Language: OCL
Formal wording:
result = (not classifier->isEmpty() or association.navigableOwnedEnd->includes(self))
Name: spec
Related element: Property-opposite.1 Property-opposite
Language: OCL
Formal wording:
result = (if association <> null and association.memberEnd->size() = 2
then
association.memberEnd->any(e | e <> self)
else
null
endif)
Name: spec
Related element: Property-subsettingContext
Language: OCL
Formal wording:
result = (if association <> null
then association.memberEnd->excluding(self)->collect(type)->asSet()
else
if classifier<>null
then classifier->asSet()
else Set{}
endif
endif)
Name: redefinition_consistent
Related element: RedefinableElement
Description: A redefining element must be consistent with each redefined element.
Language: OCL
Formal wording:
redefinedElement->forAll(re | re.isConsistentWith(self))
Name: non_leaf_redefinition
Related element: RedefinableElement
Description: A RedefinableElement can only redefine non-leaf RedefinableElements.
Language: OCL
Formal wording:
redefinedElement->forAll(re | not re.isLeaf)
Name: redefinition_context_valid
Related element: RedefinableElement
Description: At least one of the redefinition contexts of the redefining element must be a specialization of at least one of the redefinition contexts for each redefined element.
Language: OCL
Formal wording:
redefinedElement->forAll(re | self.isRedefinitionContextValid(re))
Name: spec
Related element: RedefinableElement-isConsistentWith
Language: OCL
Formal wording:
result = (false)
Name: pre
Related element: RedefinableElement-isConsistentWith
Language: OCL
Formal wording:
redefiningElement.isRedefinitionContextValid(self)
Name: spec
Related element: RedefinableElement-isRedefinitionContextValid
Language: OCL
Formal wording:
result = (redefinitionContext->exists(c | c.allParents()->includesAll(redefinedElement.redefinitionContext)))
Name: redefines_parents
Related element: RedefinableTemplateSignature
Description: If any of the parent Classifiers are a template, then the extendedSignature must include the signature of that Classifier.
Language: OCL
Formal wording:
classifier.allParents()->forAll(c | c.ownedTemplateSignature->notEmpty() implies self->closure(extendedSignature)->includes(c.ownedTemplateSignature))
Name: spec
Related element: RedefinableTemplateSignature-inheritedParameter.1 RedefinableTemplateSignature-inheritedParameter
Language: OCL
Formal wording:
result = (if extendedSignature->isEmpty() then Set{} else extendedSignature.parameter->asSet() endif)
Name: spec
Related element: RedefinableTemplateSignature-isConsistentWith
Language: OCL
Formal wording:
result = (redefiningElement.oclIsKindOf(RedefinableTemplateSignature))
Name: pre
Related element: RedefinableTemplateSignature-isConsistentWith
Language: OCL
Formal wording:
redefiningElement.isRedefinitionContextValid(self)
Name: multiplicity
Related element: ValueSpecificationAction
Description: The multiplicity of the result OutputPin is 1..1
Language: OCL
Formal wording:
result.is(1,1)
Name: compatible_type
Related element: ValueSpecificationAction
Description: The type of the value ValueSpecification must conform to the type of the result OutputPin.
Language: OCL
Formal wording:
value.type.conformsTo(result.type)
Name: scope_of_variable
Related element: VariableAction
Description: The VariableAction must be in the scope of the variable.
Language: OCL
Formal wording:
variable.isAccessibleBy(self)
Name: allow_access
Related element: WriteLinkAction
Description: The visibility of at least one end must allow access from the context Classifier of the WriteLinkAction.
Language: OCL
Formal wording:
endData.end->exists(end |
end.type=_'context' or
end.visibility=VisibilityKind::public or
end.visibility=VisibilityKind::protected and
endData.end->exists(other |
other<>end and _'context'.conformsTo(other.type.oclAsType(Classifier))))
Name: multiplicity_of_result
Related element: WriteStructuralFeatureAction
Description: The multiplicity of the result OutputPin must be 1..1.
Language: OCL
Formal wording:
result <> null implies result.is(1,1)
Name: type_of_value
Related element: WriteStructuralFeatureAction
Description: The type of the value InputPin must conform to the type of the structuralFeature.
Language: OCL
Formal wording:
value <> null implies value.type.conformsTo(structuralFeature.type)
Name: multiplicity_of_value
Related element: WriteStructuralFeatureAction
Description: The multiplicity of the value InputPin is 1..1.
Language: OCL
Formal wording:
value<>null implies value.is(1,1)
Name: type_of_result
Related element: WriteStructuralFeatureAction
Description: The type of the result OutputPin is the same as the type of the inherited object InputPin.
Language: OCL
Formal wording:
result <> null implies result.type = object.type
Name: value_type
Related element: WriteVariableAction
Description: The type of the value InputPin must conform to the type of the variable.
Language: OCL
Formal wording:
value <> null implies value.type.conformsTo(variable.type)
Name: multiplicity
Related element: WriteVariableAction
Description: The multiplicity of the value InputPin is 1..1.
Language: OCL
Formal wording:
value<>null implies value.is(1,1)
Name: result_pins
Related element: AcceptCallAction
Description: The number of result OutputPins must be the same as the number of input (in and inout) ownedParameters of the Operation specified by the trigger Event. The type, ordering and multiplicity of each result OutputPin must be consistent with the corresponding input Parameter.
Language: OCL
Formal wording:
let parameter: OrderedSet(Parameter) = trigger.event->asSequence()->first().oclAsType(CallEvent).operation.inputParameters() in
result->size() = parameter->size() and
Sequence{1..result->size()}->forAll(i |
parameter->at(i).type.conformsTo(result->at(i).type) and
parameter->at(i).isOrdered = result->at(i).isOrdered and
parameter->at(i).compatibleWith(result->at(i)))
Name: trigger_call_event
Related element: AcceptCallAction
Description: The action must have exactly one trigger, which must be for a CallEvent.
Language: OCL
Formal wording:
trigger->size()=1 and trigger->asSequence()->first().event.oclIsKindOf(CallEvent)
Name: unmarshall
Related element: AcceptCallAction
Description: isUnmrashall must be true for an AcceptCallAction.
Language: OCL
Formal wording:
isUnmarshall = true
Name: one_output_pin
Related element: AcceptEventAction
Description: If isUnmarshall=false and any of the triggers are for SignalEvents or TimeEvents, there must be exactly one result OutputPin with multiplicity 1..1.
Language: OCL
Formal wording:
not isUnmarshall and trigger->exists(event.oclIsKindOf(SignalEvent) or event.oclIsKindOf(TimeEvent)) implies output->size() = 1 and output->first().is(1,1)
Name: no_input_pins
Related element: AcceptEventAction
Description: AcceptEventActions may have no input pins.
Language: OCL
Formal wording:
input->size() = 0
Name: no_output_pins
Related element: AcceptEventAction
Description: There are no OutputPins if the trigger events are only ChangeEvents and/or CallEvents when this action is an instance of AcceptEventAction and not an instance of a descendant of AcceptEventAction (such as AcceptCallAction).
Language: OCL
Formal wording:
(self.oclIsTypeOf(AcceptEventAction) and
(trigger->forAll(event.oclIsKindOf(ChangeEvent) or
event.oclIsKindOf(CallEvent))))
implies output->size() = 0
Name: unmarshall_signal_events
Related element: AcceptEventAction
Description: If isUnmarshall is true (and this is not an AcceptCallAction), there must be exactly one trigger, which is for a SignalEvent. The number of result output pins must be the same as the number of attributes of the signal. The type and ordering of each result output pin must be the same as the corresponding attribute of the signal. The multiplicity of each result output pin must be compatible with the multiplicity of the corresponding attribute.
Language: OCL
Formal wording:
isUnmarshall and self.oclIsTypeOf(AcceptEventAction) implies
trigger->size()=1 and
trigger->asSequence()->first().event.oclIsKindOf(SignalEvent) and
let attribute: OrderedSet(Property) = trigger->asSequence()->first().event.oclAsType(SignalEvent).signal.allAttributes() in
attribute->size()>0 and result->size() = attribute->size() and
Sequence{1..result->size()}->forAll(i |
result->at(i).type = attribute->at(i).type and
result->at(i).isOrdered = attribute->at(i).isOrdered and
result->at(i).includesMultiplicity(attribute->at(i)))
Name: conforming_type
Related element: AcceptEventAction
Description: If isUnmarshall=false and all the triggers are for SignalEvents, then the type of the single result OutputPin must either be null or all the signals must conform to it.
Language: OCL
Formal wording:
not isUnmarshall implies result->isEmpty() or let type: Type = result->first().type in type=null or (trigger->forAll(event.oclIsKindOf(SignalEvent)) and trigger.event.oclAsType(SignalEvent).signal->forAll(s | s.conformsTo(type)))
Name: spec
Related element: Action-context.1 Action-context
Language: OCL
Formal wording:
result = (let behavior: Behavior = self.containingBehavior() in if behavior=null then null else if behavior._'context' = null then behavior else behavior._'context' endif endif)
Name: spec
Related element: Action-allActions
Language: OCL
Formal wording:
result = (self->asSet())
Name: spec
Related element: Action-allOwnedNodes
Language: OCL
Formal wording:
result = (input.oclAsType(Pin)->asSet()->union(output->asSet()))
Name: spec
Related element: Action-containingBehavior
Language: OCL
Formal wording:
result = (if inStructuredNode<>null then inStructuredNode.containingBehavior() else if activity<>null then activity else interaction endif endif )
Name: input_pin
Related element: ActionInputPin
Description: The fromAction of an ActionInputPin must only have ActionInputPins as InputPins.
Language: OCL
Formal wording:
fromAction.input->forAll(oclIsKindOf(ActionInputPin))
Name: one_output_pin
Related element: ActionInputPin
Description: The fromAction of an ActionInputPin must have exactly one OutputPin.
Language: OCL
Formal wording:
fromAction.output->size() = 1
Name: no_control_or_object_flow
Related element: ActionInputPin
Description: The fromAction of an ActionInputPin cannot have ActivityEdges coming into or out of it or its Pins.
Language: OCL
Formal wording:
fromAction.incoming->union(outgoing)->isEmpty() and fromAction.input.incoming->isEmpty() and fromAction.output.outgoing->isEmpty()
Name: required_value
Related element: AddStructuralFeatureValueAction
Description: A value InputPin is required.
Language: OCL
Formal wording:
value<>null
Name: insertAt_pin
Related element: AddStructuralFeatureValueAction
Description: AddStructuralFeatureActions adding a value to ordered StructuralFeatures must have a single InputPin for the insertion point with type UnlimitedNatural and multiplicity of 1..1 if isReplaceAll=false, and must have no Input Pin for the insertion point when the StructuralFeature is unordered.
Language: OCL
Formal wording:
if not structuralFeature.isOrdered then insertAt = null else not isReplaceAll implies insertAt<>null and insertAt->forAll(type=UnlimitedNatural and is(1,1.oclAsType(UnlimitedNatural))) endif
Name: required_value
Related element: AddVariableValueAction
Description: A value InputPin is required.
Language: OCL
Formal wording:
value <> null
Name: insertAt_pin
Related element: AddVariableValueAction
Description: AddVariableValueActions for ordered Variables must have a single InputPin for the insertion point with type UnlimtedNatural and multiplicity of 1..1 if isReplaceAll=false, otherwise the Action has no InputPin for the insertion point.
Language: OCL
Formal wording:
if not variable.isOrdered then insertAt = null else not isReplaceAll implies insertAt<>null and insertAt->forAll(type=UnlimitedNatural and is(1,1.oclAsType(UnlimitedNatural))) endif
Name: number_of_arguments
Related element: BroadcastSignalAction
Description: The number of argument InputPins must be the same as the number of attributes in the signal.
Language: OCL
Formal wording:
argument->size() = signal.allAttributes()->size()
Name: type_ordering_multiplicity
Related element: BroadcastSignalAction
Description: The type, ordering, and multiplicity of an argument InputPin must be the same as the corresponding attribute of the signal.
Language: OCL
Formal wording:
let attribute: OrderedSet(Property) = signal.allAttributes() in
Sequence{1..argument->size()}->forAll(i |
argument->at(i).type.conformsTo(attribute->at(i).type) and
argument->at(i).isOrdered = attribute->at(i).isOrdered and
argument->at(i).compatibleWith(attribute->at(i)))
Name: no_onport
Related element: BroadcastSignalAction
Description: A BroadcaseSignalAction may not specify onPort.
Language: OCL
Formal wording:
onPort=null
Name: argument_pins
Related element: CallAction
Description: The number of argument InputPins must be the same as the number of input (in and inout) ownedParameters of the called Behavior or Operation. The type, ordering and multiplicity of each argument InputPin must be consistent with the corresponding input Parameter.
Language: OCL
Formal wording:
let parameter: OrderedSet(Parameter) = self.inputParameters() in
argument->size() = parameter->size() and
Sequence{1..argument->size()}->forAll(i |
argument->at(i).type.conformsTo(parameter->at(i).type) and
argument->at(i).isOrdered = parameter->at(i).isOrdered and
argument->at(i).compatibleWith(parameter->at(i)))
Name: result_pins
Related element: CallAction
Description: The number of result OutputPins must be the same as the number of output (inout, out and return) ownedParameters of the called Behavior or Operation. The type, ordering and multiplicity of each result OutputPin must be consistent with the corresponding input Parameter.
Language: OCL
Formal wording:
let parameter: OrderedSet(Parameter) = self.outputParameters() in
result->size() = parameter->size() and
Sequence{1..result->size()}->forAll(i |
parameter->at(i).type.conformsTo(result->at(i).type) and
parameter->at(i).isOrdered = result->at(i).isOrdered and
parameter->at(i).compatibleWith(result->at(i)))
Name: synchronous_call
Related element: CallAction
Description: Only synchronous CallActions can have result OutputPins.
Language: OCL
Formal wording:
result->notEmpty() implies isSynchronous
Name: no_onport
Related element: CallBehaviorAction
Description: A CallBehaviorAction may not specify onPort.
Language: OCL
Formal wording:
onPort=null
Name: spec
Related element: CallBehaviorAction-outputParameters
Language: OCL
Formal wording:
result = (behavior.outputParameters())
Name: spec
Related element: CallBehaviorAction-inputParameters
Language: OCL
Formal wording:
result = (behavior.inputParameters())
Name: type_target_pin
Related element: CallOperationAction
Description: If onPort has no value, the operation must be an owned or inherited feature of the type of the target InputPin, otherwise the Port given by onPort must be an owned or inherited feature of the type of the target InputPin, and the Port must have a required or provided Interface with the operation as an owned or inherited feature.
Language: OCL
Formal wording:
if onPort=null then target.type.oclAsType(Classifier).allFeatures()->includes(operation) else target.type.oclAsType(Classifier).allFeatures()->includes(onPort) and onPort.provided->union(onPort.required).allFeatures()->includes(operation) endif
Name: spec
Related element: CallOperationAction-outputParameters
Language: OCL
Formal wording:
result = (operation.outputParameters())
Name: spec
Related element: CallOperationAction-inputParameters
Language: OCL
Formal wording:
result = (operation.inputParameters())
Name: body_output_pins
Related element: Clause
Description: The bodyOutput Pins are OutputPins on Actions in the body of the Clause.
Language: OCL
Formal wording:
_'body'.oclAsType(Action).allActions().output->includesAll(bodyOutput)
Name: decider_output
Related element: Clause
Description: The decider Pin must be on an Action in the test section of the Clause and must be of type Boolean with multiplicity 1..1.
Language: OCL
Formal wording:
test.oclAsType(Action).allActions().output->includes(decider) and decider.type = Boolean and decider.is(1,1)
Name: test_and_body
Related element: Clause
Description: The test and body parts of a ConditionalNode must be disjoint with each other.
Language: OCL
Formal wording:
test->intersection(_'body')->isEmpty()
Name: multiplicity
Related element: ClearAssociationAction
Description: The multiplicity of the object InputPin is 1..1.
Language: OCL
Formal wording:
object.is(1,1)
Name: same_type
Related element: ClearAssociationAction
Description: The type of the InputPin must conform to the type of at least one of the memberEnds of the association.
Language: OCL
Formal wording:
association.memberEnd->exists(self.object.type.conformsTo(type))
Name: type_of_result
Related element: ClearStructuralFeatureAction
Description: The type of the result OutputPin is the same as the type of the inherited object InputPin.
Language: OCL
Formal wording:
result<>null implies result.type = object.type
Name: multiplicity_of_result
Related element: ClearStructuralFeatureAction
Description: The multiplicity of the result OutputPin must be 1..1.
Language: OCL
Formal wording:
result<>null implies result.is(1,1)
Name: result_no_incoming
Related element: ConditionalNode
Description: The result OutputPins have no incoming edges.
Language: OCL
Formal wording:
result.incoming->isEmpty()
Name: no_input_pins
Related element: ConditionalNode
Description: A ConditionalNode has no InputPins.
Language: OCL
Formal wording:
input->isEmpty()
Name: one_clause_with_executable_node
Related element: ConditionalNode
Description: No ExecutableNode in the ConditionNode may appear in the test or body part of more than one clause of a ConditionalNode.
Language: OCL
Formal wording:
node->select(oclIsKindOf(ExecutableNode)).oclAsType(ExecutableNode)->forAll(n | self.clause->select(test->union(_'body')->includes(n))->size()=1)
Name: matching_output_pins
Related element: ConditionalNode
Description: Each clause of a ConditionalNode must have the same number of bodyOutput pins as the ConditionalNode has result OutputPins, and each clause bodyOutput Pin must be compatible with the corresponding result OutputPin (by positional order) in type, multiplicity, ordering, and uniqueness.
Language: OCL
Formal wording:
clause->forAll(
bodyOutput->size()=self.result->size() and
Sequence{1..self.result->size()}->forAll(i |
bodyOutput->at(i).type.conformsTo(result->at(i).type) and
bodyOutput->at(i).isOrdered = result->at(i).isOrdered and
bodyOutput->at(i).isUnique = result->at(i).isUnique and
bodyOutput->at(i).compatibleWith(result->at(i))))
Name: executable_nodes
Related element: ConditionalNode
Description: The union of the ExecutableNodes in the test and body parts of all clauses must be the same as the subset of nodes contained in the ConditionalNode (considered as a StructuredActivityNode) that are ExecutableNodes.
Language: OCL
Formal wording:
clause.test->union(clause._'body') = node->select(oclIsKindOf(ExecutableNode)).oclAsType(ExecutableNode)
Name: clause_no_predecessor
Related element: ConditionalNode
Description: No two clauses within a ConditionalNode may be predecessorClauses of each other, either directly or indirectly.
Language: OCL
Formal wording:
clause->closure(predecessorClause)->intersection(clause)->isEmpty()
Name: spec
Related element: ConditionalNode-allActions
Language: OCL
Formal wording:
result = (self->asSet())
Name: association_not_abstract
Related element: CreateLinkAction
Description: The Association cannot be an abstract Classifier.
Language: OCL
Formal wording:
not self.association().isAbstract
Name: multiplicity
Related element: CreateLinkObjectAction
Description: The multiplicity of the OutputPin is 1..1.
Language: OCL
Formal wording:
result.is(1,1)
Name: type_of_result
Related element: CreateLinkObjectAction
Description: The type of the result OutputPin must be the same as the Association of the CreateLinkObjectAction.
Language: OCL
Formal wording:
result.type = association()
Name: association_class
Related element: CreateLinkObjectAction
Description: The Association must be an AssociationClass.
Language: OCL
Formal wording:
self.association().oclIsKindOf(AssociationClass)
Name: classifier_not_abstract
Related element: CreateObjectAction
Description: The classifier cannot be abstract.
Language: OCL
Formal wording:
not classifier.isAbstract
Name: multiplicity
Related element: CreateObjectAction
Description: The multiplicity of the result OutputPin is 1..1.
Language: OCL
Formal wording:
result.is(1,1)
Name: classifier_not_association_class
Related element: CreateObjectAction
Description: The classifier cannot be an AssociationClass.
Language: OCL
Formal wording:
not classifier.oclIsKindOf(AssociationClass)
Name: same_type
Related element: CreateObjectAction
Description: The type of the result OutputPin must be the same as the classifier of the CreateObjectAction.
Language: OCL
Formal wording:
result.type = classifier
Name: multiplicity
Related element: DestroyObjectAction
Description: The multiplicity of the targe IinputPin is 1..1.
Language: OCL
Formal wording:
target.is(1,1)
Name: no_type
Related element: DestroyObjectAction
Description: The target InputPin has no type.
Language: OCL
Formal wording:
target.type= null
Name: region_as_input_or_output
Related element: ExpansionNode
Description: One of regionAsInput or regionAsOutput must be non-empty, but not both.
Language: OCL
Formal wording:
regionAsInput->notEmpty() xor regionAsOutput->notEmpty()
Name: outgoing_edges_structured_only
Related element: InputPin
Description: An InputPin may have outgoing ActivityEdges only when it is owned by a StructuredActivityNode, and these edges must target a node contained (directly or indirectly) in the owning StructuredActivityNode.
Language: OCL
Formal wording:
outgoing->notEmpty() implies action<>null and action.oclIsKindOf(StructuredActivityNode) and action.oclAsType(StructuredActivityNode).allOwnedNodes()->includesAll(outgoing.target)
Name: same_pins
Related element: LinkAction
Description: The inputValue InputPins is the same as the union of all the InputPins referenced by the endData.
Language: OCL
Formal wording:
inputValue->asBag()=endData.allPins()
Name: same_association
Related element: LinkAction
Description: The ends of the endData must all be from the same Association and include all and only the memberEnds of that association.
Language: OCL
Formal wording:
endData.end = self.association().memberEnd->asBag()
Name: not_static
Related element: LinkAction
Description: The ends of the endData must not be static.
Language: OCL
Formal wording:
endData->forAll(not end.isStatic)
Name: spec
Related element: LinkAction-association
Language: OCL
Formal wording:
result = (endData->asSequence()->first().end.association)
Name: insertAt_pin
Related element: LinkEndCreationData
Description: LinkEndCreationData for ordered Association ends must have a single insertAt InputPin for the insertion point with type UnlimitedNatural and multiplicity of 1..1, if isReplaceAll=false, and must have no InputPin for the insertion point when the association ends are unordered.
Language: OCL
Formal wording:
if not end.isOrdered then insertAt = null else not isReplaceAll=false implies insertAt <> null and insertAt->forAll(type=UnlimitedNatural and is(1,1)) endif
Name: spec
Related element: LinkEndCreationData-allPins
Language: OCL
Formal wording:
result = (self.LinkEndData::allPins()->including(insertAt))
Name: same_type
Related element: LinkEndData
Description: The type of the value InputPin conforms to the type of the Association end.
Language: OCL
Formal wording:
value<>null implies value.type.conformsTo(end.type)
Name: multiplicity
Related element: LinkEndData
Description: The multiplicity of the value InputPin must be 1..1.
Language: OCL
Formal wording:
value<>null implies value.is(1,1)
Name: end_object_input_pin
Related element: LinkEndData
Description: The value InputPin is not also the qualifier value InputPin.
Language: OCL
Formal wording:
value->excludesAll(qualifier.value)
Name: property_is_association_end
Related element: LinkEndData
Description: The Property must be an Association memberEnd.
Language: OCL
Formal wording:
end.association <> null
Name: qualifiers
Related element: LinkEndData
Description: The qualifiers must be qualifiers of the Association end.
Language: OCL
Formal wording:
end.qualifier->includesAll(qualifier.qualifier)
Name: spec
Related element: LinkEndData-allPins
Language: OCL
Formal wording:
result = (value->asBag()->union(qualifier.value))
Name: destroyAt_pin
Related element: LinkEndDestructionData
Description: LinkEndDestructionData for ordered, nonunique Association ends must have a single destroyAt InputPin if isDestroyDuplicates is false, which must be of type UnlimitedNatural and have a multiplicity of 1..1. Otherwise, the action has no destroyAt input pin.
Language: OCL
Formal wording:
if not end.isOrdered or end.isUnique or isDestroyDuplicates then destroyAt = null else destroyAt <> null and destroyAt->forAll(type=UnlimitedNatural and is(1,1)) endif
Name: spec
Related element: LinkEndDestructionData-allPins
Language: OCL
Formal wording:
result = (self.LinkEndData::allPins()->including(destroyAt))
Name: result_no_incoming
Related element: LoopNode
Description: The result OutputPins have no incoming edges.
Language: OCL
Formal wording:
result.incoming->isEmpty()
Name: input_edges
Related element: LoopNode
Description: The loopVariableInputs must not have outgoing edges.
Language: OCL
Formal wording:
loopVariableInput.outgoing->isEmpty()
Name: executable_nodes
Related element: LoopNode
Description: The union of the ExecutableNodes in the setupPart, test and bodyPart of a LoopNode must be the same as the subset of nodes contained in the LoopNode (considered as a StructuredActivityNode) that are ExecutableNodes.
Language: OCL
Formal wording:
setupPart->union(test)->union(bodyPart)=node->select(oclIsKindOf(ExecutableNode)).oclAsType(ExecutableNode)->asSet()
Name: body_output_pins
Related element: LoopNode
Description: The bodyOutput pins are OutputPins on Actions in the body of the LoopNode.
Language: OCL
Formal wording:
bodyPart.oclAsType(Action).allActions().output->includesAll(bodyOutput)
Name: setup_test_and_body
Related element: LoopNode
Description: The test and body parts of a ConditionalNode must be disjoint with each other.
Language: OCL
Formal wording:
setupPart->intersection(test)->isEmpty() and setupPart->intersection(bodyPart)->isEmpty() and test->intersection(bodyPart)->isEmpty()
Name: matching_output_pins
Related element: LoopNode
Description: A LoopNode must have the same number of bodyOutput Pins as loopVariables, and each bodyOutput Pin must be compatible with the corresponding loopVariable (by positional order) in type, multiplicity, ordering and uniqueness.
Language: OCL
Formal wording:
bodyOutput->size()=loopVariable->size() and
Sequence{1..loopVariable->size()}->forAll(i |
bodyOutput->at(i).type.conformsTo(loopVariable->at(i).type) and
bodyOutput->at(i).isOrdered = loopVariable->at(i).isOrdered and
bodyOutput->at(i).isUnique = loopVariable->at(i).isUnique and
loopVariable->at(i).includesMultiplicity(bodyOutput->at(i)))
Name: matching_loop_variables
Related element: LoopNode
Description: A LoopNode must have the same number of loopVariableInputs and loopVariables, and they must match in type, uniqueness and multiplicity.
Language: OCL
Formal wording:
loopVariableInput->size()=loopVariable->size() and loopVariableInput.type=loopVariable.type and loopVariableInput.isUnique=loopVariable.isUnique and loopVariableInput.lower=loopVariable.lower and loopVariableInput.upper=loopVariable.upper
Name: matching_result_pins
Related element: LoopNode
Description: A LoopNode must have the same number of result OutputPins and loopVariables, and they must match in type, uniqueness and multiplicity.
Language: OCL
Formal wording:
result->size()=loopVariable->size() and result.type=loopVariable.type and result.isUnique=loopVariable.isUnique and result.lower=loopVariable.lower and result.upper=loopVariable.upper
Name: loop_variable_outgoing
Related element: LoopNode
Description: All ActivityEdges outgoing from loopVariable OutputPins must have targets within the LoopNode.
Language: OCL
Formal wording:
allOwnedNodes()->includesAll(loopVariable.outgoing.target)
Name: spec
Related element: LoopNode-allActions
Language: OCL
Formal wording:
result = (self->asSet())
Name: spec
Related element: LoopNode-sourceNodes
Language: OCL
Formal wording:
result = (self.StructuredActivityNode::sourceNodes()->union(loopVariable))
Name: language_body_size
Related element: OpaqueAction
Description: If the language attribute is not empty, then the size of the body and language lists must be the same.
Language: OCL
Formal wording:
language->notEmpty() implies (_'body'->size() = language->size())
Name: incoming_edges_structured_only
Related element: OutputPin
Description: An OutputPin may have incoming ActivityEdges only when it is owned by a StructuredActivityNode, and these edges must have sources contained (directly or indirectly) in the owning StructuredActivityNode.
Language: OCL
Formal wording:
incoming->notEmpty() implies action<>null and action.oclIsKindOf(StructuredActivityNode) and action.oclAsType(StructuredActivityNode).allOwnedNodes()->includesAll(incoming.source)
Name: control_pins
Related element: Pin
Description: A control Pin has a control type.
Language: OCL
Formal wording:
isControl implies isControlType
Name: not_unique
Related element: Pin
Description: Pin multiplicity is not unique.
Language: OCL
Formal wording:
not isUnique
Name: multiplicity_of_qualifier
Related element: QualifierValue
Description: The multiplicity of the value InputPin is 1..1.
Language: OCL
Formal wording:
value.is(1,1)
Name: type_of_qualifier
Related element: QualifierValue
Description: The type of the value InputPin conforms to the type of the qualifier Property.
Language: OCL
Formal wording:
value.type.conformsTo(qualifier.type)
Name: qualifier_attribute
Related element: QualifierValue
Description: The qualifier must be a qualifier of the Association end of the linkEndData that owns this QualifierValue.
Language: OCL
Formal wording:
linkEndData.end.qualifier->includes(qualifier)
Name: type_is_classifier
Related element: ReadExtentAction
Description: The type of the result OutputPin is the classifier.
Language: OCL
Formal wording:
result.type = classifier
Name: multiplicity_of_result
Related element: ReadExtentAction
Description: The multiplicity of the result OutputPin is 0..*.
Language: OCL
Formal wording:
result.is(0,*)
Name: no_type
Related element: ReadIsClassifiedObjectAction
Description: The object InputPin has no type.
Language: OCL
Formal wording:
object.type = null
Name: multiplicity_of_output
Related element: ReadIsClassifiedObjectAction
Description: The multiplicity of the result OutputPin is 1..1.
Language: OCL
Formal wording:
result.is(1,1)
Name: boolean_result
Related element: ReadIsClassifiedObjectAction
Description: The type of the result OutputPin is Boolean.
Language: OCL
Formal wording:
result.type = Boolean
Name: multiplicity_of_input
Related element: ReadIsClassifiedObjectAction
Description: The multiplicity of the object InputPin is 1..1.
Language: OCL
Formal wording:
object.is(1,1)
Name: type_and_ordering
Related element: ReadLinkAction
Description: The type and ordering of the result OutputPin are same as the type and ordering of the open Association end.
Language: OCL
Formal wording:
self.openEnd()->forAll(type=result.type and isOrdered=result.isOrdered)
Name: compatible_multiplicity
Related element: ReadLinkAction
Description: The multiplicity of the open Association end must be compatible with the multiplicity of the result OutputPin.
Language: OCL
Formal wording:
self.openEnd()->first().compatibleWith(result)
Name: visibility
Related element: ReadLinkAction
Description: Visibility of the open end must allow access from the object performing the action.
Language: OCL
Formal wording:
let openEnd : Property = self.openEnd()->first() in
openEnd.visibility = VisibilityKind::public or
endData->exists(oed |
oed.end<>openEnd and
(_'context' = oed.end.type or
(openEnd.visibility = VisibilityKind::protected and
_'context'.conformsTo(oed.end.type.oclAsType(Classifier)))))
Name: one_open_end
Related element: ReadLinkAction
Description: Exactly one linkEndData specification (corresponding to the "open" end) must not have an value InputPin.
Language: OCL
Formal wording:
self.openEnd()->size() = 1
Name: navigable_open_end
Related element: ReadLinkAction
Description: The open end must be navigable.
Language: OCL
Formal wording:
self.openEnd()->first().isNavigable()
Name: spec
Related element: ReadLinkAction-openEnd
Language: OCL
Formal wording:
result = (endData->select(value=null).end->asOrderedSet())
Name: property
Related element: ReadLinkObjectEndAction
Description: The end Property must be an Association memberEnd.
Language: OCL
Formal wording:
end.association <> null
Name: multiplicity_of_object
Related element: ReadLinkObjectEndAction
Description: The multiplicity of the object InputPin is 1..1.
Language: OCL
Formal wording:
object.is(1,1)
Name: ends_of_association
Related element: ReadLinkObjectEndAction
Description: The ends of the association must not be static.
Language: OCL
Formal wording:
end.association.memberEnd->forAll(e | not e.isStatic)
Name: type_of_result
Related element: ReadLinkObjectEndAction
Description: The type of the result OutputPin is the same as the type of the end Property.
Language: OCL
Formal wording:
result.type = end.type
Name: multiplicity_of_result
Related element: ReadLinkObjectEndAction
Description: The multiplicity of the result OutputPin is 1..1.
Language: OCL
Formal wording:
result.is(1,1)
Name: type_of_object
Related element: ReadLinkObjectEndAction
Description: The type of the object InputPin is the AssociationClass that owns the end Property.
Language: OCL
Formal wording:
object.type = end.association
Name: association_of_association
Related element: ReadLinkObjectEndAction
Description: The association of the end must be an AssociationClass.
Language: OCL
Formal wording:
end.association.oclIsKindOf(AssociationClass)
Name: multiplicity_of_object
Related element: ReadLinkObjectEndQualifierAction
Description: The multiplicity of the object InputPin is 1..1.
Language: OCL
Formal wording:
object.is(1,1)
Name: type_of_object
Related element: ReadLinkObjectEndQualifierAction
Description: The type of the object InputPin is the AssociationClass that owns the Association end that has the given qualifier Property.
Language: OCL
Formal wording:
object.type = qualifier.associationEnd.association
Name: multiplicity_of_qualifier
Related element: ReadLinkObjectEndQualifierAction
Description: The multiplicity of the qualifier Property is 1..1.
Language: OCL
Formal wording:
qualifier.is(1,1)
Name: ends_of_association
Related element: ReadLinkObjectEndQualifierAction
Description: The ends of the Association must not be static.
Language: OCL
Formal wording:
qualifier.associationEnd.association.memberEnd->forAll(e | not e.isStatic)
Name: multiplicity_of_result
Related element: ReadLinkObjectEndQualifierAction
Description: The multiplicity of the result OutputPin is 1..1.
Language: OCL
Formal wording:
result.is(1,1)
Name: same_type
Related element: ReadLinkObjectEndQualifierAction
Description: The type of the result OutputPin is the same as the type of the qualifier Property.
Language: OCL
Formal wording:
result.type = qualifier.type
Name: association_of_association
Related element: ReadLinkObjectEndQualifierAction
Description: The association of the Association end of the qualifier Property must be an AssociationClass.
Language: OCL
Formal wording:
qualifier.associationEnd.association.oclIsKindOf(AssociationClass)
Name: qualifier_attribute
Related element: ReadLinkObjectEndQualifierAction
Description: The qualifier Property must be a qualifier of an Association end.
Language: OCL
Formal wording:
qualifier.associationEnd <> null
Name: contained
Related element: ReadSelfAction
Description: A ReadSelfAction must have a context Classifier.
Language: OCL
Formal wording:
_'context' <> null
Name: multiplicity
Related element: ReadSelfAction
Description: The multiplicity of the result OutputPin is 1..1.
Language: OCL
Formal wording:
result.is(1,1)
Name: not_static
Related element: ReadSelfAction
Description: If the ReadSelfAction is contained in an Behavior that is acting as a method, then the Operation of the method must not be static.
Language: OCL
Formal wording:
let behavior: Behavior = self.containingBehavior() in behavior.specification<>null implies not behavior.specification.isStatic
Name: type
Related element: ReadSelfAction
Description: The type of the result OutputPin is the context Classifier.
Language: OCL
Formal wording:
result.type = _'context'
Name: multiplicity
Related element: ReadStructuralFeatureAction
Description: The multiplicity of the StructuralFeature must be compatible with the multiplicity of the result OutputPin.
Language: OCL
Formal wording:
structuralFeature.compatibleWith(result)
Name: type_and_ordering
Related element: ReadStructuralFeatureAction
Description: The type and ordering of the result OutputPin are the same as the type and ordering of the StructuralFeature.
Language: OCL
Formal wording:
result.type =structuralFeature.type and result.isOrdered = structuralFeature.isOrdered
Name: type_and_ordering
Related element: ReadVariableAction
Description: The type and ordering of the result OutputPin are the same as the type and ordering of the variable.
Language: OCL
Formal wording:
result.type =variable.type and result.isOrdered = variable.isOrdered
Name: compatible_multiplicity
Related element: ReadVariableAction
Description: The multiplicity of the variable must be compatible with the multiplicity of the output pin.
Language: OCL
Formal wording:
variable.compatibleWith(result)
Name: input_pin
Related element: ReclassifyObjectAction
Description: The object InputPin has no type.
Language: OCL
Formal wording:
object.type = null
Name: classifier_not_abstract
Related element: ReclassifyObjectAction
Description: None of the newClassifiers may be abstract.
Language: OCL
Formal wording:
not newClassifier->exists(isAbstract)
Name: multiplicity
Related element: ReclassifyObjectAction
Description: The multiplicity of the object InputPin is 1..1.
Language: OCL
Formal wording:
object.is(1,1)
Name: reducer_inputs_output
Related element: ReduceAction
Description: The reducer Behavior must have two input ownedParameters and one output ownedParameter, where the type of the output Parameter and the type of elements of the input collection conform to the types of the input Parameters.
Language: OCL
Formal wording:
let inputs: OrderedSet(Parameter) = reducer.inputParameters() in let outputs: OrderedSet(Parameter) = reducer.outputParameters() in inputs->size()=2 and outputs->size()=1 and inputs.type->forAll(t | outputs.type->forAll(conformsTo(t)) and -- Note that the following only checks the case when the collection is via multiple tokens. collection.upperBound()>1 implies collection.type.conformsTo(t))
Name: input_type_is_collection
Related element: ReduceAction
Description: The type of the collection InputPin must be a collection.
Name: output_types_are_compatible
Related element: ReduceAction
Description: The type of the output of the reducer Behavior must conform to the type of the result OutputPin.
Language: OCL
Formal wording:
reducer.outputParameters().type->forAll(conformsTo(result.type))
Name: removeAt_and_value
Related element: RemoveStructuralFeatureValueAction
Description: RemoveStructuralFeatureValueActions removing a value from ordered, non-unique StructuralFeatures must have a single removeAt InputPin and no value InputPin, if isRemoveDuplicates is false. The removeAt InputPin must be of type Unlimited Natural with multiplicity 1..1. Otherwise, the Action has a value InputPin and no removeAt InputPin.
Language: OCL
Formal wording:
if structuralFeature.isOrdered and not structuralFeature.isUnique and not isRemoveDuplicates then value = null and removeAt <> null and removeAt.type = UnlimitedNatural and removeAt.is(1,1) else removeAt = null and value <> null endif
Name: removeAt_and_value
Related element: RemoveVariableValueAction
Description: ReadVariableActions removing a value from ordered, non-unique Variables must have a single removeAt InputPin and no value InputPin, if isRemoveDuplicates is false. The removeAt InputPin must be of type Unlimited Natural with multiplicity 1..1. Otherwise, the Action has a value InputPin and no removeAt InputPin.
Language: OCL
Formal wording:
if variable.isOrdered and not variable.isUnique and not isRemoveDuplicates then value = null and removeAt <> null and removeAt.type = UnlimitedNatural and removeAt.is(1,1) else removeAt = null and value <> null endif
Name: pins_match_parameter
Related element: ReplyAction
Description: The replyValue InputPins must match the output (return, out, and inout) parameters of the operation of the event of the replyToCall Trigger in number, type, ordering, and multiplicity.
Language: OCL
Formal wording:
let parameter:OrderedSet(Parameter) = replyToCall.event.oclAsType(CallEvent).operation.outputParameters() in
replyValue->size()=parameter->size() and
Sequence{1..replyValue->size()}->forAll(i |
replyValue->at(i).type.conformsTo(parameter->at(i).type) and
replyValue->at(i).isOrdered=parameter->at(i).isOrdered and
replyValue->at(i).compatibleWith(parameter->at(i)))
Name: event_on_reply_to_call_trigger
Related element: ReplyAction
Description: The event of the replyToCall Trigger must be a CallEvent.
Language: OCL
Formal wording:
replyToCall.event.oclIsKindOf(CallEvent)
Name: type_target_pin
Related element: SendObjectAction
Description: If onPort is not empty, the Port given by onPort must be an owned or inherited feature of the type of the target InputPin.
Language: OCL
Formal wording:
onPort<>null implies target.type.oclAsType(Classifier).allFeatures()->includes(onPort)
Name: type_ordering_multiplicity
Related element: SendSignalAction
Description: The type, ordering, and multiplicity of an argument InputPin must be the same as the corresponding attribute of the signal.
Language: OCL
Formal wording:
let attribute: OrderedSet(Property) = signal.allAttributes() in
Sequence{1..argument->size()}->forAll(i |
argument->at(i).type.conformsTo(attribute->at(i).type) and
argument->at(i).isOrdered = attribute->at(i).isOrdered and
argument->at(i).compatibleWith(attribute->at(i)))
Name: number_order
Related element: SendSignalAction
Description: The number and order of argument InputPins must be the same as the number and order of attributes of the signal.
Language: OCL
Formal wording:
argument->size()=signal.allAttributes()->size()
Name: type_target_pin
Related element: SendSignalAction
Description: If onPort is not empty, the Port given by onPort must be an owned or inherited feature of the type of the target InputPin.
Language: OCL
Formal wording:
not onPort->isEmpty() implies target.type.oclAsType(Classifier).allFeatures()->includes(onPort)
Name: multiplicity
Related element: StartClassifierBehaviorAction
Description: The multiplicity of the object InputPin is 1..1
Language: OCL
Formal wording:
object.is(1,1)
Name: type_has_classifier
Related element: StartClassifierBehaviorAction
Description: If the InputPin has a type, then the type or one of its ancestors must have a classifierBehavior.
Language: OCL
Formal wording:
object.type->notEmpty() implies (object.type.oclIsKindOf(BehavioredClassifier) and object.type.oclAsType(BehavioredClassifier).classifierBehavior<>null)
Name: multiplicity_of_object
Related element: StartObjectBehaviorAction
Description: The multiplicity of the object InputPin must be 1..1.
Language: OCL
Formal wording:
object.is(1,1)
Name: type_of_object
Related element: StartObjectBehaviorAction
Description: The type of the object InputPin must be either a Behavior or a BehavioredClassifier with a classifierBehavior.
Language: OCL
Formal wording:
self.behavior()<>null
Name: no_onport
Related element: StartObjectBehaviorAction
Description: A StartObjectBehaviorAction may not specify onPort.
Language: OCL
Formal wording:
onPort->isEmpty()
Name: spec
Related element: StartObjectBehaviorAction-outputParameters
Language: OCL
Formal wording:
result = (self.behavior().outputParameters())
Name: spec
Related element: StartObjectBehaviorAction-inputParameters
Language: OCL
Formal wording:
result = (self.behavior().inputParameters())
Name: spec
Related element: StartObjectBehaviorAction-behavior
Language: OCL
Formal wording:
result = (if object.type.oclIsKindOf(Behavior) then object.type.oclAsType(Behavior) else if object.type.oclIsKindOf(BehavioredClassifier) then object.type.oclAsType(BehavioredClassifier).classifierBehavior else null endif endif)
Name: multiplicity
Related element: StructuralFeatureAction
Description: The multiplicity of the object InputPin must be 1..1.
Language: OCL
Formal wording:
object.is(1,1)
Name: object_type
Related element: StructuralFeatureAction
Description: The structuralFeature must either be an owned or inherited feature of the type of the object InputPin, or it must be an owned end of a binary Association whose opposite end had as a type to which the type of the object InputPin conforms.
Language: OCL
Formal wording:
object.type.oclAsType(Classifier).allFeatures()->includes(structuralFeature) or object.type.conformsTo(structuralFeature.oclAsType(Property).opposite.type)
Name: visibility
Related element: StructuralFeatureAction
Description: The visibility of the structuralFeature must allow access from the object performing the ReadStructuralFeatureAction.
Language: OCL
Formal wording:
structuralFeature.visibility = VisibilityKind::public or _'context'.allFeatures()->includes(structuralFeature) or structuralFeature.visibility=VisibilityKind::protected and _'context'.conformsTo(structuralFeature.oclAsType(Property).opposite.type.oclAsType(Classifier))
Name: not_static
Related element: StructuralFeatureAction
Description: The structuralFeature must not be static.
Language: OCL
Formal wording:
not structuralFeature.isStatic
Name: one_featuring_classifier
Related element: StructuralFeatureAction
Description: The structuralFeature must have exactly one featuringClassifier.
Language: OCL
Formal wording:
structuralFeature.featuringClassifier->size() = 1
Name: output_pin_edges
Related element: StructuredActivityNode
Description: The outgoing ActivityEdges of the OutputPins of a StructuredActivityNode must have targets that are not within the StructuredActivityNode.
Language: OCL
Formal wording:
output.outgoing.target->excludesAll(allOwnedNodes()-input)
Name: edges
Related element: StructuredActivityNode
Description: The edges of a StructuredActivityNode are all the ActivityEdges with source and target ActivityNodes contained directly or indirectly within the StructuredActivityNode and at least one of the source or target not contained in any more deeply nested StructuredActivityNode.
Language: OCL
Formal wording:
edge=self.sourceNodes().outgoing->intersection(self.allOwnedNodes().incoming)-> union(self.targetNodes().incoming->intersection(self.allOwnedNodes().outgoing))->asSet()
Name: input_pin_edges
Related element: StructuredActivityNode
Description: The incoming ActivityEdges of an InputPin of a StructuredActivityNode must have sources that are not within the StructuredActivityNode.
Language: OCL
Formal wording:
input.incoming.source->excludesAll(allOwnedNodes()-output)
Name: spec
Related element: StructuredActivityNode-allActions
Language: OCL
Formal wording:
result = (node->select(oclIsKindOf(Action)).oclAsType(Action).allActions()->including(self)->asSet())
Name: spec
Related element: StructuredActivityNode-allOwnedNodes
Language: OCL
Formal wording:
result = (self.Action::allOwnedNodes()->union(node)->union(node->select(oclIsKindOf(Action)).oclAsType(Action).allOwnedNodes())->asSet())
Name: spec
Related element: StructuredActivityNode-sourceNodes
Language: OCL
Formal wording:
result = (node->union(input.oclAsType(ActivityNode)->asSet())-> union(node->select(oclIsKindOf(Action)).oclAsType(Action).output)->asSet())
Name: spec
Related element: StructuredActivityNode-targetNodes
Language: OCL
Formal wording:
result = (node->union(output.oclAsType(ActivityNode)->asSet())-> union(node->select(oclIsKindOf(Action)).oclAsType(Action).input)->asSet())
Name: spec
Related element: StructuredActivityNode-containingActivity
Language: OCL
Formal wording:
result = (self.Action::containingActivity())
Name: multiplicity
Related element: TestIdentityAction
Description: The multiplicity of the InputPins is 1..1.
Language: OCL
Formal wording:
first.is(1,1) and second.is(1,1)
Name: no_type
Related element: TestIdentityAction
Description: The InputPins have no type.
Language: OCL
Formal wording:
first.type= null and second.type = null
Name: result_is_boolean
Related element: TestIdentityAction
Description: The type of the result OutputPin is Boolean.
Language: OCL
Formal wording:
result.type=Boolean
Name: structural_feature
Related element: UnmarshallAction
Description: The unmarshallType must have at least one StructuralFeature.
Language: OCL
Formal wording:
unmarshallType.allAttributes()->size() >= 1
Name: number_of_result
Related element: UnmarshallAction
Description: The number of result outputPins must be the same as the number of attributes of the unmarshallType.
Language: OCL
Formal wording:
unmarshallType.allAttributes()->size() = result->size()
Name: type_ordering_and_multiplicity
Related element: UnmarshallAction
Description: The type, ordering and multiplicity of each attribute of the unmarshallType must be compatible with the type, ordering and multiplicity of the corresponding result OutputPin.
Language: OCL
Formal wording:
let attribute:OrderedSet(Property) = unmarshallType.allAttributes() in
Sequence{1..result->size()}->forAll(i |
attribute->at(i).type.conformsTo(result->at(i).type) and
attribute->at(i).isOrdered=result->at(i).isOrdered and
attribute->at(i).compatibleWith(result->at(i)))
Name: multiplicity_of_object
Related element: UnmarshallAction
Description: The multiplicity of the object InputPin is 1..1
Language: OCL
Formal wording:
object.is(1,1)
Name: object_type
Related element: UnmarshallAction
Description: The type of the object InputPin conform to the unmarshallType.
Language: OCL
Formal wording:
object.type.conformsTo(unmarshallType)
Name: no_incoming_edges
Related element: ValuePin
Description: A ValuePin may have no incoming ActivityEdges.
Language: OCL
Formal wording:
incoming->isEmpty()
Name: compatible_type
Related element: ValuePin
Description: The type of the value ValueSpecification must conform to the type of the ValuePin.
Language: OCL
Formal wording:
value.type.conformsTo(type)