import primitives : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/PrimitiveTypes.xmi#_0'
import uml : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#_0'
import actions : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#Actions'
import activities : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#Activities'
import classification : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#Classification'
import commonBehavior : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#CommonBehavior'
import commonStructure : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#CommonStructure'
import deployments : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#Deployments'
import informationFlows : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#InformationFlows'
import interactions : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#Interactions'
import packages : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#Packages'
import simpleClassifiers : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#SimpleClassifiers'
import stateMachines : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#StateMachines'
import structuredClassifiers : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#StructuredClassifiers'
import useCases : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#UseCases'
import values : 'platform:/resource/org.eclipse.ocl.examples.uml25/model/UML.xmi#Values'

package uml::Activities

	context uml::Activities::Activity

	inv maximum_one_parameter_node:
		ownedParameter->forAll(p | p.direction <> UML::Classification::ParameterDirectionKind::inout implies
		  node->select(
		    (
		      oclIsKindOf(activities::ActivityParameterNode) and
		      oclAsType(activities::ActivityParameterNode).parameter = p
		    ))
		  ->size() = 1)

	inv maximum_two_parameter_nodes:
		ownedParameter->forAll(p | p.direction = UML::Classification::ParameterDirectionKind::inout implies
		  let
		    associatedNodes : Set(activities::ActivityNode) = node->select(
		      oclIsKindOf(activities::ActivityParameterNode) and
		      oclAsType(activities::ActivityParameterNode).parameter = p)
		  in
		    associatedNodes->size() = 2 and
		    associatedNodes->select(incoming->notEmpty())
		    ->size() <= 1 and
		    associatedNodes->select(outgoing->notEmpty())
		    ->size() <= 1)

	context uml::Activities::Activity::isReadOnly : Boolean

	init:
	false

	context uml::Activities::Activity::isSingleExecution : Boolean

	init:
	false

	context uml::Activities::ActivityEdge

	inv source_and_target:
		activity <> null implies
		source.containingActivity() = activity and
		target.containingActivity() = activity

	context ActivityEdge::isConsistentWith(redefiningElement : uml::Classification::RedefinableElement) : Boolean

	body:
	(redefiningElement.oclIsKindOf(ActivityEdge))

	context uml::Activities::ActivityGroup

	inv nodes_and_edges:
		containedNode->forAll(activity = self.containingActivity()) and
		containedEdge->forAll(activity = self.containingActivity())

	inv not_contained:
		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)

	context ActivityGroup::containingActivity() : uml::Activities::Activity

	body:
	(if superGroup<>null then superGroup.containingActivity()
else inActivity
endif)

	context uml::Activities::ActivityParameterNode

	inv no_outgoing_edges:
		incoming->notEmpty() and
		outgoing->isEmpty() implies parameter.direction = UML::Classification::ParameterDirectionKind::out or parameter.direction = UML::Classification::ParameterDirectionKind::inout or parameter.direction = UML::Classification::ParameterDirectionKind::return

	inv has_parameters:
		activity.ownedParameter->includes(parameter)

	inv same_type:
		type = parameter.type

	inv no_incoming_edges:
		outgoing->notEmpty() and
		incoming->isEmpty() implies parameter.direction = UML::Classification::ParameterDirectionKind::_'in' or parameter.direction = UML::Classification::ParameterDirectionKind::inout

	inv no_edges:
		incoming->isEmpty() or outgoing->isEmpty()

	context uml::Activities::ActivityPartition

	inv represents_classifier:
		not isExternal and
		represents.oclIsKindOf(classification::Classifier) and
		superPartition->notEmpty() implies
		let
		  representedClassifier : classification::Classifier = represents.oclAsType(classification::Classifier)
		in
		  superPartition.represents.oclIsKindOf(classification::Classifier) and
		  let
		    representedSuperClassifier : classification::Classifier = superPartition.represents.oclAsType(classification::Classifier)
		  in
		    (
		      representedSuperClassifier.oclIsKindOf(simpleClassifiers::BehavioredClassifier) and
		      representedClassifier.oclIsKindOf(commonBehavior::Behavior) and
		      representedSuperClassifier.oclAsType(simpleClassifiers::BehavioredClassifier)
		      .ownedBehavior->includes(
		        representedClassifier.oclAsType(commonBehavior::Behavior)) or
		      representedSuperClassifier.oclIsKindOf(structuredClassifiers::Class) and
		      representedSuperClassifier.oclAsType(structuredClassifiers::Class)
		      .nestedClassifier->includes(representedClassifier) or
		      structuredClassifiers::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)))
		    )

	inv represents_property_and_is_contained:
		represents.oclIsKindOf(classification::Property) and
		superPartition->notEmpty() implies
		superPartition.represents.oclIsKindOf(classification::Classifier) and represents.owner = superPartition.represents or
		superPartition.represents.oclIsKindOf(classification::Property) and represents.owner =
		superPartition.represents.oclAsType(classification::Property).type

	inv represents_property:
		represents.oclIsKindOf(classification::Property) and
		superPartition->notEmpty() and
		superPartition.represents.oclIsKindOf(classification::Classifier) implies
		let
		  representedClassifier : classification::Classifier = superPartition.represents.oclAsType(classification::Classifier)
		in
		  superPartition.subpartition->reject(isExternal)
		  ->forAll(p |
		    p.represents.oclIsKindOf(classification::Property) and p.owner = representedClassifier)

	inv dimension_not_contained:
		isDimension implies superPartition->isEmpty()

	context uml::Activities::ActivityPartition::isDimension : Boolean

	init:
	false

	context uml::Activities::ActivityPartition::isExternal : Boolean

	init:
	false

	context uml::Activities::ControlFlow

	inv object_nodes:
		(
		  source.oclIsKindOf(activities::ObjectNode) implies
		  source.oclAsType(activities::ObjectNode).isControlType
		) and
		(
		  target.oclIsKindOf(activities::ObjectNode) implies
		  target.oclAsType(activities::ObjectNode).isControlType
		)

	context uml::Activities::DecisionNode

	inv zero_input_parameters:
		decisionInput <> null and decisionInputFlow = null and
		incoming->exists(oclIsKindOf(activities::ControlFlow)) implies
		decisionInput.inputParameters()
		->isEmpty()

	inv edges:
		let
		  allEdges : Set(activities::ActivityEdge) = incoming->union(outgoing)
		in
		  let
		    allRelevantEdges : Set(activities::ActivityEdge) = if
		      decisionInputFlow->notEmpty()
		    then allEdges->excluding(decisionInputFlow)
		    else allEdges
		    endif
		  in
		    allRelevantEdges->forAll(
		      oclIsKindOf(activities::ControlFlow)) or
		    allRelevantEdges->forAll(
		      oclIsKindOf(activities::ObjectFlow))

	inv decision_input_flow_incoming:
		incoming->includes(decisionInputFlow)

	inv two_input_parameters:
		decisionInput <> null and decisionInputFlow <> null and
		incoming->forAll(oclIsKindOf(activities::ObjectFlow)) implies
		decisionInput.inputParameters()
		->size() = 2

	inv incoming_outgoing_edges:
		(incoming->size() = 1 or incoming->size() = 2
		) and
		outgoing->size() > 0

	inv incoming_control_one_input_parameter:
		decisionInput <> null and decisionInputFlow <> null and
		incoming->exists(oclIsKindOf(activities::ControlFlow)) implies
		decisionInput.inputParameters()
		->size() = 1

	inv parameters:
		decisionInput <> null implies
		decisionInput.ownedParameter->forAll(par | par.direction <> UML::Classification::ParameterDirectionKind::out and par.direction <> UML::Classification::ParameterDirectionKind::inout) and
		decisionInput.ownedParameter->one(par | par.direction <> UML::Classification::ParameterDirectionKind::return)

	inv incoming_object_one_input_parameter:
		decisionInput <> null and decisionInputFlow = null and
		incoming->forAll(oclIsKindOf(activities::ObjectFlow)) implies
		decisionInput.inputParameters()
		->size() = 1

	context uml::Activities::ExceptionHandler

	inv handler_body_edges:
		handlerBody.incoming->isEmpty() and
		handlerBody.outgoing->isEmpty() and
		exceptionInput.incoming->isEmpty()

	inv output_pins:
		protectedNode.oclIsKindOf(actions::Action) and
		protectedNode.oclAsType(actions::Action)
		.output->notEmpty() implies
		handlerBody.oclIsKindOf(actions::Action) and
		let
		  protectedNodeOutput : OrderedSet(actions::OutputPin) = protectedNode.oclAsType(actions::Action).output
		in
		  let
		    handlerBodyOutput : OrderedSet(actions::OutputPin) = handlerBody.oclAsType(actions::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)))

	inv one_input:
		handlerBody.oclIsKindOf(actions::Action) and
		let
		  inputs : OrderedSet(actions::InputPin) = handlerBody.oclAsType(actions::Action).input
		in inputs->size() = 1 and inputs->first() = exceptionInput

	inv edge_source_target:
		let
		  nodes : Set(activities::ActivityNode) = handlerBody.oclAsType(actions::Action)
		  .allOwnedNodes()
		in
		  nodes.outgoing->forAll(nodes->includes(target)) and
		  nodes.incoming->forAll(nodes->includes(source))

	inv handler_body_owner:
		handlerBody.owner = protectedNode.owner

	inv exception_input_type:
		exceptionInput.type = null or
		exceptionType->forAll(
		  conformsTo(
		    exceptionInput.type.oclAsType(classification::Classifier)))

	context uml::Activities::FinalNode

	inv no_outgoing_edges:
		outgoing->isEmpty()

	context uml::Activities::ForkNode

	inv edges:
		let
		  allEdges : Set(activities::ActivityEdge) = incoming->union(outgoing)
		in
		  allEdges->forAll(oclIsKindOf(activities::ControlFlow)) or
		  allEdges->forAll(oclIsKindOf(activities::ObjectFlow))

	inv one_incoming_edge:
		incoming->size() = 1

	context uml::Activities::InitialNode

	inv no_incoming_edges:
		incoming->isEmpty()

	inv control_edges:
		outgoing->forAll(oclIsKindOf(activities::ControlFlow))

	context uml::Activities::InterruptibleActivityRegion

	inv interrupting_edges:
		interruptingEdge->forAll(edge |
		  node->includes(edge.source) and
		  node->excludes(edge.target) and
		  edge.target.containingActivity() = inActivity)

	context uml::Activities::JoinNode

	inv one_outgoing_edge:
		outgoing->size() = 1

	inv incoming_object_flow:
		if
		  incoming->exists(oclIsKindOf(activities::ObjectFlow))
		then
		  outgoing->forAll(oclIsKindOf(activities::ObjectFlow))
		else
		  outgoing->forAll(oclIsKindOf(activities::ControlFlow))
		endif

	context uml::Activities::JoinNode::isCombineDuplicate : Boolean

	init:
	true

	context uml::Activities::MergeNode

	inv one_outgoing_edge:
		outgoing->size() = 1

	inv edges:
		let
		  allEdges : Set(activities::ActivityEdge) = incoming->union(outgoing)
		in
		  allEdges->forAll(oclIsKindOf(activities::ControlFlow)) or
		  allEdges->forAll(oclIsKindOf(activities::ObjectFlow))

	context uml::Activities::ObjectFlow

	inv input_and_output_parameter:
		selection <> null implies
		selection.inputParameters()
		->size() = 1 and
		selection.inputParameters()
		->forAll(not isUnique and is(0, *)) and
		selection.outputParameters()
		->size() = 1

	inv no_executable_nodes:
		not (
		  source.oclIsKindOf(activities::ExecutableNode) or
		  target.oclIsKindOf(activities::ExecutableNode)
		)

	inv transformation_behavior:
		transformation <> null implies
		transformation.inputParameters()
		->size() = 1 and
		transformation.outputParameters()
		->size() = 1

	inv selection_behavior:
		selection <> null implies
		source.oclIsKindOf(activities::ObjectNode)

	inv compatible_types:
		null

	inv same_upper_bounds:
		null

	inv target:
		null

	inv is_multicast_or_is_multireceive:
		not (isMulticast and isMultireceive)

	context uml::Activities::ObjectFlow::isMulticast : Boolean

	init:
	false

	context uml::Activities::ObjectFlow::isMultireceive : Boolean

	init:
	false

	context uml::Activities::ObjectNode

	inv input_output_parameter:
		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))

	inv selection_behavior:
		selection <> null = ordering = UML::Activities::ObjectNodeOrderingKind::ordered

	inv object_flow_edges:
		not isControlType implies
		incoming->union(outgoing)
		->forAll(oclIsKindOf(activities::ObjectFlow))

	context uml::Activities::ObjectNode::isControlType : Boolean

	init:
	false

	context uml::Activities::ObjectNode::ordering : uml::Activities::ObjectNodeOrderingKind

	init:
	UML::Activities::ObjectNodeOrderingKind::FIFO

	context ActivityNode::containingActivity() : uml::Activities::Activity

	body:
	(if inStructuredNode<>null then inStructuredNode.containingActivity()
else activity
endif)

	context ActivityNode::isConsistentWith(redefiningElement : uml::Classification::RedefinableElement) : Boolean

	body:
	(redefiningElement.oclIsKindOf(ActivityNode))

	context Variable::isAccessibleBy(a : uml::Actions::Action) : Boolean

	body:
	(if scope<>null then scope.allOwnedNodes()->includes(a)
else a.containingActivity()=activityScope
endif)

endpackage

package uml::Values

	context uml::Values::Duration

	inv no_expr_requires_observation:
		expr = null implies
		observation->size() = 1 and
		observation->forAll(
		  oclIsKindOf(values::DurationObservation))

	context uml::Values::DurationConstraint

	inv first_event_multiplicity:
		if constrainedElement->size() = 2
		then firstEvent->size() = 2
		else firstEvent->size() = 0
		endif

	inv has_one_or_two_constrainedElements:
		constrainedElement->size() = 1 or constrainedElement->size() = 2

	context uml::Values::DurationObservation

	inv first_event_multiplicity:
		if event->size() = 2
		then firstEvent->size() = 2
		else firstEvent->size() = 0
		endif

	context uml::Values::OpaqueExpression

	inv language_body_size:
		language->notEmpty() implies _'body'->size() = language->size()

	inv one_return_result_parameter:
		behavior <> null implies
		behavior.ownedParameter->select(direction = UML::Classification::ParameterDirectionKind::return)
		->size() = 1

	inv only_return_result_parameters:
		behavior <> null implies
		behavior.ownedParameter->select(direction <> UML::Classification::ParameterDirectionKind::return)
		->isEmpty()

	context OpaqueExpression::isNonNegative() : Boolean

	pre _'pre':
		self.isIntegral()

	body:
	(false)

	context OpaqueExpression::isPositive() : Boolean

	pre _'pre':
		self.isIntegral()

	body:
	(false)

	context OpaqueExpression::value() : Integer

	pre _'pre':
		self.isIntegral()

	body:
	(0)

	context OpaqueExpression::isIntegral() : Boolean

	body:
	(false)

	context OpaqueExpression::result() : uml::Classification::Parameter

	body:
	(if behavior = null then
	null
else
	behavior.ownedParameter->first()
endif)

	context uml::Values::StringExpression

	inv operands:
		operand->forAll(oclIsKindOf(values::LiteralString))

	inv subexpressions:
		if subExpression->notEmpty()
		then operand->isEmpty()
		else operand->notEmpty()
		endif

	context StringExpression::stringValue() : String

	body:
	(if subExpression->notEmpty()
then subExpression->iterate(se; stringValue: String = '' | stringValue.concat(se.stringValue()))
else operand->iterate(op; stringValue: String = '' | stringValue.concat(op.stringValue()))
endif)

	context uml::Values::TimeConstraint

	inv has_one_constrainedElement:
		constrainedElement->size() = 1

	context uml::Values::TimeConstraint::firstEvent : Boolean

	init:
	true

	context uml::Values::TimeExpression

	inv no_expr_requires_observation:
		expr = null implies
		observation->size() = 1 and
		observation->forAll(
		  oclIsKindOf(values::TimeObservation))

	context LiteralBoolean::booleanValue() : Boolean

	body:
	(value)

	context LiteralBoolean::isComputable() : Boolean

	body:
	(true)

	context uml::Values::LiteralBoolean::value : Boolean

	init:
	false

	context LiteralInteger::integerValue() : Integer

	body:
	(value)

	context LiteralInteger::isComputable() : Boolean

	body:
	(true)

	context uml::Values::LiteralInteger::value : Integer

	init:
	0

	context LiteralNull::isComputable() : Boolean

	body:
	(true)

	context LiteralNull::isNull() : Boolean

	body:
	(true)

	context LiteralReal::isComputable() : Boolean

	body:
	(true)

	context LiteralReal::realValue() : Real

	body:
	(value)

	context LiteralString::isComputable() : Boolean

	body:
	(true)

	context LiteralString::stringValue() : String

	body:
	(value)

	context LiteralUnlimitedNatural::isComputable() : Boolean

	body:
	(true)

	context LiteralUnlimitedNatural::unlimitedValue() : UnlimitedNatural

	body:
	(value)

	context uml::Values::LiteralUnlimitedNatural::value : UnlimitedNatural

	init:
	0

	context uml::Values::TimeObservation::firstEvent : Boolean

	init:
	true

	context ValueSpecification::booleanValue() : Boolean

	body:
	(null)

	context ValueSpecification::integerValue() : Integer

	body:
	(null)

	context ValueSpecification::isCompatibleWith(p : uml::CommonStructure::ParameterableElement) : Boolean

	body:
	(self.oclIsKindOf(p.oclType()) and (p.oclIsKindOf(TypedElement) implies 
self.type.conformsTo(p.oclAsType(TypedElement).type)))

	context ValueSpecification::isComputable() : Boolean

	body:
	(false)

	context ValueSpecification::isNull() : Boolean

	body:
	(false)

	context ValueSpecification::realValue() : Real

	body:
	(null)

	context ValueSpecification::stringValue() : String

	body:
	(null)

	context ValueSpecification::unlimitedValue() : UnlimitedNatural

	body:
	(null)

endpackage

package uml::UseCases

	context uml::UseCases::Actor

	inv associations:
		structuredClassifiers::Association.allInstances()
		->forAll(a |
		  a.memberEnd->collect(type)
		  ->includes(self) implies
		  a.memberEnd->size() = 2 and
		  let actorEnd : classification::Property = a.memberEnd->any(type = self)
		  in
		    (
		      actorEnd.opposite.class.oclIsKindOf(useCases::UseCase) or
		      actorEnd.opposite.class.oclIsKindOf(structuredClassifiers::Class) and
		      not actorEnd.opposite.class.oclIsKindOf(commonBehavior::Behavior)
		    ))

	inv must_have_name:
		name->notEmpty()

	context uml::UseCases::Extend

	inv extension_points:
		extensionLocation->forAll(xp | extendedCase.extensionPoint->includes(xp))

	context uml::UseCases::ExtensionPoint

	inv must_have_name:
		name->notEmpty()

	context uml::UseCases::UseCase

	inv binary_associations:
		structuredClassifiers::Association.allInstances()
		->forAll(a |
		  a.memberEnd.type->includes(self) implies
		  a.memberEnd->size() = 2)

	inv no_association_to_use_case:
		structuredClassifiers::Association.allInstances()
		->forAll(a |
		  a.memberEnd.type->includes(self) implies
		  let
		    usecases : Set(useCases::UseCase) = a.memberEnd.type->select(
		      oclIsKindOf(useCases::UseCase))
		    ->collect(oclAsType(useCases::UseCase))
		    ->asSet()
		  in
		    usecases->size() > 1 implies
		    usecases->collect(subject)
		    ->size() > 1)

	inv cannot_include_self:
		not allIncludedUseCases()->includes(self)

	inv must_have_name:
		name->notEmpty()

	context UseCase::allIncludedUseCases() : Set(uml::UseCases::UseCase)

	body:
	(self.include.addition->union(self.include.addition->collect(uc | uc.allIncludedUseCases()))->asSet())

endpackage

package uml::StructuredClassifiers

	context uml::StructuredClassifiers::Association

	inv specialized_end_number:
		parents()
		->select(
		  oclIsKindOf(structuredClassifiers::Association))
		.oclAsType(structuredClassifiers::Association)
		->forAll(p | p.memberEnd->size() = self.memberEnd->size())

	inv specialized_end_types:
		Sequence{1..memberEnd->size()
		}
		->forAll(i |
		  general->select(
		    oclIsKindOf(structuredClassifiers::Association))
		  .oclAsType(structuredClassifiers::Association)
		  ->forAll(ga |
		    self.memberEnd->at(i)
		    .type.conformsTo(ga.memberEnd->at(i).type)))

	inv binary_associations:
		memberEnd->exists(aggregation <> UML::Classification::AggregationKind::none) implies
		memberEnd->size() = 2 and
		memberEnd->exists(aggregation = UML::Classification::AggregationKind::none)

	inv association_ends:
		memberEnd->size() > 2 implies ownedEnd->includesAll(memberEnd)

	inv ends_must_be_typed:
		memberEnd->forAll(type->notEmpty())

	context Association::endType() : Set(uml::CommonStructure::Type)

	body:
	(memberEnd->collect(type)->asSet())

	context uml::StructuredClassifiers::Association::isDerived : Boolean

	init:
	false

	context uml::StructuredClassifiers::AssociationClass

	inv cannot_be_defined:
		self.endType()
		->excludes(self) and
		self.endType()
		->collect(et |
		  et.oclAsType(classification::Classifier)
		  .allParents())
		->flatten()
		->excludes(self)

	inv disjoint_attributes_ends:
		ownedAttribute->intersection(ownedEnd)->isEmpty()

	context uml::StructuredClassifiers::Class

	inv passive_class:
		not isActive implies ownedReception->isEmpty() and classifierBehavior = null

	context Class::extension() : Set(uml::Packages::Extension)

	body:
	(Extension.allInstances()->select(ext | 
  let endTypes : Sequence(Classifier) = ext.memberEnd->collect(type.oclAsType(Classifier)) in
  endTypes->includes(self) or endTypes.allParents()->includes(self) ))

	context Class::superClass() : Set(uml::StructuredClassifiers::Class)

	body:
	(self.general()->select(oclIsKindOf(Class))->collect(oclAsType(Class))->asSet())

	context uml::StructuredClassifiers::Class::isAbstract : Boolean

	init:
	false

	context uml::StructuredClassifiers::Class::isActive : Boolean

	init:
	false

	context uml::StructuredClassifiers::CollaborationUse

	inv client_elements:
		roleBinding->collect(client)
		->forAll(ne1, ne2 |
		  ne1.oclIsKindOf(structuredClassifiers::ConnectableElement) and
		  ne2.oclIsKindOf(structuredClassifiers::ConnectableElement) and
		  let
		    ce1 : structuredClassifiers::ConnectableElement = ne1.oclAsType(structuredClassifiers::ConnectableElement)
		  in
		    let
		      ce2 : structuredClassifiers::ConnectableElement = ne2.oclAsType(structuredClassifiers::ConnectableElement)
		    in ce1.structuredClassifier = ce2.structuredClassifier) and
		roleBinding->collect(supplier)
		->forAll(ne1, ne2 |
		  ne1.oclIsKindOf(structuredClassifiers::ConnectableElement) and
		  ne2.oclIsKindOf(structuredClassifiers::ConnectableElement) and
		  let
		    ce1 : structuredClassifiers::ConnectableElement = ne1.oclAsType(structuredClassifiers::ConnectableElement)
		  in
		    let
		      ce2 : structuredClassifiers::ConnectableElement = ne2.oclAsType(structuredClassifiers::ConnectableElement)
		    in ce1.collaboration = ce2.collaboration)

	inv every_role:
		type.collaborationRole->forAll(role |
		  roleBinding->exists(rb | rb.supplier->includes(role)))

	inv connectors:
		type.ownedConnector->forAll(connector |
		  let
		    rolesConnectedInCollab : Set(structuredClassifiers::ConnectableElement) = connector.end.role->asSet()
		  in
		    let
		      relevantBindings : Set(commonStructure::Dependency) = roleBinding->select(rb |
		        rb.supplier->intersection(rolesConnectedInCollab)
		        ->notEmpty())
		    in
		      let
		        boundRoles : Set(structuredClassifiers::ConnectableElement) = relevantBindings->collect(
		          client.oclAsType(structuredClassifiers::ConnectableElement))
		        ->asSet()
		      in
		        let
		          contextClassifier : structuredClassifiers::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))))

	context uml::StructuredClassifiers::Component

	inv no_nested_classifiers:
		nestedClassifier->isEmpty()

	inv no_packaged_elements:
		nestingClass <> null implies packagedElement->isEmpty()

	context Component::provided() : Set(uml::SimpleClassifiers::Interface)

	body:
	(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())

	context Component::required() : Set(uml::SimpleClassifiers::Interface)

	body:
	(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()
)

	context uml::StructuredClassifiers::Component::isIndirectlyInstantiated : Boolean

	init:
	true

	context uml::StructuredClassifiers::Connector

	inv types:
		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))

	inv roles:
		structuredClassifier <> null and
		end->forAll(e |
		  (
		    structuredClassifier.allRoles()
		    ->includes(e.role) or
		    e.role.oclIsKindOf(structuredClassifiers::Port) and
		    structuredClassifier.allRoles()
		    ->includes(e.partWithPort)
		  ))

	context Connector::kind() : uml::StructuredClassifiers::ConnectorKind

	body:
	(if end->exists(
		role.oclIsKindOf(Port) 
		and partWithPort->isEmpty()
		and not role.oclAsType(Port).isBehavior)
then ConnectorKind::delegation 
else ConnectorKind::assembly 
endif)

	context uml::StructuredClassifiers::ConnectorEnd

	inv role_and_part_with_port:
		partWithPort->notEmpty() implies
		role.oclIsKindOf(structuredClassifiers::Port) and
		partWithPort.type.oclAsType(commonStructure::Namespace)
		.member->includes(role)

	inv part_with_port_empty:
		role.oclIsKindOf(structuredClassifiers::Port) and role.owner = connector.owner implies
		partWithPort->isEmpty()

	inv multiplicity:
		self.compatibleWith(definingEnd)

	inv self_part_with_port:
		partWithPort->notEmpty() implies
		not partWithPort.oclIsKindOf(structuredClassifiers::Port)

	context ConnectorEnd::definingEnd() : uml::Classification::Property

	body:
	(if connector.type = null 
then
  null 
else
  let index : Integer = connector.end->indexOf(self) in
    connector.type.memberEnd->at(index)
endif)

	context uml::StructuredClassifiers::Port

	inv port_aggregation:
		aggregation = UML::Classification::AggregationKind::composite

	inv default_value:
		type.oclIsKindOf(simpleClassifiers::Interface) implies
		defaultValue->isEmpty()

	inv encapsulated_owner:
		owner = encapsulatedClassifier

	context Port::provided() : Set(uml::SimpleClassifiers::Interface)

	body:
	(if isConjugated then basicRequired() else basicProvided() endif)

	context Port::required() : Set(uml::SimpleClassifiers::Interface)

	body:
	(if isConjugated then basicProvided() else basicRequired() endif)

	context Port::basicProvided() : Set(uml::SimpleClassifiers::Interface)

	body:
	(if type.oclIsKindOf(Interface) 
then type.oclAsType(Interface)->asSet() 
else type.oclAsType(Classifier).allRealizedInterfaces() 
endif)

	context Port::basicRequired() : Set(uml::SimpleClassifiers::Interface)

	body:
	( type.oclAsType(Classifier).allUsedInterfaces() )

	context uml::StructuredClassifiers::Port::isBehavior : Boolean

	init:
	false

	context uml::StructuredClassifiers::Port::isConjugated : Boolean

	init:
	false

	context uml::StructuredClassifiers::Port::isService : Boolean

	init:
	true

	context ConnectableElement::end() : Set(uml::StructuredClassifiers::ConnectorEnd)

	body:
	(ConnectorEnd.allInstances()->select(role = self))

	context EncapsulatedClassifier::ownedPort() : OrderedSet(uml::StructuredClassifiers::Port)

	body:
	(ownedAttribute->select(oclIsKindOf(Port))->collect(oclAsType(Port))->asOrderedSet())

	context StructuredClassifier::part() : Set(uml::Classification::Property)

	body:
	(ownedAttribute->select(isComposite))

	context StructuredClassifier::allRoles() : Set(uml::StructuredClassifiers::ConnectableElement)

	body:
	(allFeatures()->select(oclIsKindOf(ConnectableElement))->collect(oclAsType(ConnectableElement))->asSet())

endpackage

package uml::StateMachines

	context uml::StateMachines::ConnectionPointReference

	inv exit_pseudostates:
		exit->forAll(kind = UML::StateMachines::PseudostateKind::exitPoint)

	inv entry_pseudostates:
		entry->forAll(kind = UML::StateMachines::PseudostateKind::entryPoint)

	context uml::StateMachines::FinalState

	inv no_exit_behavior:
		exit->isEmpty()

	inv no_outgoing_transitions:
		outgoing->size() = 0

	inv no_regions:
		region->size() = 0

	inv cannot_reference_submachine:
		submachine->isEmpty()

	inv no_entry_behavior:
		entry->isEmpty()

	inv no_state_behavior:
		doActivity->isEmpty()

	context uml::StateMachines::ProtocolStateMachine

	inv classifier_context:
		_'context' <> null and specification = null

	inv deep_or_shallow_history:
		region->forAll(r |
		  r.subvertex->forAll(v |
		    v.oclIsKindOf(stateMachines::Pseudostate) implies
		    v.oclAsType(stateMachines::Pseudostate).kind <> UML::StateMachines::PseudostateKind::deepHistory and
		    v.oclAsType(stateMachines::Pseudostate).kind <> UML::StateMachines::PseudostateKind::shallowHistory))

	inv entry_exit_do:
		region->forAll(r |
		  r.subvertex->forAll(v |
		    v.oclIsKindOf(stateMachines::State) implies
		    v.oclAsType(stateMachines::State)
		    .entry->isEmpty() and
		    v.oclAsType(stateMachines::State)
		    .exit->isEmpty() and
		    v.oclAsType(stateMachines::State)
		    .doActivity->isEmpty()))

	inv protocol_transitions:
		region->forAll(r |
		  r.transition->forAll(t |
		    t.oclIsTypeOf(stateMachines::ProtocolTransition)))

	context uml::StateMachines::ProtocolTransition

	inv refers_to_operation:
		if referred()->notEmpty() and containingStateMachine()._'context'->notEmpty()
		then
		  containingStateMachine()
		  ._'context'.oclAsType(simpleClassifiers::BehavioredClassifier)
		  .allFeatures()
		  ->includesAll(referred())
		else true
		endif

	inv associated_actions:
		effect = null

	inv belongs_to_psm:
		container.belongsToPSM()

	context ProtocolTransition::referred() : Set(uml::Classification::Operation)

	body:
	(trigger->collect(event)->select(oclIsKindOf(CallEvent))->collect(oclAsType(CallEvent).operation)->asSet())

	context uml::StateMachines::Pseudostate

	inv transitions_outgoing:
		kind = UML::StateMachines::PseudostateKind::fork implies
		outgoing->forAll(t1, t2 |
		  let
		    contState : stateMachines::State = containingStateMachine()
		    .LCAState(t1.target, t2.target)
		  in contState <> null and
		    contState.region->exists(r1, r2 | r1 <> r2 and
		      t1.target.isContainedInRegion(r1) and
		      t2.target.isContainedInRegion(r2)))

	inv choice_vertex:
		kind = UML::StateMachines::PseudostateKind::choice implies
		incoming->size() >= 1 and
		outgoing->size() >= 1

	inv outgoing_from_initial:
		kind = UML::StateMachines::PseudostateKind::initial implies outgoing.guard = null and
		outgoing.trigger->isEmpty()

	inv join_vertex:
		kind = UML::StateMachines::PseudostateKind::join implies
		outgoing->size() = 1 and
		incoming->size() >= 2

	inv junction_vertex:
		kind = UML::StateMachines::PseudostateKind::junction implies
		incoming->size() >= 1 and
		outgoing->size() >= 1

	inv history_vertices:
		kind = UML::StateMachines::PseudostateKind::deepHistory or kind = UML::StateMachines::PseudostateKind::shallowHistory implies
		outgoing->size() <= 1

	inv initial_vertex:
		kind = UML::StateMachines::PseudostateKind::initial implies outgoing->size() <= 1

	inv fork_vertex:
		kind = UML::StateMachines::PseudostateKind::fork implies
		incoming->size() = 1 and
		outgoing->size() >= 2

	inv transitions_incoming:
		kind = UML::StateMachines::PseudostateKind::join implies
		incoming->forAll(t1, t2 |
		  let
		    contState : stateMachines::State = containingStateMachine()
		    .LCAState(t1.source, t2.source)
		  in contState <> null and
		    contState.region->exists(r1, r2 | r1 <> r2 and
		      t1.source.isContainedInRegion(r1) and
		      t2.source.isContainedInRegion(r2)))

	context uml::StateMachines::Pseudostate::kind : uml::StateMachines::PseudostateKind

	init:
	UML::StateMachines::PseudostateKind::initial

	context uml::StateMachines::Region

	inv deep_history_vertex:
		self.subvertex->select(
		  oclIsKindOf(stateMachines::Pseudostate))
		->collect(oclAsType(stateMachines::Pseudostate))
		->select((kind = UML::StateMachines::PseudostateKind::deepHistory))
		->size() <= 1

	inv shallow_history_vertex:
		subvertex->select(
		  oclIsKindOf(stateMachines::Pseudostate))
		->collect(oclAsType(stateMachines::Pseudostate))
		->select((kind = UML::StateMachines::PseudostateKind::shallowHistory))
		->size() <= 1

	inv owned:
		(stateMachine <> null implies state = null
		) and
		(state <> null implies stateMachine = null
		)

	inv initial_vertex:
		self.subvertex->select(
		  oclIsKindOf(stateMachines::Pseudostate))
		->collect(oclAsType(stateMachines::Pseudostate))
		->select((kind = UML::StateMachines::PseudostateKind::initial))
		->size() <= 1

	context Region::isConsistentWith(redefiningElement : uml::Classification::RedefinableElement) : Boolean

	pre _'pre':
		redefiningElement.isRedefinitionContextValid(self)

	body:
	(-- the following is merely a default body; it is expected that the specific form of this constraint will be specified by profiles
true)

	context Region::belongsToPSM() : Boolean

	body:
	(if  stateMachine <> null 
then
  stateMachine.oclIsKindOf(ProtocolStateMachine)
else 
  state <> null  implies  state.container.belongsToPSM()
endif )

	context Region::containingStateMachine() : uml::StateMachines::StateMachine

	body:
	(if stateMachine = null 
then
  state.containingStateMachine()
else
  stateMachine
endif)

	context Region::isRedefinitionContextValid(redefinedElement : uml::Classification::RedefinableElement) : Boolean

	body:
	(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)

	context Region::redefinitionContext() : uml::Classification::Classifier

	body:
	(let sm : StateMachine = containingStateMachine() in
if sm._'context' = null or sm.general->notEmpty() then
  sm
else
  sm._'context'
endif)

	context uml::StateMachines::State

	inv entry_or_exit:
		connectionPoint->forAll(kind = UML::StateMachines::PseudostateKind::entryPoint or kind = UML::StateMachines::PseudostateKind::exitPoint)

	inv submachine_states:
		isSubmachineState implies connection->notEmpty()

	inv composite_states:
		connectionPoint->notEmpty() implies isComposite

	inv destinations_or_sources_of_transitions:
		self.isSubmachineState implies
		self.connection->forAll(cp |
		  cp.entry->forAll(ps | ps.stateMachine = self.submachine) and
		  cp.exit->forAll(ps | ps.stateMachine = self.submachine))

	inv submachine_or_regions:
		isComposite implies not isSubmachineState

	context State::isConsistentWith(redefiningElement : uml::Classification::RedefinableElement) : Boolean

	pre _'pre':
		redefiningElement.isRedefinitionContextValid(self)

	body:
	(-- the following is merely a default body; it is expected that the specific form of this constraint will be specified by profiles
true)

	context State::containingStateMachine() : uml::StateMachines::StateMachine

	body:
	(container.containingStateMachine())

	context State::isComposite() : Boolean

	body:
	(region->notEmpty())

	context State::isOrthogonal() : Boolean

	body:
	(region->size () > 1)

	context State::isRedefinitionContextValid(redefinedElement : uml::Classification::RedefinableElement) : Boolean

	body:
	(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)

	context State::isSimple() : Boolean

	body:
	((region->isEmpty()) and not isSubmachineState())

	context State::isSubmachineState() : Boolean

	body:
	(submachine <> null)

	context State::redefinitionContext() : uml::Classification::Classifier

	body:
	(let sm : StateMachine = containingStateMachine() in
if sm._'context' = null or sm.general->notEmpty() then
  sm
else
  sm._'context'
endif)

	context uml::StateMachines::StateMachine

	inv connection_points:
		connectionPoint->forAll(kind = UML::StateMachines::PseudostateKind::entryPoint or kind = UML::StateMachines::PseudostateKind::exitPoint)

	inv classifier_context:
		_'context' <> null implies
		not _'context'.oclIsKindOf(simpleClassifiers::Interface)

	inv method:
		specification <> null implies connectionPoint->isEmpty()

	inv context_classifier:
		specification <> null implies _'context' <> null and
		specification.featuringClassifier->exists(c | c = _'context')

	context StateMachine::LCA(s1 : uml::StateMachines::Vertex, s2 : uml::StateMachines::Vertex) :
	uml::StateMachines::Region

	body:
	(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)

	context StateMachine::ancestor(s1 : uml::StateMachines::Vertex, s2 : uml::StateMachines::Vertex) : Boolean

	body:
	(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  )

	context StateMachine::isConsistentWith(redefiningElement : uml::Classification::RedefinableElement) : Boolean

	body:
	(-- the following is merely a default body; it is expected that the specific form of this constraint will be specified by profiles
true)

	context StateMachine::isRedefinitionContextValid(redefinedElement : uml::Classification::RedefinableElement) :
	Boolean

	body:
	(if redefinedElement.oclIsKindOf(StateMachine) then
  let redefinedStateMachine : StateMachine = redefinedElement.oclAsType(StateMachine) in
    self._'context'().oclAsType(BehavioredClassifier).redefinedClassifier->
      includes(redefinedStateMachine._'context'())
else
  false
endif)

	context StateMachine::LCAState(v1 : uml::StateMachines::Vertex, v2 : uml::StateMachines::Vertex) :
	uml::StateMachines::State

	body:
	(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)

	context uml::StateMachines::Transition

	inv state_is_external:
		kind = UML::StateMachines::TransitionKind::external implies
		not (
		  source.oclIsKindOf(stateMachines::Pseudostate) and
		  source.oclAsType(stateMachines::Pseudostate).kind = UML::StateMachines::PseudostateKind::entryPoint
		)

	inv join_segment_guards:
		target.oclIsKindOf(stateMachines::Pseudostate) and
		target.oclAsType(stateMachines::Pseudostate).kind = UML::StateMachines::PseudostateKind::join implies guard = null and
		trigger->isEmpty()

	inv state_is_internal:
		kind = UML::StateMachines::TransitionKind::internal implies
		source.oclIsKindOf(stateMachines::State) and source = target

	inv outgoing_pseudostates:
		source.oclIsKindOf(stateMachines::Pseudostate) and
		source.oclAsType(stateMachines::Pseudostate).kind <> UML::StateMachines::PseudostateKind::initial implies
		trigger->isEmpty()

	inv join_segment_state:
		target.oclIsKindOf(stateMachines::Pseudostate) and
		target.oclAsType(stateMachines::Pseudostate).kind = UML::StateMachines::PseudostateKind::join implies
		source.oclIsKindOf(stateMachines::State)

	inv fork_segment_state:
		source.oclIsKindOf(stateMachines::Pseudostate) and
		source.oclAsType(stateMachines::Pseudostate).kind = UML::StateMachines::PseudostateKind::fork implies
		target.oclIsKindOf(stateMachines::State)

	inv state_is_local:
		kind = UML::StateMachines::TransitionKind::local implies
		source.oclIsKindOf(stateMachines::State) and
		source.oclAsType(stateMachines::State).isComposite or
		source.oclIsKindOf(stateMachines::Pseudostate) and
		source.oclAsType(stateMachines::Pseudostate).kind = UML::StateMachines::PseudostateKind::entryPoint

	inv initial_transition:
		source.oclIsKindOf(stateMachines::Pseudostate) and
		container.stateMachine->notEmpty() implies
		trigger->isEmpty()

	inv fork_segment_guards:
		source.oclIsKindOf(stateMachines::Pseudostate) and
		source.oclAsType(stateMachines::Pseudostate).kind = UML::StateMachines::PseudostateKind::fork implies guard = null and
		trigger->isEmpty()

	context Transition::isConsistentWith(redefiningElement : uml::Classification::RedefinableElement) : Boolean

	pre _'pre':
		redefiningElement.isRedefinitionContextValid(self)

	body:
	(-- the following is merely a default body; it is expected that the specific form of this constraint will be specified by profiles
true)

	context Transition::containingStateMachine() : uml::StateMachines::StateMachine

	body:
	(container.containingStateMachine())

	context Transition::redefinitionContext() : uml::Classification::Classifier

	body:
	(let sm : StateMachine = containingStateMachine() in
if sm._'context' = null or sm.general->notEmpty() then
  sm
else
  sm._'context'
endif)

	context uml::StateMachines::Transition::kind : uml::StateMachines::TransitionKind

	init:
	UML::StateMachines::TransitionKind::external

	context Vertex::containingStateMachine() : uml::StateMachines::StateMachine

	body:
	(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

)

	context Vertex::incoming() : Set(uml::StateMachines::Transition)

	body:
	(Transition.allInstances()->select(target=self))

	context Vertex::outgoing() : Set(uml::StateMachines::Transition)

	body:
	(Transition.allInstances()->select(source=self))

	context Vertex::isContainedInState(s : uml::StateMachines::State) : Boolean

	body:
	(if not s.isComposite() or container->isEmpty() then
	false
else
	if container.state = s then 
		true
	else
		container.state.isContainedInState(s)
	endif
endif)

	context Vertex::isContainedInRegion(r : uml::StateMachines::Region) : Boolean

	body:
	(if (container = r) then
	true
else
	if (r.state->isEmpty()) then
		false
	else
		container.state.isContainedInRegion(r)
	endif
endif)

endpackage

package uml::SimpleClassifiers

	context uml::SimpleClassifiers::BehavioredClassifier

	inv class_behavior:
		classifierBehavior->notEmpty() implies
		classifierBehavior.specification->isEmpty()

	context uml::SimpleClassifiers::Enumeration

	inv immutable:
		ownedAttribute->forAll(isReadOnly)

	context uml::SimpleClassifiers::Interface

	inv visibility:
		feature->forAll(visibility = UML::CommonStructure::VisibilityKind::public)

	context uml::SimpleClassifiers::Reception

	inv same_name_as_signal:
		name = signal.name

	inv same_structure_as_signal:
		signal.ownedAttribute->size() =
		ownedParameter->size() and
		Sequence{1..signal.ownedAttribute->size()
		}
		->forAll(i |
		  ownedParameter->at(i).direction = UML::Classification::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())

	context EnumerationLiteral::classifier() : uml::SimpleClassifiers::Enumeration

	body:
	(enumeration)

endpackage

package uml::Packages

	context uml::Packages::Extension

	inv non_owned_end:
		metaclassEnd()
		->notEmpty() and
		metaclassEnd()
		.type.oclIsKindOf(structuredClassifiers::Class)

	inv is_binary:
		memberEnd->size() = 2

	context Extension::isRequired() : Boolean

	body:
	(ownedEnd.lowerBound() = 1)

	context Extension::metaclass() : uml::StructuredClassifiers::Class

	body:
	(metaclassEnd().type.oclAsType(Class))

	context Extension::metaclassEnd() : uml::Classification::Property

	body:
	(memberEnd->reject(p | ownedEnd->includes(p.oclAsType(ExtensionEnd)))->any(true))

	context uml::Packages::ExtensionEnd

	inv multiplicity:
		(lowerBound() = 0 or lowerBound() = 1
		) and
		upperBound() = 1

	inv aggregation:
		self.aggregation = UML::Classification::AggregationKind::composite

	context ExtensionEnd::lowerBound() : Integer

	body:
	(if lowerValue=null then 0 else lowerValue.integerValue() endif)

	context uml::Packages::Package

	inv elements_public_or_private:
		packagedElement->forAll(e | e.visibility <> null implies e.visibility = UML::CommonStructure::VisibilityKind::public or e.visibility = UML::CommonStructure::VisibilityKind::private)

	context Package::makesVisible(el : uml::CommonStructure::NamedElement) : Boolean

	pre _'pre':
		member->includes(el)

	body:
	(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()))

	context Package::allApplicableStereotypes() : Set(uml::Packages::Stereotype)

	body:
	(let ownedPackages : Bag(Package) = ownedMember->select(oclIsKindOf(Package))->collect(oclAsType(Package)) in
 ownedStereotype->union(ownedPackages.allApplicableStereotypes())->flatten()->asSet()
)

	context Package::containingProfile() : uml::Packages::Profile

	body:
	(if self.oclIsKindOf(Profile) then 
	self.oclAsType(Profile)
else
	self.namespace.oclAsType(Package).containingProfile()
endif)

	context Package::mustBeOwned() : Boolean

	body:
	(false)

	context Package::nestedPackage() : Set(uml::Packages::Package)

	body:
	(packagedElement->select(oclIsKindOf(Package))->collect(oclAsType(Package))->asSet())

	context Package::ownedStereotype() : Set(uml::Packages::Stereotype)

	body:
	(packagedElement->select(oclIsKindOf(Stereotype))->collect(oclAsType(Stereotype))->asSet())

	context Package::ownedType() : Set(uml::CommonStructure::Type)

	body:
	(packagedElement->select(oclIsKindOf(Type))->collect(oclAsType(Type))->asSet())

	context Package::visibleMembers() : Set(uml::CommonStructure::PackageableElement)

	body:
	(member->select( m | m.oclIsKindOf(PackageableElement) and self.makesVisible(m))->collect(oclAsType(PackageableElement))->asSet())

	context uml::Packages::Profile

	inv metaclass_reference_not_specialized:
		metaclassReference.importedElement->select(c |
		  c.oclIsKindOf(classification::Classifier) and
		  c.oclAsType(classification::Classifier)
		  .allParents()
		  ->collect(namespace)
		  ->includes(self))
		->isEmpty() and
		packagedElement->select(
		  oclIsKindOf(classification::Classifier))
		->collect(
		  oclAsType(classification::Classifier)
		  .allParents())
		->intersection(
		  metaclassReference.importedElement->select(
		    oclIsKindOf(classification::Classifier))
		  ->collect(oclAsType(classification::Classifier)))
		->isEmpty()

	inv references_same_metamodel:
		metamodelReference.importedPackage.elementImport.importedElement.allOwningPackages()
		->union(metaclassReference.importedElement.allOwningPackages())
		->notEmpty()

	context uml::Packages::Stereotype

	inv binaryAssociationsOnly:
		ownedAttribute.association->forAll(memberEnd->size() = 2)

	inv generalize:
		allParents()
		->forAll(oclIsKindOf(packages::Stereotype)) and
		classification::Classifier.allInstances()
		->forAll(c |
		  (
		    c.allParents()
		    ->exists(oclIsKindOf(packages::Stereotype)) implies
		    c.oclIsKindOf(packages::Stereotype)
		  ))

	inv name_not_clash:
		null

	inv associationEndOwnership:
		ownedAttribute->select(
		  association->notEmpty() and
		  not association.oclIsKindOf(packages::Extension) and
		  not type.oclIsKindOf(packages::Stereotype))
		->forAll(opposite.owner = association)

	inv base_property_upper_bound:
		null

	inv base_property_multiplicity_single_extension:
		null

	inv base_property_multiplicity_multiple_extension:
		null

	context Stereotype::containingProfile() : uml::Packages::Profile

	body:
	(self.namespace.oclAsType(Package).containingProfile())

	context Stereotype::profile() : uml::Packages::Profile

	body:
	(self.containingProfile())

	context uml::Packages::ProfileApplication::isStrict : Boolean

	init:
	false

endpackage

package uml::Interactions

	context uml::Interactions::ActionExecutionSpecification

	inv action_referenced:
		(
		  enclosingInteraction->notEmpty() or
		  enclosingOperand.combinedFragment->notEmpty()
		) and
		let
		  parentInteraction : Set(interactions::Interaction) = enclosingInteraction.oclAsType(interactions::Interaction)
		  ->asSet()
		  ->union(
		    enclosingOperand.combinedFragment->closure(enclosingOperand.combinedFragment)
		    ->collect(enclosingInteraction)
		    .oclAsType(interactions::Interaction)
		    ->asSet())
		in
		  parentInteraction->size() = 1 and
		  self.action.interaction->asSet() = parentInteraction

	context uml::Interactions::CombinedFragment

	inv break:
		interactionOperator = UML::Interactions::InteractionOperatorKind::break implies
		enclosingInteraction.oclAsType(interactions::InteractionFragment)
		->asSet()
		->union(
		  enclosingOperand.oclAsType(interactions::InteractionFragment)
		  ->asSet())
		.covered->asSet() =
		self.covered->asSet()

	inv consider_and_ignore:
		interactionOperator = UML::Interactions::InteractionOperatorKind::consider or interactionOperator = UML::Interactions::InteractionOperatorKind::ignore implies
		oclIsKindOf(interactions::ConsiderIgnoreFragment)

	inv opt_loop_break_neg:
		interactionOperator = UML::Interactions::InteractionOperatorKind::opt or interactionOperator = UML::Interactions::InteractionOperatorKind::loop or interactionOperator = UML::Interactions::InteractionOperatorKind::break or interactionOperator = UML::Interactions::InteractionOperatorKind::assert or interactionOperator = UML::Interactions::InteractionOperatorKind::neg implies
		operand->size() = 1

	context uml::Interactions::CombinedFragment::interactionOperator : uml::Interactions::InteractionOperatorKind

	init:
	UML::Interactions::InteractionOperatorKind::seq

	context uml::Interactions::ConsiderIgnoreFragment

	inv consider_or_ignore:
		interactionOperator = UML::Interactions::InteractionOperatorKind::consider or interactionOperator = UML::Interactions::InteractionOperatorKind::ignore

	inv type:
		message->forAll(m |
		  m.oclIsKindOf(classification::Operation) or
		  m.oclIsKindOf(simpleClassifiers::Signal))

	context uml::Interactions::Continuation

	inv first_or_last_interaction_fragment:
		enclosingOperand->notEmpty() and
		let peerFragments : OrderedSet(interactions::InteractionFragment) = enclosingOperand.fragment
		in
		  peerFragments->notEmpty() and
		  (peerFragments->first() = self or peerFragments->last() = self
		  )

	inv same_name:
		enclosingOperand.combinedFragment->notEmpty() and
		let
		  parentInteraction : Set(interactions::Interaction) = enclosingOperand.combinedFragment->closure(enclosingOperand.combinedFragment)
		  ->collect(enclosingInteraction)
		  .oclAsType(interactions::Interaction)
		  ->asSet()
		in
		  parentInteraction->size() = 1 and
		  let
		    peerInteractions : Set(interactions::Interaction) = parentInteraction->union(
		      parentInteraction->collect(_'context')
		      ->collect(behavior)
		      ->select(oclIsKindOf(interactions::Interaction))
		      .oclAsType(interactions::Interaction)
		      ->asSet())
		    ->asSet()
		  in
		    peerInteractions->notEmpty() and
		    let
		      combinedFragments1 : Set(interactions::CombinedFragment) = peerInteractions.fragment->select(
		        oclIsKindOf(interactions::CombinedFragment))
		      .oclAsType(interactions::CombinedFragment)
		      ->asSet()
		    in
		      combinedFragments1->notEmpty() and
		      combinedFragments1->closure(
		        operand.fragment->select(
		          oclIsKindOf(interactions::CombinedFragment))
		        .oclAsType(interactions::CombinedFragment))
		      ->asSet()
		      .operand.fragment->select(
		        oclIsKindOf(interactions::Continuation))
		      .oclAsType(interactions::Continuation)
		      ->asSet()
		      ->forAll(c |
		        (c.name = self.name implies
		          c.covered->asSet()
		          ->forAll(cl |
		            self.covered->asSet()
		            ->select(
		              (represents = cl.represents and selector = cl.selector
		              ))
		            ->asSet()
		            ->size() = 1) and
		          self.covered->asSet()
		          ->forAll(cl |
		            c.covered->asSet()
		            ->select(
		              (represents = cl.represents and selector = cl.selector
		              ))
		            ->asSet()
		            ->size() = 1)
		        ))

	inv global:
		enclosingOperand->notEmpty() and
		let operandLifelines : Set(interactions::Lifeline) = enclosingOperand.covered
		in
		  operandLifelines->notEmpty() and
		  operandLifelines->forAll(ol | self.covered->includes(ol))

	context uml::Interactions::Continuation::setting : Boolean

	init:
	true

	context uml::Interactions::DestructionOccurrenceSpecification

	inv no_occurrence_specifications_below:
		let o : interactions::InteractionOperand = enclosingOperand
		in
		  o->notEmpty() and
		  let
		    peerEvents : OrderedSet(interactions::OccurrenceSpecification) = covered.events->select(enclosingOperand = o)
		  in peerEvents->last() = self

	context uml::Interactions::ExecutionSpecification

	inv same_lifeline:
		start.covered = finish.covered

	context uml::Interactions::Gate

	inv actual_gate_matched:
		interactionUse->notEmpty() implies
		interactionUse.refersTo.formalGate->select(matches(self))
		->size() = 1

	inv inside_cf_matched:
		isInsideCF() implies
		combinedFragment.cfragmentGate->select(
		  (isOutsideCF() and matches(self)
		  ))
		->size() = 1

	inv outside_cf_matched:
		isOutsideCF() implies
		if
		  self.combinedFragment.interactionOperator->asOrderedSet()
		  ->first() = UML::Interactions::InteractionOperatorKind::alt
		then
		  self.combinedFragment.operand->forAll(op |
		    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

	inv formal_gate_distinguishable:
		isFormal() implies
		interaction.formalGate->select(getName() = self.getName())
		->size() = 1

	inv actual_gate_distinguishable:
		isActual() implies
		interactionUse.actualGate->select(getName() = self.getName())
		->size() = 1

	inv outside_cf_gate_distinguishable:
		isOutsideCF() implies
		combinedFragment.cfragmentGate->select(getName() = self.getName())
		->size() = 1

	inv inside_cf_gate_distinguishable:
		isInsideCF() implies
		let selfOperand : interactions::InteractionOperand = self.getOperand()
		in
		  combinedFragment.cfragmentGate->select(
		    (isInsideCF() and getName() = self.getName()
		    ))
		  ->select(getOperand() = selfOperand)
		  ->size() = 1

	context Gate::isOutsideCF() : Boolean

	body:
	(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)

	context Gate::isInsideCF() : Boolean

	body:
	(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)

	context Gate::isActual() : Boolean

	body:
	(interactionUse->notEmpty())

	context Gate::isFormal() : Boolean

	body:
	(interaction->notEmpty())

	context Gate::getName() : String

	body:
	(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)

	context Gate::matches(gateToMatch : uml::Interactions::Gate) : Boolean

	body:
	(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)

	context Gate::isDistinguishableFrom(n : uml::CommonStructure::NamedElement, ns : uml::CommonStructure::Namespace) :
	Boolean

	body:
	(true)

	context Gate::getOperand() : uml::Interactions::InteractionOperand

	body:
	(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)

	context uml::Interactions::GeneralOrdering

	inv irreflexive_transitive_closure:
		after->closure(toAfter.after)->excludes(before)

	context uml::Interactions::Interaction

	inv not_contained:
		enclosingInteraction->isEmpty()

	context uml::Interactions::InteractionConstraint

	inv minint_maxint:
		maxint->notEmpty() or
		minint->notEmpty() implies interactionOperand.combinedFragment.interactionOperator = UML::Interactions::InteractionOperatorKind::loop

	inv minint_non_negative:
		minint->notEmpty() implies minint->asSequence()->first().integerValue() >= 0

	inv maxint_positive:
		maxint->notEmpty() implies maxint->asSequence()->first().integerValue() > 0

	inv dynamic_variables:
		null

	inv global_data:
		null

	inv maxint_greater_equal_minint:
		maxint->notEmpty() implies
		minint->notEmpty() and
		maxint->asSequence()
		->first()
		.integerValue() >=
		minint->asSequence()
		->first()
		.integerValue()

	context uml::Interactions::InteractionOperand

	inv guard_contain_references:
		null

	inv guard_directly_prior:
		null

	context uml::Interactions::InteractionUse

	inv gates_match:
		actualGate->notEmpty() implies
		refersTo.formalGate->forAll(fg |
		  self.actualGate->select(matches(fg))
		  ->size() = 1) and
		self.actualGate->forAll(ag |
		  refersTo.formalGate->select(matches(ag))
		  ->size() = 1)

	inv arguments_are_constants:
		null

	inv returnValueRecipient_coverage:
		returnValueRecipient->asSet()
		->notEmpty() implies
		let
		  covCE : Set(structuredClassifiers::ConnectableElement) = covered.represents->asSet()
		in
		  covCE->notEmpty() and
		  let
		    classes : Set(classification::Classifier) = covCE.type.oclIsKindOf(classification::Classifier)
		    .oclAsType(classification::Classifier)
		    ->asSet()
		  in
		    let
		      allProps : Set(classification::Property) = classes.attribute->union(
		        classes.allParents().attribute)
		      ->asSet()
		    in allProps->includes(returnValueRecipient)

	inv arguments_correspond_to_parameters:
		null

	inv returnValue_type_recipient_correspondence:
		returnValue.type->asSequence()
		->notEmpty() implies
		returnValue.type->asSequence()
		->first() =
		returnValueRecipient.type->asSequence()
		->first()

	inv all_lifelines:
		let
		  parentInteraction : Set(interactions::Interaction) = enclosingInteraction->asSet()
		  ->union(
		    enclosingOperand.combinedFragment->closure(enclosingOperand.combinedFragment)
		    ->collect(enclosingInteraction)
		    .oclAsType(interactions::Interaction)
		    ->asSet())
		in
		  parentInteraction->size() = 1 and
		  let refInteraction : interactions::Interaction = refersTo
		  in
		    parentInteraction.covered->forAll(intLifeline |
		      refInteraction.covered->forAll(refLifeline |
		        (refLifeline.represents = intLifeline.represents and
		          (
		            refLifeline.selector.oclIsKindOf(values::LiteralString) implies
		            intLifeline.selector.oclIsKindOf(values::LiteralString) and
		            refLifeline.selector.oclAsType(values::LiteralString).value =
		            intLifeline.selector.oclAsType(values::LiteralString).value
		          ) and
		          (
		            refLifeline.selector.oclIsKindOf(values::LiteralInteger) implies
		            intLifeline.selector.oclIsKindOf(values::LiteralInteger) and
		            refLifeline.selector.oclAsType(values::LiteralInteger).value =
		            intLifeline.selector.oclAsType(values::LiteralInteger).value
		          ) implies
		          self.covered->asSet()
		          ->includes(intLifeline)
		        )))

	context uml::Interactions::Lifeline

	inv selector_specified:
		self.selector->notEmpty() =
		(
		  self.represents.oclIsKindOf(commonStructure::MultiplicityElement) and
		  self.represents.oclAsType(commonStructure::MultiplicityElement)
		  .isMultivalued()
		)

	inv interaction_uses_share_lifeline:
		let intUses : Set(interactions::InteractionUse) = interaction.interactionUse
		in
		  intUses->forAll(iuse |
		    let
		      usingInteraction : Set(interactions::Interaction) = iuse.enclosingInteraction->asSet()
		      ->union(
		        iuse.enclosingOperand.combinedFragment->asSet()
		        ->closure(enclosingOperand.combinedFragment)
		        .enclosingInteraction->asSet())
		    in
		      let
		        peerUses : Set(interactions::InteractionUse) = usingInteraction.fragment->select(
		          oclIsKindOf(interactions::InteractionUse))
		        .oclAsType(interactions::InteractionUse)
		        ->asSet()
		        ->union(
		          usingInteraction.fragment->select(
		            oclIsKindOf(interactions::CombinedFragment))
		          .oclAsType(interactions::CombinedFragment)
		          ->asSet()
		          ->closure(
		            operand.fragment->select(
		              oclIsKindOf(interactions::CombinedFragment))
		            .oclAsType(interactions::CombinedFragment))
		          .operand.fragment->select(
		            oclIsKindOf(interactions::InteractionUse))
		          .oclAsType(interactions::InteractionUse)
		          ->asSet())
		        ->excluding(iuse)
		      in
		        peerUses->forAll(peerUse |
		          peerUse.refersTo.lifeline->forAll(l | l.represents = self.represents and
		            (
		              self.selector.oclIsKindOf(values::LiteralString) implies
		              l.selector.oclIsKindOf(values::LiteralString) and
		              self.selector.oclAsType(values::LiteralString).value =
		              l.selector.oclAsType(values::LiteralString).value
		            ) and
		            (
		              self.selector.oclIsKindOf(values::LiteralInteger) implies
		              l.selector.oclIsKindOf(values::LiteralInteger) and
		              self.selector.oclAsType(values::LiteralInteger).value =
		              l.selector.oclAsType(values::LiteralInteger).value
		            ) implies
		            usingInteraction.lifeline->exists(represents = self.represents and
		              (
		                self.selector.oclIsKindOf(values::LiteralString) implies
		                l.selector.oclIsKindOf(values::LiteralString) and
		                self.selector.oclAsType(values::LiteralString).value =
		                l.selector.oclAsType(values::LiteralString).value
		              ) and
		              (
		                self.selector.oclIsKindOf(values::LiteralInteger) implies
		                l.selector.oclIsKindOf(values::LiteralInteger) and
		                self.selector.oclAsType(values::LiteralInteger).value =
		                l.selector.oclAsType(values::LiteralInteger).value
		              )))))

	inv same_classifier:
		represents.namespace->closure(namespace)
		->includes(interaction._'context')

	inv selector_int_or_string:
		self.selector->notEmpty() implies
		self.selector.oclIsKindOf(values::LiteralInteger) or
		self.selector.oclIsKindOf(values::LiteralString)

	context uml::Interactions::Message

	inv sending_receiving_message_event:
		receiveEvent.oclIsKindOf(interactions::MessageOccurrenceSpecification) implies
		let
		  f : interactions::Lifeline = sendEvent->select(
		    oclIsKindOf(interactions::MessageOccurrenceSpecification))
		  .oclAsType(interactions::MessageOccurrenceSpecification)
		  ->asOrderedSet()
		  ->first().covered
		in f =
		  receiveEvent->select(
		    oclIsKindOf(interactions::MessageOccurrenceSpecification))
		  .oclAsType(interactions::MessageOccurrenceSpecification)
		  ->asOrderedSet()
		  ->first().covered implies
		  f.events->indexOf(
		    sendEvent.oclAsType(interactions::MessageOccurrenceSpecification)
		    ->asOrderedSet()
		    ->first()) <
		  f.events->indexOf(
		    receiveEvent.oclAsType(interactions::MessageOccurrenceSpecification)
		    ->asOrderedSet()
		    ->first())

	inv arguments:
		null

	inv cannot_cross_boundaries:
		sendEvent->notEmpty() and
		receiveEvent->notEmpty() implies
		let
		  sendEnclosingFrag : Set(interactions::InteractionFragment) = sendEvent->asOrderedSet()
		  ->first()
		  .enclosingFragment()
		in
		  let
		    receiveEnclosingFrag : Set(interactions::InteractionFragment) = receiveEvent->asOrderedSet()
		    ->first()
		    .enclosingFragment()
		  in sendEnclosingFrag = receiveEnclosingFrag

	inv signature_is_signal:
		messageSort = UML::Interactions::MessageSort::asynchSignal and
		signature.oclIsKindOf(simpleClassifiers::Signal) implies
		let
		  signalAttributes : OrderedSet(classification::Property) = signature.oclAsType(simpleClassifiers::Signal)
		  .inheritedMember()
		  ->select(n |
		    n.oclIsTypeOf(classification::Property))
		  ->collect(oclAsType(classification::Property))
		  ->asOrderedSet()
		in
		  signalAttributes->size() =
		  self.argument->size() and
		  self.argument->forAll(o |
		    (
		      not (
		        o.oclIsKindOf(values::Expression) and
		        o.oclAsType(values::Expression)
		        .symbol->size() = 0 and
		        o.oclAsType(values::Expression)
		        .operand->isEmpty()
		      ) implies
		      let
		        p : classification::Property = signalAttributes->at(
		          self.argument->indexOf(o))
		      in
		        o.type.oclAsType(classification::Classifier)
		        .conformsTo(
		          p.type.oclAsType(classification::Classifier))
		    ))

	inv occurrence_specifications:
		null

	inv signature_refer_to:
		signature->notEmpty() implies
		(
		  signature.oclIsKindOf(classification::Operation) and
		  (messageSort = UML::Interactions::MessageSort::asynchCall or messageSort = UML::Interactions::MessageSort::synchCall or messageSort = UML::Interactions::MessageSort::reply
		  ) or
		  signature.oclIsKindOf(simpleClassifiers::Signal) and messageSort = UML::Interactions::MessageSort::asynchSignal
		) and name = signature.name

	inv signature_is_operation_request:
		(messageSort = UML::Interactions::MessageSort::asynchCall or messageSort = UML::Interactions::MessageSort::synchCall
		) and
		signature.oclIsKindOf(classification::Operation) implies
		let
		  requestParms : OrderedSet(classification::Parameter) = signature.oclAsType(classification::Operation)
		  .ownedParameter->select(direction = UML::Classification::ParameterDirectionKind::inout or direction = UML::Classification::ParameterDirectionKind::_'in')
		in
		  requestParms->size() =
		  self.argument->size() and
		  self.argument->forAll(o |
		    (
		      not (
		        o.oclIsKindOf(values::Expression) and
		        o.oclAsType(values::Expression)
		        .symbol->size() = 0 and
		        o.oclAsType(values::Expression)
		        .operand->isEmpty()
		      ) implies
		      let
		        p : classification::Parameter = requestParms->at(
		          self.argument->indexOf(o))
		      in
		        o.type.oclAsType(classification::Classifier)
		        .conformsTo(
		          p.type.oclAsType(classification::Classifier))
		    ))

	inv signature_is_operation_reply:
		messageSort = UML::Interactions::MessageSort::reply and
		signature.oclIsKindOf(classification::Operation) implies
		let
		  replyParms : OrderedSet(classification::Parameter) = signature.oclAsType(classification::Operation)
		  .ownedParameter->select(direction = UML::Classification::ParameterDirectionKind::inout or direction = UML::Classification::ParameterDirectionKind::out or direction = UML::Classification::ParameterDirectionKind::return)
		in
		  replyParms->size() =
		  self.argument->size() and
		  self.argument->forAll(o |
		    o.oclIsKindOf(values::Expression) and
		    let
		      e : values::Expression = o.oclAsType(values::Expression)
		    in
		      (
		        e.operand->notEmpty() implies
		        let
		          p : classification::Parameter = replyParms->at(
		            self.argument->indexOf(o))
		        in
		          e.operand->asSequence()
		          ->first()
		          .type.oclAsType(classification::Classifier)
		          .conformsTo(
		            p.type.oclAsType(classification::Classifier))
		      ))

	context Message::messageKind() : uml::Interactions::MessageKind

	body:
	(messageKind)

	context Message::isDistinguishableFrom(n : uml::CommonStructure::NamedElement, ns : uml::CommonStructure::Namespace)
	: Boolean

	body:
	(true)

	context uml::Interactions::Message::messageSort : uml::Interactions::MessageSort

	init:
	UML::Interactions::MessageSort::synchCall

	context MessageEnd::oppositeEnd() : Set(uml::Interactions::MessageEnd)

	pre _'pre':
		message->notEmpty()

	body:
	(message->asSet().messageEnd->asSet()->excluding(self))

	context MessageEnd::isSend() : Boolean

	pre _'pre':
		message->notEmpty()

	body:
	(message.sendEvent->asSet()->includes(self))

	context MessageEnd::isReceive() : Boolean

	pre _'pre':
		message->notEmpty()

	body:
	(message.receiveEvent->asSet()->includes(self))

	context MessageEnd::enclosingFragment() : Set(uml::Interactions::InteractionFragment)

	body:
	(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)

	context uml::Interactions::PartDecomposition

	inv commutativity_of_decomposition:
		null

	inv assume:
		null

	inv parts_of_internal_structures:
		null

endpackage

package uml::InformationFlows

	context uml::InformationFlows::InformationFlow

	inv must_conform:
		null

	inv sources_and_targets_kind:
		self.informationSource->forAll(sis |
		  (
		    oclIsKindOf(useCases::Actor) or
		    oclIsKindOf(deployments::Node) or
		    oclIsKindOf(useCases::UseCase) or
		    oclIsKindOf(deployments::Artifact) or
		    oclIsKindOf(structuredClassifiers::Class) or
		    oclIsKindOf(structuredClassifiers::Component) or
		    oclIsKindOf(structuredClassifiers::Port) or
		    oclIsKindOf(classification::Property) or
		    oclIsKindOf(simpleClassifiers::Interface) or
		    oclIsKindOf(packages::Package) or
		    oclIsKindOf(activities::ActivityNode) or
		    oclIsKindOf(activities::ActivityPartition) or
		    oclIsKindOf(classification::InstanceSpecification) and
		    not sis.oclAsType(classification::InstanceSpecification)
		    .classifier->exists(
		      oclIsKindOf(commonStructure::Relationship))
		  )) and
		self.informationTarget->forAll(sit |
		  (
		    oclIsKindOf(useCases::Actor) or
		    oclIsKindOf(deployments::Node) or
		    oclIsKindOf(useCases::UseCase) or
		    oclIsKindOf(deployments::Artifact) or
		    oclIsKindOf(structuredClassifiers::Class) or
		    oclIsKindOf(structuredClassifiers::Component) or
		    oclIsKindOf(structuredClassifiers::Port) or
		    oclIsKindOf(classification::Property) or
		    oclIsKindOf(simpleClassifiers::Interface) or
		    oclIsKindOf(packages::Package) or
		    oclIsKindOf(activities::ActivityNode) or
		    oclIsKindOf(activities::ActivityPartition) or
		    oclIsKindOf(classification::InstanceSpecification) and
		    not sit.oclAsType(classification::InstanceSpecification)
		    .classifier->exists(
		      oclIsKindOf(commonStructure::Relationship))
		  ))

	inv convey_classifiers:
		self.conveyed->forAll(
		  oclIsKindOf(structuredClassifiers::Class) or
		  oclIsKindOf(simpleClassifiers::Interface) or
		  oclIsKindOf(informationFlows::InformationItem) or
		  oclIsKindOf(simpleClassifiers::Signal) or
		  oclIsKindOf(structuredClassifiers::Component))

	context uml::InformationFlows::InformationItem

	inv sources_and_targets:
		self.represented->select(
		  oclIsKindOf(informationFlows::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(structuredClassifiers::Class) or
		    oclIsKindOf(simpleClassifiers::Interface) or
		    oclIsKindOf(informationFlows::InformationItem) or
		    oclIsKindOf(simpleClassifiers::Signal) or
		    oclIsKindOf(structuredClassifiers::Component)
		  ))

	inv has_no:
		self.generalization->isEmpty() and self.feature->isEmpty()

	inv not_instantiable:
		isAbstract

endpackage

package uml::Deployments

	context uml::Deployments::CommunicationPath

	inv association_ends:
		endType->forAll(
		  oclIsKindOf(deployments::DeploymentTarget))

	context uml::Deployments::DeploymentSpecification

	inv deployment_target:
		deployment->forAll(
		  location.oclIsKindOf(deployments::ExecutionEnvironment))

	inv deployed_elements:
		deployment->forAll(
		  location.deployedElement->forAll(
		    oclIsKindOf(structuredClassifiers::Component)))

	context uml::Deployments::Node

	inv internal_structure:
		part->forAll(oclIsKindOf(deployments::Node))

	context DeploymentTarget::deployedElement() : Set(uml::CommonStructure::PackageableElement)

	body:
	(deployment.deployedArtifact->select(oclIsKindOf(Artifact))->collect(oclAsType(Artifact).manifestation)->collect(utilizedElement)->asSet())

endpackage

package uml::CommonStructure

	context uml::CommonStructure::Constraint

	inv boolean_value:
		null

	inv no_side_effects:
		null

	inv not_apply_to_self:
		not constrainedElement->includes(self)

	context uml::CommonStructure::Element

	inv has_owner:
		mustBeOwned() implies owner->notEmpty()

	inv not_own_self:
		not allOwnedElements()->includes(self)

	context Element::allOwnedElements() : Set(uml::CommonStructure::Element)

	body:
	(ownedElement->union(ownedElement->collect(e | e.allOwnedElements()))->asSet())

	context Element::mustBeOwned() : Boolean

	body:
	(true)

	context uml::CommonStructure::ElementImport

	inv imported_element_is_public:
		importedElement.visibility <> null implies importedElement.visibility = UML::CommonStructure::VisibilityKind::public

	inv visibility_public_or_private:
		visibility = UML::CommonStructure::VisibilityKind::public or visibility = UML::CommonStructure::VisibilityKind::private

	context ElementImport::getName() : String

	body:
	(if alias->notEmpty() then
  alias
else
  importedElement.name
endif)

	context uml::CommonStructure::ElementImport::visibility : uml::CommonStructure::VisibilityKind

	init:
	UML::CommonStructure::VisibilityKind::public

	context uml::CommonStructure::MultiplicityElement

	inv upper_ge_lower:
		upperBound() >= lowerBound()

	inv lower_ge_0:
		lowerBound() >= 0

	inv value_specification_no_side_effects:
		null

	inv value_specification_constant:
		null

	inv lower_is_integer:
		lowerValue <> null implies lowerValue.integerValue() <> null

	inv upper_is_unlimitedNatural:
		upperValue <> null implies upperValue.unlimitedValue() <> null

	context MultiplicityElement::includesMultiplicity(M : uml::CommonStructure::MultiplicityElement) : Boolean

	pre _'pre':
		self.upperBound()
		->notEmpty() and
		self.lowerBound()
		->notEmpty() and
		M.upperBound()
		->notEmpty() and
		M.lowerBound()
		->notEmpty()

	body:
	((self.lowerBound() <= M.lowerBound()) and (self.upperBound() >= M.upperBound()))

	context MultiplicityElement::isMultivalued() : Boolean

	pre _'pre':
		upperBound()->notEmpty()

	body:
	(upperBound() > 1)

	context MultiplicityElement::compatibleWith(other : uml::CommonStructure::MultiplicityElement) : Boolean

	body:
	((other.lowerBound() <= self.lowerBound()) and ((other.upperBound() = *) or (self.upperBound() <= other.upperBound())))

	context MultiplicityElement::is(lowerbound : Integer, upperbound : UnlimitedNatural) : Boolean

	body:
	(lowerbound = self.lowerBound() and upperbound = self.upperBound())

	context MultiplicityElement::lower() : Integer

	body:
	(lowerBound())

	context MultiplicityElement::lowerBound() : Integer

	body:
	(if (lowerValue=null or lowerValue.integerValue()=null) then 1 else lowerValue.integerValue() endif)

	context MultiplicityElement::upper() : UnlimitedNatural

	body:
	(upperBound())

	context MultiplicityElement::upperBound() : UnlimitedNatural

	body:
	(if (upperValue=null or upperValue.unlimitedValue()=null) then 1 else upperValue.unlimitedValue() endif)

	context uml::CommonStructure::MultiplicityElement::isOrdered : Boolean

	init:
	false

	context uml::CommonStructure::MultiplicityElement::isUnique : Boolean

	init:
	true

	context uml::CommonStructure::NamedElement

	inv visibility_needs_ownership:
		namespace = null and owner <> null implies visibility = null

	inv has_qualified_name:
		name <> null and
		allNamespaces()
		->select(ns | ns.name = null)
		->isEmpty() implies qualifiedName =
		allNamespaces()
		->iterate(ns; agg : String = name |
		  ns.name.concat(self.separator())
		  .concat(agg))

	inv has_no_qualified_name:
		name = null or
		allNamespaces()
		->select(ns | ns.name = null)
		->notEmpty() implies qualifiedName = null

	context NamedElement::allNamespaces() : OrderedSet(uml::CommonStructure::Namespace)

	body:
	(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)

	context NamedElement::allOwningPackages() : Set(uml::Packages::Package)

	body:
	(if namespace.oclIsKindOf(Package)
then
  let owningPackage : Package = namespace.oclAsType(Package) in
    owningPackage->union(owningPackage.allOwningPackages())
else
  null
endif)

	context NamedElement::isDistinguishableFrom(n : uml::CommonStructure::NamedElement, ns :
		uml::CommonStructure::Namespace) : Boolean

	body:
	((self.oclIsKindOf(n.oclType()) or n.oclIsKindOf(self.oclType())) implies
    ns.getNamesOfMember(self)->intersection(ns.getNamesOfMember(n))->isEmpty()
)

	context NamedElement::qualifiedName() : String

	body:
	(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)

	context NamedElement::separator() : String

	body:
	('::')

	context NamedElement::clientDependency() : Set(uml::CommonStructure::Dependency)

	body:
	(Dependency.allInstances()->select(d | d.client->includes(self)))

	context uml::CommonStructure::Namespace

	inv members_distinguishable:
		membersAreDistinguishable()

	inv cannot_import_self:
		packageImport.importedPackage.oclAsType(commonStructure::Namespace)
		->excludes(self)

	inv cannot_import_ownedMembers:
		elementImport.importedElement.oclAsType(commonStructure::Element)
		->excludesAll(ownedMember)

	context Namespace::excludeCollisions(imps : Set(uml::CommonStructure::PackageableElement)) :
	Set(uml::CommonStructure::PackageableElement)

	body:
	(imps->reject(imp1  | imps->exists(imp2 | not imp1.isDistinguishableFrom(imp2, self))))

	context Namespace::getNamesOfMember(element : uml::CommonStructure::NamedElement) : Set(String)

	body:
	(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)

	context Namespace::importMembers(imps : Set(uml::CommonStructure::PackageableElement)) :
	Set(uml::CommonStructure::PackageableElement)

	body:
	(self.excludeCollisions(imps)->select(imp | self.ownedMember->forAll(mem | imp.isDistinguishableFrom(mem, self))))

	context Namespace::importedMember() : Set(uml::CommonStructure::PackageableElement)

	body:
	(self.importMembers(elementImport.importedElement->asSet()->union(packageImport.importedPackage->collect(p | p.visibleMembers()))->asSet()))

	context Namespace::membersAreDistinguishable() : Boolean

	body:
	(member->forAll( memb |
   member->excluding(memb)->forAll(other |
       memb.isDistinguishableFrom(other, self))))

	context uml::CommonStructure::PackageableElement

	inv namespace_needs_visibility:
		visibility = null implies namespace = null

	context uml::CommonStructure::PackageableElement::visibility : uml::CommonStructure::VisibilityKind

	init:
	UML::CommonStructure::VisibilityKind::public

	context uml::CommonStructure::PackageImport

	inv public_or_private:
		visibility = UML::CommonStructure::VisibilityKind::public or visibility = UML::CommonStructure::VisibilityKind::private

	context uml::CommonStructure::PackageImport::visibility : uml::CommonStructure::VisibilityKind

	init:
	UML::CommonStructure::VisibilityKind::public

	context uml::CommonStructure::TemplateBinding

	inv parameter_substitution_formal:
		parameterSubstitution->forAll(b |
		  signature.parameter->includes(b.formal))

	inv one_parameter_substitution:
		signature.parameter->forAll(p |
		  parameterSubstitution->select(b | (b.formal = p))
		  ->size() <= 1)

	context uml::CommonStructure::TemplateParameter

	inv must_be_compatible:
		default <> null implies
		default.isCompatibleWith(parameteredElement)

	context uml::CommonStructure::TemplateParameterSubstitution

	inv must_be_compatible:
		actual->forAll(a |
		  a.isCompatibleWith(formal.parameteredElement))

	context uml::CommonStructure::TemplateSignature

	inv own_elements:
		template.ownedElement->includesAll(
		  parameter.parameteredElement->asSet() -
		  parameter.ownedParameteredElement->asSet())

	inv unique_parameters:
		parameter->forAll(p1, p2 | p1 <> p2 and
		  p1.parameteredElement.oclIsKindOf(commonStructure::NamedElement) and
		  p2.parameteredElement.oclIsKindOf(commonStructure::NamedElement) implies
		  p1.parameteredElement.oclAsType(commonStructure::NamedElement).name <>
		  p2.parameteredElement.oclAsType(commonStructure::NamedElement).name)

	context ParameterableElement::isCompatibleWith(p : uml::CommonStructure::ParameterableElement) : Boolean

	body:
	(self.oclIsKindOf(p.oclType()))

	context ParameterableElement::isTemplateParameter() : Boolean

	body:
	(templateParameter->notEmpty())

	context TemplateableElement::isTemplate() : Boolean

	body:
	(ownedTemplateSignature <> null)

	context TemplateableElement::parameterableElements() : Set(uml::CommonStructure::ParameterableElement)

	body:
	(self.allOwnedElements()->select(oclIsKindOf(ParameterableElement)).oclAsType(ParameterableElement)->asSet())

	context Type::conformsTo(other : uml::CommonStructure::Type) : Boolean

	body:
	(false)

endpackage

package uml::CommonBehavior

	context uml::CommonBehavior::Behavior

	inv most_one_behavior:
		specification <> null implies
		_'context'.ownedBehavior->select(specification = self.specification)
		->size() = 1

	inv parameters_match:
		specification <> null implies
		ownedParameter->size() =
		specification.ownedParameter->size()

	inv feature_of_context_classifier:
		_'context'.feature->includes(specification)

	context Behavior::behavioredClassifier(from : uml::CommonStructure::Element) :
	uml::SimpleClassifiers::BehavioredClassifier

	pre spec:
		if
		  from.oclIsKindOf(simpleClassifiers::BehavioredClassifier)
		then
		  from.oclAsType(simpleClassifiers::BehavioredClassifier)
		else
		  if from.owner = null
		  then null
		  else self.behavioredClassifier(from.owner)
		  endif
		endif

	context Behavior::_'context'() : uml::SimpleClassifiers::BehavioredClassifier

	body:
	(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
        )

	context Behavior::inputParameters() : OrderedSet(uml::Classification::Parameter)

	body:
	(ownedParameter->select(direction=ParameterDirectionKind::_'in' or direction=ParameterDirectionKind::inout))

	context Behavior::outputParameters() : OrderedSet(uml::Classification::Parameter)

	body:
	(ownedParameter->select(direction=ParameterDirectionKind::out or direction=ParameterDirectionKind::inout or direction=ParameterDirectionKind::return))

	context uml::CommonBehavior::Behavior::isReentrant : Boolean

	init:
	true

	context uml::CommonBehavior::FunctionBehavior

	inv one_output_parameter:
		self.ownedParameter->select(p |
		  (p.direction = UML::Classification::ParameterDirectionKind::out or p.direction = UML::Classification::ParameterDirectionKind::inout or p.direction = UML::Classification::ParameterDirectionKind::return
		  ))
		->size() >= 1

	inv types_of_parameters:
		ownedParameter->forAll(p | p.type <> null and
		  p.type.oclIsTypeOf(simpleClassifiers::DataType) and
		  hasAllDataTypeAttributes(
		    p.type.oclAsType(simpleClassifiers::DataType)))

	context FunctionBehavior::hasAllDataTypeAttributes(d : uml::SimpleClassifiers::DataType) : Boolean

	body:
	(d.ownedAttribute->forAll(a |
    a.type.oclIsKindOf(DataType) and
      hasAllDataTypeAttributes(a.type.oclAsType(DataType))))

	context uml::CommonBehavior::TimeEvent

	inv when_non_negative:
		when.integerValue() >= 0

	context uml::CommonBehavior::TimeEvent::isRelative : Boolean

	init:
	false

	context uml::CommonBehavior::Trigger

	inv trigger_with_ports:
		port->notEmpty() implies
		event.oclIsKindOf(commonBehavior::MessageEvent)

endpackage

package uml::Classification

	context uml::Classification::BehavioralFeature

	inv abstract_no_method:
		isAbstract implies method->isEmpty()

	context BehavioralFeature::isDistinguishableFrom(n : uml::CommonStructure::NamedElement, ns :
		uml::CommonStructure::Namespace) : Boolean

	body:
	((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 }))
  )

	context BehavioralFeature::inputParameters() : OrderedSet(uml::Classification::Parameter)

	body:
	(ownedParameter->select(direction=ParameterDirectionKind::_'in' or direction=ParameterDirectionKind::inout))

	context BehavioralFeature::outputParameters() : OrderedSet(uml::Classification::Parameter)

	body:
	(ownedParameter->select(direction=ParameterDirectionKind::out or direction=ParameterDirectionKind::inout or direction=ParameterDirectionKind::return))

	context uml::Classification::BehavioralFeature::concurrency : uml::Classification::CallConcurrencyKind

	init:
	UML::Classification::CallConcurrencyKind::sequential

	context uml::Classification::BehavioralFeature::isAbstract : Boolean

	init:
	false

	context uml::Classification::Classifier

	inv specialize_type:
		parents()->forAll(c | self.maySpecializeType(c))

	inv maps_to_generalization_set:
		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)))

	inv non_final_parents:
		parents()->forAll(not isFinalSpecialization)

	inv no_cycles_in_generalization:
		not allParents()->includes(self)

	context Classifier::hasVisibilityOf(n : uml::CommonStructure::NamedElement) : Boolean

	pre _'pre':
		allParents()->including(self)->collect(member)->includes(n)

	body:
	(n.visibility <> VisibilityKind::private)

	context Classifier::inheritableMembers(c : uml::Classification::Classifier) : Set(uml::CommonStructure::NamedElement)

	pre _'pre':
		c.allParents()->includes(self)

	body:
	(member->select(m | c.hasVisibilityOf(m)))

	context Classifier::allFeatures() : Set(uml::Classification::Feature)

	body:
	(member->select(oclIsKindOf(Feature))->collect(oclAsType(Feature))->asSet())

	context Classifier::allParents() : Set(uml::Classification::Classifier)

	body:
	(parents()->union(parents()->collect(allParents())->asSet()))

	context Classifier::conformsTo(other : uml::CommonStructure::Type) : Boolean

	body:
	(if other.oclIsKindOf(Classifier) then
  let otherClassifier : Classifier = other.oclAsType(Classifier) in
    self = otherClassifier or allParents()->includes(otherClassifier)
else
  false
endif)

	context Classifier::general() : Set(uml::Classification::Classifier)

	body:
	(parents())

	context Classifier::inherit(inhs : Set(uml::CommonStructure::NamedElement)) : Set(uml::CommonStructure::NamedElement)

	body:
	(inhs->reject(inh |
  inh.oclIsKindOf(RedefinableElement) and
  ownedMember->select(oclIsKindOf(RedefinableElement))->
    select(redefinedElement->includes(inh.oclAsType(RedefinableElement)))
       ->notEmpty()))

	context Classifier::inheritedMember() : Set(uml::CommonStructure::NamedElement)

	body:
	(inherit(parents()->collect(inheritableMembers(self))->asSet()))

	context Classifier::isTemplate() : Boolean

	body:
	(ownedTemplateSignature <> null or general->exists(g | g.isTemplate()))

	context Classifier::maySpecializeType(c : uml::Classification::Classifier) : Boolean

	body:
	(self.oclIsKindOf(c.oclType()))

	context Classifier::parents() : Set(uml::Classification::Classifier)

	body:
	(generalization.general->asSet())

	context Classifier::directlyRealizedInterfaces() : Set(uml::SimpleClassifiers::Interface)

	body:
	((clientDependency->
  select(oclIsKindOf(Realization) and supplier->forAll(oclIsKindOf(Interface))))->
      collect(supplier.oclAsType(Interface))->asSet())

	context Classifier::directlyUsedInterfaces() : Set(uml::SimpleClassifiers::Interface)

	body:
	((supplierDependency->
  select(oclIsKindOf(Usage) and client->forAll(oclIsKindOf(Interface))))->
    collect(client.oclAsType(Interface))->asSet())

	context Classifier::allRealizedInterfaces() : Set(uml::SimpleClassifiers::Interface)

	body:
	(directlyRealizedInterfaces()->union(self.allParents()->collect(directlyRealizedInterfaces()))->asSet())

	context Classifier::allUsedInterfaces() : Set(uml::SimpleClassifiers::Interface)

	body:
	(directlyUsedInterfaces()->union(self.allParents()->collect(directlyUsedInterfaces()))->asSet())

	context Classifier::isSubstitutableFor(contract : uml::Classification::Classifier) : Boolean

	body:
	(substitution.contract->includes(contract))

	context Classifier::allAttributes() : OrderedSet(uml::Classification::Property)

	body:
	(attribute->asSequence()->union(parents()->asSequence().allAttributes())->select(p | member->includes(p))->asOrderedSet())

	context Classifier::allSlottableFeatures() : Set(uml::Classification::StructuralFeature)

	body:
	(member->select(oclIsKindOf(StructuralFeature))->
  collect(oclAsType(StructuralFeature))->
   union(self.inherit(self.allParents()->collect(p | p.attribute)->asSet())->
     collect(oclAsType(StructuralFeature)))->asSet())

	context uml::Classification::Classifier::isAbstract : Boolean

	init:
	false

	context uml::Classification::Classifier::isFinalSpecialization : Boolean

	init:
	false

	context uml::Classification::ClassifierTemplateParameter

	inv has_constraining_classifier:
		allowSubstitutable implies constrainingClassifier->notEmpty()

	inv parametered_element_no_features:
		parameteredElement.feature->isEmpty() and
		(
		  constrainingClassifier->isEmpty() implies
		  parameteredElement.allParents()
		  ->isEmpty()
		)

	inv matching_abstract:
		not parameteredElement.isAbstract implies
		templateParameterSubstitution.actual->forAll(a |
		  not a.oclAsType(classification::Classifier).isAbstract)

	inv actual_is_classifier:
		templateParameterSubstitution.actual->forAll(a |
		  a.oclIsKindOf(classification::Classifier))

	inv constraining_classifiers_constrain_args:
		templateParameterSubstitution.actual->forAll(a |
		  let
		    arg : classification::Classifier = a.oclAsType(classification::Classifier)
		  in
		    constrainingClassifier->forAll(cc | arg = cc or
		      arg.conformsTo(cc) or allowSubstitutable and
		      arg.isSubstitutableFor(cc)))

	inv constraining_classifiers_constrain_parametered_element:
		constrainingClassifier->forAll(cc | parameteredElement = cc or
		  parameteredElement.conformsTo(cc) or allowSubstitutable and
		  parameteredElement.isSubstitutableFor(cc))

	context uml::Classification::ClassifierTemplateParameter::allowSubstitutable : Boolean

	init:
	true

	context uml::Classification::GeneralizationSet

	inv generalization_same_classifier:
		generalization->collect(general)->asSet()->size() <= 1

	inv maps_to_generalization_set:
		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))

	context uml::Classification::GeneralizationSet::isCovering : Boolean

	init:
	false

	context uml::Classification::GeneralizationSet::isDisjoint : Boolean

	init:
	false

	context uml::Classification::InstanceSpecification

	inv deployment_artifact:
		deploymentForArtifact->notEmpty() implies
		classifier->exists(oclIsKindOf(deployments::Artifact))

	inv structural_feature:
		classifier->forAll(c |
		  c.allSlottableFeatures()
		  ->forAll(f |
		    slot->select(s | (s.definingFeature = f))
		    ->size() <= 1))

	inv defining_feature:
		slot->forAll(s |
		  classifier->exists(c |
		    c.allSlottableFeatures()
		    ->includes(s.definingFeature)))

	inv deployment_target:
		deployment->notEmpty() implies
		classifier->exists(node |
		  node.oclIsKindOf(deployments::Node) and
		  deployments::Node.allInstances()
		  ->exists(n | n.part->exists(p | p.type = node)))

	context uml::Classification::Operation

	inv at_most_one_return:
		self.ownedParameter->select(
		  (direction = UML::Classification::ParameterDirectionKind::return
		  ))
		->size() <= 1

	inv only_body_for_query:
		bodyCondition <> null implies isQuery

	context Operation::isConsistentWith(redefiningElement : uml::Classification::RedefinableElement) : Boolean

	pre _'pre':
		redefiningElement.isRedefinitionContextValid(self)

	body:
	(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))
		))

	context Operation::isOrdered() : Boolean

	body:
	(if returnResult()->notEmpty() then returnResult()-> exists(isOrdered) else false endif)

	context Operation::isUnique() : Boolean

	body:
	(if returnResult()->notEmpty() then returnResult()->exists(isUnique) else true endif)

	context Operation::lower() : Integer

	body:
	(if returnResult()->notEmpty() then returnResult()->any(true).lower else null endif)

	context Operation::returnResult() : Set(uml::Classification::Parameter)

	body:
	(ownedParameter->select (direction = ParameterDirectionKind::return))

	context Operation::type() : uml::CommonStructure::Type

	body:
	(if returnResult()->notEmpty() then returnResult()->any(true).type else null endif)

	context Operation::upper() : UnlimitedNatural

	body:
	(if returnResult()->notEmpty() then returnResult()->any(true).upper else null endif)

	context uml::Classification::Operation::isQuery : Boolean

	init:
	false

	context uml::Classification::OperationTemplateParameter

	inv match_default_signature:
		default->notEmpty() implies
		default.oclIsKindOf(classification::Operation) and
		let
		  defaultOp : classification::Operation = default.oclAsType(classification::Operation)
		in
		  defaultOp.ownedParameter->size() =
		  parameteredElement.ownedParameter->size() and
		  Sequence{1..defaultOp.ownedParameter->size()
		  }
		  ->forAll(ix |
		    let p1 : classification::Parameter = defaultOp.ownedParameter->at(ix)
		    in
		      let
		        p2 : classification::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)

	context uml::Classification::Parameter

	inv in_and_out:
		(effect = UML::Classification::ParameterEffectKind::delete implies direction = UML::Classification::ParameterDirectionKind::_'in' or direction = UML::Classification::ParameterDirectionKind::inout
		) and
		(effect = UML::Classification::ParameterEffectKind::create implies direction = UML::Classification::ParameterDirectionKind::out or direction = UML::Classification::ParameterDirectionKind::inout or direction = UML::Classification::ParameterDirectionKind::return
		)

	inv not_exception:
		isException implies direction <> UML::Classification::ParameterDirectionKind::_'in' and direction <> UML::Classification::ParameterDirectionKind::inout

	inv connector_end:
		end->notEmpty() implies collaboration->notEmpty()

	inv reentrant_behaviors:
		isStream and behavior <> null implies not behavior.isReentrant

	inv stream_and_exception:
		not (isException and isStream)

	inv object_effect:
		type.oclIsKindOf(simpleClassifiers::DataType) implies effect = null

	context Parameter::default() : String

	body:
	(if self.type = String then defaultValue.stringValue() else null endif)

	context uml::Classification::Parameter::direction : uml::Classification::ParameterDirectionKind

	init:
	UML::Classification::ParameterDirectionKind::_'in'

	context uml::Classification::Parameter::isException : Boolean

	init:
	false

	context uml::Classification::Parameter::isStream : Boolean

	init:
	false

	context uml::Classification::ParameterSet

	inv same_parameterized_entity:
		parameter->forAll(p1, p2 | self.owner = p1.owner and self.owner = p2.owner and p1.direction = p2.direction)

	inv input:
		(
		  parameter->exists(direction = UML::Classification::ParameterDirectionKind::_'in') implies
		  behavioralFeature.ownedParameter->select(p | p.direction = UML::Classification::ParameterDirectionKind::_'in' and
		    p.parameterSet->isEmpty())
		  ->forAll(isStream)
		) and
		(
		  parameter->exists(direction = UML::Classification::ParameterDirectionKind::out) implies
		  behavioralFeature.ownedParameter->select(p | p.direction = UML::Classification::ParameterDirectionKind::out and
		    p.parameterSet->isEmpty())
		  ->forAll(isStream)
		)

	inv two_parameter_sets:
		parameter->forAll(
		  parameterSet->forAll(s1, s2 |
		    s1->size() =
		    s2->size() implies
		    s1.parameter->exists(p | not s2.parameter->includes(p))))

	context uml::Classification::Property

	inv subsetting_context_conforms:
		subsettedProperty->notEmpty() implies
		subsettingContext()
		->notEmpty() and
		subsettingContext()
		->forAll(sc |
		  subsettedProperty->forAll(sp |
		    sp.subsettingContext()
		    ->exists(c | sc.conformsTo(c))))

	inv derived_union_is_read_only:
		isDerivedUnion implies isReadOnly

	inv multiplicity_of_composite:
		isComposite and association <> null implies opposite.upperBound() <= 1

	inv redefined_property_inherited:
		redefinedProperty->notEmpty() implies
		redefinitionContext->notEmpty() and
		redefinedProperty->forAll(rp |
		  redefinitionContext->collect(fc | fc.allParents())
		  ->asSet()
		  ->collect(c | c.allFeatures())
		  ->asSet()
		  ->includes(rp))

	inv subsetting_rules:
		subsettedProperty->forAll(sp |
		  self.type.conformsTo(sp.type) and
		  (
		    self.upperBound()
		    ->notEmpty() and
		    sp.upperBound()
		    ->notEmpty() implies
		    self.upperBound() <=
		    sp.upperBound()
		  ))

	inv binding_to_attribute:
		self.isAttribute() and
		templateParameterSubstitution->notEmpty() implies
		templateParameterSubstitution->forAll(ts |
		  ts.formal.oclIsKindOf(classification::Property) and
		  ts.formal.oclAsType(classification::Property)
		  .isAttribute())

	inv derived_union_is_derived:
		isDerivedUnion implies isDerived

	inv deployment_target:
		deployment->notEmpty() implies
		owner.oclIsKindOf(deployments::Node) and
		deployments::Node.allInstances()
		->exists(n | n.part->exists(p | p = self))

	inv subsetted_property_names:
		subsettedProperty->forAll(sp | sp.name <> name)

	inv type_of_opposite_end:
		opposite->notEmpty() and owningAssociation->isEmpty() implies classifier = opposite.type

	inv qualified_is_association_end:
		qualifier->notEmpty() implies association->notEmpty()

	context Property::isConsistentWith(redefiningElement : uml::Classification::RedefinableElement) : Boolean

	pre _'pre':
		redefiningElement.isRedefinitionContextValid(self)

	body:
	(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)))

	context Property::isAttribute() : Boolean

	body:
	(not classifier->isEmpty())

	context Property::isCompatibleWith(p : uml::CommonStructure::ParameterableElement) : Boolean

	body:
	(self.oclIsKindOf(p.oclType()) and (p.oclIsKindOf(TypedElement) implies
self.type.conformsTo(p.oclAsType(TypedElement).type)))

	context Property::isComposite() : Boolean

	body:
	(aggregation = AggregationKind::composite)

	context Property::isNavigable() : Boolean

	body:
	(not classifier->isEmpty() or association.navigableOwnedEnd->includes(self))

	context Property::opposite() : uml::Classification::Property

	body:
	(if association <> null and association.memberEnd->size() = 2
then
    association.memberEnd->any(e | e <> self)
else
    null
endif)

	context Property::subsettingContext() : Set(uml::CommonStructure::Type)

	body:
	(if association <> null
then association.memberEnd->excluding(self)->collect(type)->asSet()
else 
  if classifier<>null
  then classifier->asSet()
  else Set{} 
  endif
endif)

	context uml::Classification::Property::aggregation : uml::Classification::AggregationKind

	init:
	UML::Classification::AggregationKind::none

	context uml::Classification::Property::isComposite : Boolean

	init:
	false

	context uml::Classification::Property::isDerived : Boolean

	init:
	false

	context uml::Classification::Property::isDerivedUnion : Boolean

	init:
	false

	context uml::Classification::Property::isID : Boolean

	init:
	false

	context uml::Classification::RedefinableElement

	inv redefinition_consistent:
		redefinedElement->forAll(re | re.isConsistentWith(self))

	inv non_leaf_redefinition:
		redefinedElement->forAll(re | not re.isLeaf)

	inv redefinition_context_valid:
		redefinedElement->forAll(re | self.isRedefinitionContextValid(re))

	context RedefinableElement::isConsistentWith(redefiningElement : uml::Classification::RedefinableElement) : Boolean

	pre _'pre':
		redefiningElement.isRedefinitionContextValid(self)

	body:
	(false)

	context RedefinableElement::isRedefinitionContextValid(redefinedElement : uml::Classification::RedefinableElement) :
	Boolean

	body:
	(redefinitionContext->exists(c | c.allParents()->includesAll(redefinedElement.redefinitionContext)))

	context uml::Classification::RedefinableElement::isLeaf : Boolean

	init:
	false

	context uml::Classification::RedefinableTemplateSignature

	inv redefines_parents:
		classifier.allParents()
		->forAll(c |
		  c.ownedTemplateSignature->notEmpty() implies
		  self->closure(extendedSignature)
		  ->includes(c.ownedTemplateSignature))

	context RedefinableTemplateSignature::isConsistentWith(redefiningElement : uml::Classification::RedefinableElement) :
	Boolean

	pre _'pre':
		redefiningElement.isRedefinitionContextValid(self)

	body:
	(redefiningElement.oclIsKindOf(RedefinableTemplateSignature))

	context RedefinableTemplateSignature::inheritedParameter() : Set(uml::CommonStructure::TemplateParameter)

	body:
	(if extendedSignature->isEmpty() then Set{} else extendedSignature.parameter->asSet() endif)

	context uml::Classification::Feature::isStatic : Boolean

	init:
	false

	context uml::Classification::Generalization::isSubstitutable : Boolean

	init:
	true

	context uml::Classification::StructuralFeature::isReadOnly : Boolean

	init:
	false

endpackage

package uml::Actions

	context uml::Actions::ValueSpecificationAction

	inv multiplicity:
		result.is(1, 1)

	inv compatible_type:
		value.type.conformsTo(result.type)

	context uml::Actions::VariableAction

	inv scope_of_variable:
		variable.isAccessibleBy(self)

	context uml::Actions::WriteLinkAction

	inv allow_access:
		endData.end->exists(end | end.type = _'context' or end.visibility = UML::CommonStructure::VisibilityKind::public or end.visibility = UML::CommonStructure::VisibilityKind::protected and
		  endData.end->exists(other | other <> end and
		    _'context'.conformsTo(
		      other.type.oclAsType(classification::Classifier))))

	context uml::Actions::WriteStructuralFeatureAction

	inv multiplicity_of_result:
		result <> null implies result.is(1, 1)

	inv type_of_value:
		value <> null implies
		value.type.conformsTo(structuralFeature.type)

	inv multiplicity_of_value:
		value <> null implies value.is(1, 1)

	inv type_of_result:
		result <> null implies result.type = object.type

	context uml::Actions::WriteVariableAction

	inv value_type:
		value <> null implies value.type.conformsTo(variable.type)

	inv multiplicity:
		value <> null implies value.is(1, 1)

	context uml::Actions::AcceptCallAction

	inv result_pins:
		let
		  parameter : OrderedSet(classification::Parameter) = trigger.event->asSequence()
		  ->first()
		  .oclAsType(commonBehavior::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)))

	inv trigger_call_event:
		trigger->size() = 1 and
		trigger->asSequence()
		->first()
		.event.oclIsKindOf(commonBehavior::CallEvent)

	inv unmarshall:
		isUnmarshall = true

	context uml::Actions::AcceptEventAction

	inv one_output_pin:
		not isUnmarshall and
		trigger->exists(
		  (
		    event.oclIsKindOf(commonBehavior::SignalEvent) or
		    event.oclIsKindOf(commonBehavior::TimeEvent)
		  )) implies
		output->size() = 1 and
		output->first()
		.is(1, 1)

	inv no_input_pins:
		input->size() = 0

	inv no_output_pins:
		self.oclIsTypeOf(actions::AcceptEventAction) and
		trigger->forAll(
		  (
		    event.oclIsKindOf(commonBehavior::ChangeEvent) or
		    event.oclIsKindOf(commonBehavior::CallEvent)
		  )) implies
		output->size() = 0

	inv unmarshall_signal_events:
		isUnmarshall and
		self.oclIsTypeOf(actions::AcceptEventAction) implies
		trigger->size() = 1 and
		trigger->asSequence()
		->first()
		.event.oclIsKindOf(commonBehavior::SignalEvent) and
		let
		  attribute : OrderedSet(classification::Property) = trigger->asSequence()
		  ->first()
		  .event.oclAsType(commonBehavior::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)))

	inv conforming_type:
		not isUnmarshall implies
		result->isEmpty() or
		let type : commonStructure::Type = result->first().type
		in type = null or
		  trigger->forAll(
		    event.oclIsKindOf(commonBehavior::SignalEvent)) and
		  trigger.event.oclAsType(commonBehavior::SignalEvent)
		  .signal->forAll(s | s.conformsTo(type))

	context uml::Actions::AcceptEventAction::isUnmarshall : Boolean

	init:
	false

	context uml::Actions::ActionInputPin

	inv input_pin:
		fromAction.input->forAll(
		  oclIsKindOf(actions::ActionInputPin))

	inv one_output_pin:
		fromAction.output->size() = 1

	inv no_control_or_object_flow:
		fromAction.incoming->union(outgoing)
		->isEmpty() and
		fromAction.input.incoming->isEmpty() and
		fromAction.output.outgoing->isEmpty()

	context uml::Actions::AddStructuralFeatureValueAction

	inv required_value:
		value <> null

	inv insertAt_pin:
		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

	context uml::Actions::AddStructuralFeatureValueAction::isReplaceAll : Boolean

	init:
	false

	context uml::Actions::AddVariableValueAction

	inv required_value:
		value <> null

	inv insertAt_pin:
		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

	context uml::Actions::AddVariableValueAction::isReplaceAll : Boolean

	init:
	false

	context uml::Actions::BroadcastSignalAction

	inv number_of_arguments:
		argument->size() = signal.allAttributes()->size()

	inv type_ordering_multiplicity:
		let attribute : OrderedSet(classification::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)))

	inv no_onport:
		onPort = null

	context uml::Actions::CallAction

	inv argument_pins:
		let parameter : OrderedSet(classification::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)))

	inv result_pins:
		let
		  parameter : OrderedSet(classification::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)))

	inv synchronous_call:
		result->notEmpty() implies isSynchronous

	context uml::Actions::CallAction::isSynchronous : Boolean

	init:
	true

	context uml::Actions::CallBehaviorAction

	inv no_onport:
		onPort = null

	context CallBehaviorAction::outputParameters() : OrderedSet(uml::Classification::Parameter)

	body:
	(behavior.outputParameters())

	context CallBehaviorAction::inputParameters() : OrderedSet(uml::Classification::Parameter)

	body:
	(behavior.inputParameters())

	context uml::Actions::CallOperationAction

	inv type_target_pin:
		if onPort = null
		then
		  target.type.oclAsType(classification::Classifier)
		  .allFeatures()
		  ->includes(operation)
		else
		  target.type.oclAsType(classification::Classifier)
		  .allFeatures()
		  ->includes(onPort) and
		  onPort.provided->union(onPort.required)
		  .allFeatures()
		  ->includes(operation)
		endif

	context CallOperationAction::outputParameters() : OrderedSet(uml::Classification::Parameter)

	body:
	(operation.outputParameters())

	context CallOperationAction::inputParameters() : OrderedSet(uml::Classification::Parameter)

	body:
	(operation.inputParameters())

	context uml::Actions::Clause

	inv body_output_pins:
		_'body'.oclAsType(actions::Action)
		.allActions()
		.output->includesAll(bodyOutput)

	inv decider_output:
		test.oclAsType(actions::Action)
		.allActions()
		.output->includes(decider) and decider.type = Boolean and
		decider.is(1, 1)

	inv test_and_body:
		test->intersection(_'body')->isEmpty()

	context uml::Actions::ClearAssociationAction

	inv multiplicity:
		object.is(1, 1)

	inv same_type:
		association.memberEnd->exists(self.object.type.conformsTo(type))

	context uml::Actions::ClearStructuralFeatureAction

	inv type_of_result:
		result <> null implies result.type = object.type

	inv multiplicity_of_result:
		result <> null implies result.is(1, 1)

	context uml::Actions::ConditionalNode

	inv result_no_incoming:
		result.incoming->isEmpty()

	inv no_input_pins:
		input->isEmpty()

	inv one_clause_with_executable_node:
		node->select(oclIsKindOf(activities::ExecutableNode))
		.oclAsType(activities::ExecutableNode)
		->forAll(n |
		  self.clause->select(test->union(_'body')->includes(n))
		  ->size() = 1)

	inv matching_output_pins:
		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))))

	inv executable_nodes:
		clause.test->union(clause._'body') =
		node->select(oclIsKindOf(activities::ExecutableNode))
		.oclAsType(activities::ExecutableNode)

	inv clause_no_predecessor:
		clause->closure(predecessorClause)
		->intersection(clause)
		->isEmpty()

	context ConditionalNode::allActions() : Set(uml::Actions::Action)

	body:
	(self->asSet())

	context uml::Actions::ConditionalNode::isAssured : Boolean

	init:
	false

	context uml::Actions::ConditionalNode::isDeterminate : Boolean

	init:
	false

	context uml::Actions::CreateLinkAction

	inv association_not_abstract:
		not self.association().isAbstract

	context uml::Actions::CreateLinkObjectAction

	inv multiplicity:
		result.is(1, 1)

	inv type_of_result:
		result.type = association()

	inv association_class:
		self.association()
		.oclIsKindOf(structuredClassifiers::AssociationClass)

	context uml::Actions::CreateObjectAction

	inv classifier_not_abstract:
		not classifier.isAbstract

	inv multiplicity:
		result.is(1, 1)

	inv classifier_not_association_class:
		not classifier.oclIsKindOf(structuredClassifiers::AssociationClass)

	inv same_type:
		result.type = classifier

	context uml::Actions::DestroyObjectAction

	inv multiplicity:
		target.is(1, 1)

	inv no_type:
		target.type = null

	context uml::Actions::DestroyObjectAction::isDestroyLinks : Boolean

	init:
	false

	context uml::Actions::DestroyObjectAction::isDestroyOwnedObjects : Boolean

	init:
	false

	context uml::Actions::ExpansionNode

	inv region_as_input_or_output:
		regionAsInput->notEmpty() xor regionAsOutput->notEmpty()

	context uml::Actions::InputPin

	inv outgoing_edges_structured_only:
		outgoing->notEmpty() implies action <> null and
		action.oclIsKindOf(actions::StructuredActivityNode) and
		action.oclAsType(actions::StructuredActivityNode)
		.allOwnedNodes()
		->includesAll(outgoing.target)

	context uml::Actions::LinkAction

	inv same_pins:
		inputValue->asBag() = endData.allPins()

	inv same_association:
		endData.end = self.association().memberEnd->asBag()

	inv not_static:
		endData->forAll(not end.isStatic)

	context LinkAction::association() : uml::StructuredClassifiers::Association

	body:
	(endData->asSequence()->first().end.association)

	context uml::Actions::LinkEndCreationData

	inv insertAt_pin:
		if not end.isOrdered
		then insertAt = null
		else not isReplaceAll = false implies insertAt <> null and
		  insertAt->forAll(type = UnlimitedNatural and is(1, 1))
		endif

	context LinkEndCreationData::allPins() : Bag(uml::Actions::InputPin)

	body:
	(self.LinkEndData::allPins()->including(insertAt))

	context uml::Actions::LinkEndCreationData::isReplaceAll : Boolean

	init:
	false

	context uml::Actions::LinkEndData

	inv same_type:
		value <> null implies value.type.conformsTo(end.type)

	inv multiplicity:
		value <> null implies value.is(1, 1)

	inv end_object_input_pin:
		value->excludesAll(qualifier.value)

	inv property_is_association_end:
		end.association <> null

	inv qualifiers:
		end.qualifier->includesAll(qualifier.qualifier)

	context LinkEndData::allPins() : Bag(uml::Actions::InputPin)

	body:
	(value->asBag()->union(qualifier.value))

	context uml::Actions::LinkEndDestructionData

	inv destroyAt_pin:
		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

	context LinkEndDestructionData::allPins() : Bag(uml::Actions::InputPin)

	body:
	(self.LinkEndData::allPins()->including(destroyAt))

	context uml::Actions::LinkEndDestructionData::isDestroyDuplicates : Boolean

	init:
	false

	context uml::Actions::LoopNode

	inv result_no_incoming:
		result.incoming->isEmpty()

	inv input_edges:
		loopVariableInput.outgoing->isEmpty()

	inv executable_nodes:
		setupPart->union(test)
		->union(bodyPart) =
		node->select(oclIsKindOf(activities::ExecutableNode))
		.oclAsType(activities::ExecutableNode)
		->asSet()

	inv body_output_pins:
		bodyPart.oclAsType(actions::Action)
		.allActions()
		.output->includesAll(bodyOutput)

	inv setup_test_and_body:
		setupPart->intersection(test)
		->isEmpty() and
		setupPart->intersection(bodyPart)
		->isEmpty() and
		test->intersection(bodyPart)
		->isEmpty()

	inv matching_output_pins:
		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)))

	inv matching_loop_variables:
		loopVariableInput->size() =
		loopVariable->size() and loopVariableInput.type = loopVariable.type and loopVariableInput.isUnique = loopVariable.isUnique and loopVariableInput.lower = loopVariable.lower and loopVariableInput.upper = loopVariable.upper

	inv matching_result_pins:
		result->size() =
		loopVariable->size() and result.type = loopVariable.type and result.isUnique = loopVariable.isUnique and result.lower = loopVariable.lower and result.upper = loopVariable.upper

	inv loop_variable_outgoing:
		allOwnedNodes()
		->includesAll(loopVariable.outgoing.target)

	context LoopNode::allActions() : Set(uml::Actions::Action)

	body:
	(self->asSet())

	context LoopNode::sourceNodes() : Set(uml::Activities::ActivityNode)

	body:
	(self.StructuredActivityNode::sourceNodes()->union(loopVariable))

	context uml::Actions::LoopNode::isTestedFirst : Boolean

	init:
	false

	context uml::Actions::OpaqueAction

	inv language_body_size:
		language->notEmpty() implies _'body'->size() = language->size()

	context uml::Actions::OutputPin

	inv incoming_edges_structured_only:
		incoming->notEmpty() implies action <> null and
		action.oclIsKindOf(actions::StructuredActivityNode) and
		action.oclAsType(actions::StructuredActivityNode)
		.allOwnedNodes()
		->includesAll(incoming.source)

	context uml::Actions::Pin

	inv control_pins:
		isControl implies isControlType

	inv not_unique:
		not isUnique

	context uml::Actions::Pin::isControl : Boolean

	init:
	false

	context uml::Actions::QualifierValue

	inv multiplicity_of_qualifier:
		value.is(1, 1)

	inv type_of_qualifier:
		value.type.conformsTo(qualifier.type)

	inv qualifier_attribute:
		linkEndData.end.qualifier->includes(qualifier)

	context uml::Actions::ReadExtentAction

	inv type_is_classifier:
		result.type = classifier

	inv multiplicity_of_result:
		result.is(0, *)

	context uml::Actions::ReadIsClassifiedObjectAction

	inv no_type:
		object.type = null

	inv multiplicity_of_output:
		result.is(1, 1)

	inv boolean_result:
		result.type = Boolean

	inv multiplicity_of_input:
		object.is(1, 1)

	context uml::Actions::ReadIsClassifiedObjectAction::isDirect : Boolean

	init:
	false

	context uml::Actions::ReadLinkAction

	inv type_and_ordering:
		self.openEnd()
		->forAll(type = result.type and isOrdered = result.isOrdered)

	inv compatible_multiplicity:
		self.openEnd()->first().compatibleWith(result)

	inv visibility:
		let openEnd : classification::Property = self.openEnd()->first()
		in openEnd.visibility = UML::CommonStructure::VisibilityKind::public or
		  endData->exists(oed | oed.end <> openEnd and
		    (_'context' = oed.end.type or openEnd.visibility = UML::CommonStructure::VisibilityKind::protected and
		      _'context'.conformsTo(
		        oed.end.type.oclAsType(classification::Classifier))
		    ))

	inv one_open_end:
		self.openEnd()->size() = 1

	inv navigable_open_end:
		self.openEnd()->first().isNavigable()

	context ReadLinkAction::openEnd() : OrderedSet(uml::Classification::Property)

	body:
	(endData->select(value=null).end->asOrderedSet())

	context uml::Actions::ReadLinkObjectEndAction

	inv property:
		end.association <> null

	inv multiplicity_of_object:
		object.is(1, 1)

	inv ends_of_association:
		end.association.memberEnd->forAll(e | not e.isStatic)

	inv type_of_result:
		result.type = end.type

	inv multiplicity_of_result:
		result.is(1, 1)

	inv type_of_object:
		object.type = end.association

	inv association_of_association:
		end.association.oclIsKindOf(structuredClassifiers::AssociationClass)

	context uml::Actions::ReadLinkObjectEndQualifierAction

	inv multiplicity_of_object:
		object.is(1, 1)

	inv type_of_object:
		object.type = qualifier.associationEnd.association

	inv multiplicity_of_qualifier:
		qualifier.is(1, 1)

	inv ends_of_association:
		qualifier.associationEnd.association.memberEnd->forAll(e | not e.isStatic)

	inv multiplicity_of_result:
		result.is(1, 1)

	inv same_type:
		result.type = qualifier.type

	inv association_of_association:
		qualifier.associationEnd.association.oclIsKindOf(structuredClassifiers::AssociationClass)

	inv qualifier_attribute:
		qualifier.associationEnd <> null

	context uml::Actions::ReadSelfAction

	inv contained:
		_'context' <> null

	inv multiplicity:
		result.is(1, 1)

	inv not_static:
		let behavior : commonBehavior::Behavior = self.containingBehavior()
		in behavior.specification <> null implies not behavior.specification.isStatic

	inv type:
		result.type = _'context'

	context uml::Actions::ReadStructuralFeatureAction

	inv multiplicity:
		structuralFeature.compatibleWith(result)

	inv type_and_ordering:
		result.type = structuralFeature.type and result.isOrdered = structuralFeature.isOrdered

	context uml::Actions::ReadVariableAction

	inv type_and_ordering:
		result.type = variable.type and result.isOrdered = variable.isOrdered

	inv compatible_multiplicity:
		variable.compatibleWith(result)

	context uml::Actions::ReclassifyObjectAction

	inv input_pin:
		object.type = null

	inv classifier_not_abstract:
		not newClassifier->exists(isAbstract)

	inv multiplicity:
		object.is(1, 1)

	context uml::Actions::ReclassifyObjectAction::isReplaceAll : Boolean

	init:
	false

	context uml::Actions::ReduceAction

	inv reducer_inputs_output:
		let inputs : OrderedSet(classification::Parameter) = reducer.inputParameters()
		in
		  let
		    outputs : OrderedSet(classification::Parameter) = reducer.outputParameters()
		  in
		    inputs->size() = 2 and
		    outputs->size() = 1 and
		    inputs.type->forAll(t |
		      (
		        outputs.type->forAll(conformsTo(t)) and
		        collection.upperBound() > 1 implies
		        collection.type.conformsTo(t)
		      ))

	inv input_type_is_collection:
		null

	inv output_types_are_compatible:
		reducer.outputParameters()
		.type->forAll(conformsTo(result.type))

	context uml::Actions::ReduceAction::isOrdered : Boolean

	init:
	false

	context uml::Actions::RemoveStructuralFeatureValueAction

	inv removeAt_and_value:
		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

	context uml::Actions::RemoveStructuralFeatureValueAction::isRemoveDuplicates : Boolean

	init:
	false

	context uml::Actions::RemoveVariableValueAction

	inv removeAt_and_value:
		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

	context uml::Actions::RemoveVariableValueAction::isRemoveDuplicates : Boolean

	init:
	false

	context uml::Actions::ReplyAction

	inv pins_match_parameter:
		let
		  parameter : OrderedSet(classification::Parameter) = replyToCall.event.oclAsType(commonBehavior::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)))

	inv event_on_reply_to_call_trigger:
		replyToCall.event.oclIsKindOf(commonBehavior::CallEvent)

	context uml::Actions::SendObjectAction

	inv type_target_pin:
		onPort <> null implies
		target.type.oclAsType(classification::Classifier)
		.allFeatures()
		->includes(onPort)

	context uml::Actions::SendSignalAction

	inv type_ordering_multiplicity:
		let attribute : OrderedSet(classification::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)))

	inv number_order:
		argument->size() = signal.allAttributes()->size()

	inv type_target_pin:
		not onPort->isEmpty() implies
		target.type.oclAsType(classification::Classifier)
		.allFeatures()
		->includes(onPort)

	context uml::Actions::StartClassifierBehaviorAction

	inv multiplicity:
		object.is(1, 1)

	inv type_has_classifier:
		object.type->notEmpty() implies
		object.type.oclIsKindOf(simpleClassifiers::BehavioredClassifier) and
		object.type.oclAsType(simpleClassifiers::BehavioredClassifier).classifierBehavior <> null

	context uml::Actions::StartObjectBehaviorAction

	inv multiplicity_of_object:
		object.is(1, 1)

	inv type_of_object:
		self.behavior() <> null

	inv no_onport:
		onPort->isEmpty()

	context StartObjectBehaviorAction::outputParameters() : OrderedSet(uml::Classification::Parameter)

	body:
	(self.behavior().outputParameters())

	context StartObjectBehaviorAction::inputParameters() : OrderedSet(uml::Classification::Parameter)

	body:
	(self.behavior().inputParameters())

	context StartObjectBehaviorAction::behavior() : uml::CommonBehavior::Behavior

	body:
	(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)

	context uml::Actions::StructuralFeatureAction

	inv multiplicity:
		object.is(1, 1)

	inv object_type:
		object.type.oclAsType(classification::Classifier)
		.allFeatures()
		->includes(structuralFeature) or
		object.type.conformsTo(
		  structuralFeature.oclAsType(classification::Property).opposite.type)

	inv visibility:
		structuralFeature.visibility = UML::CommonStructure::VisibilityKind::public or
		_'context'.allFeatures()
		->includes(structuralFeature) or structuralFeature.visibility = UML::CommonStructure::VisibilityKind::protected and
		_'context'.conformsTo(
		  structuralFeature.oclAsType(classification::Property)
		  .opposite.type.oclAsType(classification::Classifier))

	inv not_static:
		not structuralFeature.isStatic

	inv one_featuring_classifier:
		structuralFeature.featuringClassifier->size() = 1

	context uml::Actions::StructuredActivityNode

	inv output_pin_edges:
		output.outgoing.target->excludesAll(allOwnedNodes() - input)

	inv edges:
		edge =
		self.sourceNodes()
		.outgoing->intersection(self.allOwnedNodes().incoming)
		->union(
		  self.targetNodes()
		  .incoming->intersection(self.allOwnedNodes().outgoing))
		->asSet()

	inv input_pin_edges:
		input.incoming.source->excludesAll(allOwnedNodes() - output)

	context StructuredActivityNode::allActions() : Set(uml::Actions::Action)

	body:
	(node->select(oclIsKindOf(Action)).oclAsType(Action).allActions()->including(self)->asSet())

	context StructuredActivityNode::allOwnedNodes() : Set(uml::Activities::ActivityNode)

	body:
	(self.Action::allOwnedNodes()->union(node)->union(node->select(oclIsKindOf(Action)).oclAsType(Action).allOwnedNodes())->asSet())

	context StructuredActivityNode::sourceNodes() : Set(uml::Activities::ActivityNode)

	body:
	(node->union(input.oclAsType(ActivityNode)->asSet())->
  union(node->select(oclIsKindOf(Action)).oclAsType(Action).output)->asSet())

	context StructuredActivityNode::targetNodes() : Set(uml::Activities::ActivityNode)

	body:
	(node->union(output.oclAsType(ActivityNode)->asSet())->
  union(node->select(oclIsKindOf(Action)).oclAsType(Action).input)->asSet())

	context StructuredActivityNode::containingActivity() : uml::Activities::Activity

	body:
	(self.Action::containingActivity())

	context uml::Actions::StructuredActivityNode::mustIsolate : Boolean

	init:
	false

	context uml::Actions::TestIdentityAction

	inv multiplicity:
		first.is(1, 1) and second.is(1, 1)

	inv no_type:
		first.type = null and second.type = null

	inv result_is_boolean:
		result.type = Boolean

	context uml::Actions::UnmarshallAction

	inv structural_feature:
		unmarshallType.allAttributes()->size() >= 1

	inv number_of_result:
		unmarshallType.allAttributes()->size() = result->size()

	inv type_ordering_and_multiplicity:
		let
		  attribute : OrderedSet(classification::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)))

	inv multiplicity_of_object:
		object.is(1, 1)

	inv object_type:
		object.type.conformsTo(unmarshallType)

	context uml::Actions::ValuePin

	inv no_incoming_edges:
		incoming->isEmpty()

	inv compatible_type:
		value.type.conformsTo(type)

	context Action::_'context'() : uml::Classification::Classifier

	body:
	(let behavior: Behavior = self.containingBehavior() in
if behavior=null then null
else if behavior._'context' = null then behavior
else behavior._'context'
endif
endif)

	context Action::allActions() : Set(uml::Actions::Action)

	body:
	(self->asSet())

	context Action::allOwnedNodes() : Set(uml::Activities::ActivityNode)

	body:
	(input.oclAsType(Pin)->asSet()->union(output->asSet()))

	context Action::containingBehavior() : uml::CommonBehavior::Behavior

	body:
	(if inStructuredNode<>null then inStructuredNode.containingBehavior() 
else if activity<>null then activity
else interaction 
endif
endif
)

	context uml::Actions::Action::isLocallyReentrant : Boolean

	init:
	false

	context uml::Actions::ExpansionRegion::mode : uml::Actions::ExpansionKind

	init:
	UML::Actions::ExpansionKind::iterative

endpackage