+ aligned constraints, #208

  -- Distinguishable qualified names

  inv DistinquishableName ('All qualified names of instances of \'NamedElement\'s shall be distinguishable within a TDL model.' + self.toString()):

  inv DistinguishableName ('All qualified names of instances of \'NamedElement\'s shall be distinguishable within a TDL model.' + self.toString()):

        NamedElement.allInstances()->one(e | e.qualifiedName = self.qualifiedName)

context Extension

  -- Inherit from element of the same meta-class

  inv Extension ('The element containing an \'Extension\' and the element in the \'extending\' property shall have the same meta-class.' + self.toString()):

  inv Extension ('The element containing an \'Extension\' and the element in the \'extending\' property shall have the same metaclass.' + self.toString()):

        self.container().oclType() = self.extending.oclType()

  -- No recursive extension

  inv NoRecursiveExtension ('The element containing an \'Extension\' shall not extend itself directly or indirectly.' + self.toString()):

        Set{self}->closure(e | e.transitiveExtending())->collect(e|e.extending)->excludes(self.container())

context Constraint

  -- Effectively static quantifiers 

  inv StaticQuantifiers ('All \'DataUse\'s specified as \'quantifier\'s shall be effectively static.' + self.toString()):

  -- All parameters shall be mapped

  inv ParameterMappings ('If the \'mappableDataElement\' refers to a \'StructuredDataType\', an \'Action\' or a \'Function\' definition, all the \'Parameters\' contained in the \'mappableDataElement\' shall be mapped.' + self.toString()):

        (self.mappableDataElement.oclIsKindOf(SimpleDataType) or self.mappableDataElement.oclIsKindOf(CollectionDataType) or self.mappableDataElement.oclIsKindOf(DataInstance)

        (self.mappableDataElement.oclIsKindOf(SimpleDataType) or 

           self.mappableDataElement.oclIsKindOf(CollectionDataType) or 

           self.mappableDataElement.oclIsKindOf(DataInstance)

      or (self.mappableDataElement.oclIsTypeOf(StructuredDataType)

      and self.mappableDataElement.oclAsType(StructuredDataType).member->forAll(p | 

               self.parameterMapping->exists(m | m.parameter = p)))

        not self.dataType.oclIsKindOf(EnumDataType) or self.oclContainer() = self.dataType

  -- Type of the 'value' shall conform to the type of the 'SimpleDataInstance'

  inv MatchingValueDataType ('The \'DataType\' of the \'DataUse\' of \'value\' shall conform to the \'DataType\' of the \'SimpleDataInstance\'.' + self.toString()):

        self.value.resolveDataType().conformsTo(self.dataType)

  -- No 'OmitValue' for 'SimpleDataInstance'

  inv OmitValueSimpleDataInstance ('A \'value\' of a \'SimpleDataInstance\' shall have a \'DataUse\' specification assigned to it that is different from \'OmitValue\' and \'AnyValueOrOmit\'.' + self.toString()):

        not (self.value.oclIsTypeOf(OmitValue) or self.value.oclIsTypeOf(AnyValueOrOmit))

  -- Static data use in 'value' 

  inv StaticDataInValue ('The \'value\' shall be effectively static. ' + self.toString()):

        self.value.isEffectivelyStatic()

  -- [Figure 6.3: Structured data type and instance]

  -- [Figure 6.5: Procedure and procedure parameter]

context FormalParameter

  -- Type of the 'value' shall conform to the type of the 'FormalParameter'

  inv MatchingValueDataTypeFormalParameter ('The \'DataType\' of the \'DataUse\' of \'value\' shall conform to the \'DataType\' of the \'SimpleDataInstance\'.' + self.toString()):

        self.value.resolveDataType().conformsTo(self.dataType)

  -- Static data use in 'FormalParameter' 'value' 

  inv StaticDataInFormalParameterValue ('The \'value\' shall be effectively static. ' + self.toString()):

        self.value.isEffectivelyStatic()

context EnumDataType

  -- No extensions for EnumDataType

  inv  EnumDataTypeExtensions ('The \'extension\' property of an \'EnumDataType\' shall be empty.' + self.toString()):

	        			and dataType.oclAsType(StructuredDataType).allMembers()->includes(mr.member))

	    			or (dataType.oclIsKindOf(CollectionDataType)

	    				and dataType.oclAsType(CollectionDataType).itemType.oclIsKindOf(StructuredDataType)

	    				and dataType.oclAsType(CollectionDataType).itemType.oclAsType(StructuredDataType).allMembers()->includes(mr.member)))))

          				and dataType.oclAsType(CollectionDataType).itemType

                                      .oclAsType(StructuredDataType).allMembers()->includes(mr.member)))))

			or (self.reduction->at(self.reduction->indexOf(mr)-1).member.oclIsUndefined())

        )  

  -- Either member or collection index is required

  inv MemberOrReduction ('Either the member or collectionIndex shall be specified. ' + self.toString()):

  inv MemberOrIndex ('Either the member or collectionIndex shall be specified. ' + self.toString()):

        not self.member.oclIsUndefined() or not self.collectionIndex.oclIsUndefined()

context VariableUse

  -- Local variables of tester components only

  inv VariableUseComponentRole ('All variables used in a \'DataUse\' specification via a \'VariableUse\' shall be local to the same \'componentInstance\' and the \'componentInstance\' shall be in the role \'Tester\'.' + self.toString()):

        self.effectiveComponent().oclIsUndefined() or self.effectiveComponent().type.allVariables()->includes(self.variable)  

        self.effectiveComponent().oclIsUndefined() or 

          self.effectiveComponent().type.allVariables()->includes(self.variable)  

          and self.effectiveComponent().role = ComponentInstanceRole::Tester

--applicable on 'LocalExpression', 'VariableUse', 'TimeOperation', and 'ActionBehaviour', 

--returns the 'ComponentInstance' specified for the element or the 'defaultTester' from the nearest containing 'Block' that has the 'defaultTester' specified.

  -- Known 'componentInstance' for 'Variable'

  inv VariableUseComponent ('The effective component shall be known.' + self.toString()):

        not self.effectiveComponent().oclIsUndefined()

  -- Integer type for integer value

  inv LiteralValueIntType ('If \'intValue\' is specified then the \'dataType\' is either unspecified or the specified \'DataType\' is instanceof of \'Time\' or conforms to predefined type \'Integer\'.' + self.toString()):

  inv LiteralValueIntType ('If \'intValue\' is specified then the \'dataType\' is either unspecified or the specified \'DataType\' is instance of \'Time\' or conforms to predefined type \'Integer\'.' + self.toString()):

        not self.intValue.oclIsUndefined() 

          implies (self.dataType.oclIsUndefined() or self.dataType.oclIsKindOf(Time) or self.dataType.conformsTo('Integer'))

context TimerOperation

  -- Timer operations on tester components only

  inv TimerOperationComponentRole ('A \'TimerOperation\' shall be performed only on a \'ComponentInstance\' in the role \'Tester\'.' + self.toString()):

        self.effectiveComponent().oclIsUndefined() or self.effectiveComponent().role = ComponentInstanceRole::Tester

        self.effectiveComponent().oclIsUndefined() or 

          self.effectiveComponent().role = ComponentInstanceRole::Tester

  -- Known 'componentInstance' for 'Timer'

  inv TimerComponent ('The effective component shall be known.' + self.toString()):

        not self.effectiveComponent().oclIsUndefined()

  -- Named 'GateReference's 

  inv NamedGateReferences ('The names of \'GateReference\'s that in turn refer to identical pairs of \'GateInstance\'/\'ComponentInstance\' within a \'TestConfiguration\' shall be identical and the names of \'GateReference\'s that in turn refer to different pairs of \'GateInstance\'/\'ComponentInstance\' shall be different.' + self.toString()):

		self.name.oclIsUndefined() or

		    self.container().container().oclAsType(TestConfiguration).connection.endPoint->forAll(ep | ep.name.oclIsUndefined() or (

		    self.container().container().oclAsType(TestConfiguration).connection.endPoint->forAll(ep | 

		        ep.name.oclIsUndefined() or (

		            (self.name = ep.name implies (self.component = ep.component and self.gate = ep.gate)) and 

		        (self.name <> ep.name implies (self.component <> ep.component or self.gate <> ep.gate)))

		    )

		            (self.name <> ep.name implies (self.component <> ep.component or self.gate <> ep.gate))))

		    ))->isEmpty()))

context Block

  -- Guard shall evaluate to Boolean

  inv GuardType ('The type of \'guard\' shall be \'Boolean\'.' + self.toString()):

        self.guard ->forAll(g | g.expression.resolveDataType().conformsTo('Boolean'))

  -- No directly contained 'ExceptionalBehaviour's and 'PeriodicBehaviour's.

  -- No directly contained 'ExceptionalBehaviour's and 'PeriodicBehaviour's

  inv AllowedBehaviourTypes ('A \'Block\' shall not contain \'ExceptionalBehaviour\'s and \'PeriodicBehaviour\'s.' + self.toString()):

    self.behaviour->forAll(b |

         not b.oclIsTypeOf(ExceptionalBehaviour) and not b.oclIsTypeOf(PeriodicBehaviour))

  -- Guard for each participating tester in locally ordered test descriptions

  inv GuardsForParticipatingComponents ('If the \'Block\' is contained in a locally ordered \'TestDescription\' then exactly one guard shall be specified for every participating \'ComponentInstance\' in the associated \'TestConfiguration\' that has the role \'Tester\' or there shall be no guards at all. ' + self.toString()):

  inv GuardsForParticipatingComponents ('If the \'Block\' is contained in a locally ordered \'TestDescription\' then a single effectively static guard shall be specified or exactly one guard shall be specified for every participating \'ComponentInstance\' in the associated \'TestConfiguration\' that has the role \'Tester\' or there shall be no guards at all. ' + self.toString()):

        self.guard->size() = 0

          or (self.guard->size() = 1 and self.guard->forAll(g | g.expression.isEffectivelyStatic()))

          or self.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT)

              ->forAll(c | self.guard->one(ex | ex.effectiveComponent() = c))

          or not self.getParentTestDescription().isLocallyOrdered

        self.getParentTestDescription().isLocallyOrdered or self.guard->size() <= 1

  -- Default tester role 

  inv DefaultTesterRole ('If the \'defaultTester\' is specified, the corresponding \'ComponentInstance\' shall have the role \'Tester\'. ' + self.toString()):

        self.defaultTester.oclIsUndefined() or self.defaultTester.role = ComponentInstanceRole::Tester

context LocalExpression

  -- Local expressions in locally ordered test descriptions have 'ComponentInstance' specified

  inv LocalExpressionComponent ('If the \'LocalExpression\' is contained in a locally ordered \'TestDescription\' then the componentInstance shall be specified. ' + self.toString()):

  inv LocalExpressionComponent ('If the \'LocalExpression\' is contained in a locally ordered \'TestDescription\' then the expression shall be effectively static or the componentInstance shall be specified. ' + self.toString()):

        self.getParentTestDescription().isLocallyOrdered 

          implies not self.effectiveComponent().oclIsUndefined()

          implies (expression.isEffectivelyStatic() or not self.effectiveComponent().oclIsUndefined())

  -- Only local variables and time labels in case of locally ordered test description

  -- Iteration count in locally ordered test descriptions

  inv  IterationCountsForParticipatingComponents ('If the \'BoundedLoopBehaviour\' is contained in a locally ordered \'TestDescription\' then a numIteration shall be specified for every participating \'ComponentInstance\' that has the role \'Tester\'.' + self.toString()):

        self.block.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT)

              ->forAll(c | self.numIteration->exists(ex | ex.effectiveComponent() = c))

  inv  IterationCountsForParticipatingComponents ('If the \'BoundedLoopBehaviour\' is contained in a locally ordered \'TestDescription\' then a single effectively static numIteration shall be specified or exactly one numIteration shall be specified for every participating \'ComponentInstance\' that has the role \'Tester\'.' + self.toString()):

        (self.numIteration->size() = 1 and self.numIteration->forAll(i | i.expression.isEffectivelyStatic()))

          or self.block.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT)

              ->forAll(c | self.numIteration->one(ex | ex.effectiveComponent() = c))

          or not self.getParentTestDescription().isLocallyOrdered

  inv AlternativeBlocksComponent ('If the containing \'TestDescription\' is locally ordered then all \'Block\'s shall start with a tester-input event of the same \'ComponentInstance\'. ' + self.toString()):

        let initial = self.block.behaviour->first() in

          Set{}

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction)

                  .target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).effectiveComponent())

          -> includingAll(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).effectiveComponent())

          ->size() = 1 or not self.getParentTestDescription().isLocallyOrdered

  inv AlternativeBehaviourParticipation ('If the \'AlternativeBehaviour\' is contained in a locally ordered \'TestDescription\' then no other tester \'ComponentInstance\' shall participate in any block than the target of the first tester-input event and \'ComponentInstance\'s participating in blocks of contained \'OptionalBehaviour\'s. ' + self.toString()):

        let initial = self.block.behaviour->first(),

          targetComponent = Set{}

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction)

                  .target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).effectiveComponent())

          -> includingAll(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).effectiveComponent()),

          nonOptionalBlocks = self.block->closure(

  inv OptionalAlternativeBehaviour ('A block of an \'AlternativeBehaviour\' if the containing \'TestDescription\' is locally ordered, shall only contain \'OptionalBehaviour\'(s) whose source \'ComponentInstance\' is the same as the target of the first tester-input event of that \'Block\'. ' + self.toString()):

        let initial = self.block.behaviour->first(),

          targetComponent = Set{}

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction)

                 .target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).effectiveComponent())

          -> includingAll(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).effectiveComponent())

          in

  inv ExceptionalGuardedandTargetComponent ('If the containing \'TestDescription\' is locally ordered and guardedComponent is specified then the \'Block\'s shall start with tester-input event of the same \'ComponentInstance\' as specified in guardedComponent. ' + self.toString()):

        let initial = self.block.behaviour->first(),

          targetComponent = Set{}

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction)

                  .target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).effectiveComponent())

          -> includingAll(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).effectiveComponent())

          in

  inv ExceptionalBehaviourParticipation ('If the \'ExceptionalBehaviour\' is contained in a locally ordered \'TestDescription\' then no other tester \'ComponentInstance\' shall participate in any block than the target of the first tester-input event and \'ComponentInstance\'s participating in blocks of contained \'OptionalBehaviour\'s . ' + self.toString()):

        let initial = self.block.behaviour->first(),

          targetComponent = Set{}

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction)

                  .target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).effectiveComponent())

          -> includingAll(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).effectiveComponent()),

          ->includingAll(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance),

          nonOptionalBlocks = self.block->closure(

              b | b.behaviour->reject(oclIsKindOf(OptionalBehaviour))

                  ->select(oclIsKindOf(SingleCombinedBehaviour)).oclAsType(SingleCombinedBehaviour).block

  inv OptionalExceptionalBehaviour ('A block of an \'ExceptionalBehaviour\' if the containing \'TestDescription\' is locally ordered, shall only contain \'OptionalBehaviour\'(s) whose source \'ComponentInstance\' is the same as the target of the first tester-input event of that \'Block\'. ' + self.toString()):

        let initial = self.block.behaviour->first(),

          targetComponent = Set{}

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction)

                  .target.targetGate.component)

          ->includingAll(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).effectiveComponent())

          -> includingAll(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).effectiveComponent())

          in

          self.block.behaviour->select(oclIsKindOf(OptionalBehaviour)).oclAsType(OptionalBehaviour)->forAll(op | op.block.behaviour->asSequence()

          self.block.behaviour->select(oclIsKindOf(OptionalBehaviour))

              .oclAsType(OptionalBehaviour)->forAll(op | op.block.behaviour->asSequence()

              ->first().oclAsType(Interaction).sourceGate.component->forAll(c | targetComponent->includes(c)))

          or not self.getParentTestDescription().isLocallyOrdered

  -- Period for each tester in locally ordered test descriptions

  inv PeriodForParticipatingComponents ('If the \'PeriodicBehaviour\' is contained in a locally ordered \'TestDescription\' then a period shall be specified for every \'ComponentInstance\' that has the role \'Tester\' and for which there is a behaviour in the contained \'Block\'. ' + self.toString()):

        self.block.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT)

              ->forAll(c | self.period->exists(ex | ex.effectiveComponent() = c))

  inv PeriodForParticipatingComponents ('If the \'PeriodicBehaviour\' is contained in a locally ordered \'TestDescription\' then a single effectively static period shall be specified or exactly one period shall be specified for every \'ComponentInstance\' that has the role \'Tester\' and for which there is a behaviour in the contained \'Block\'. ' + self.toString()):

        (self.period->size() = 1 and self.period->forAll(p | p.expression.isEffectivelyStatic()))

          or self.block.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT)

              ->forAll(c | self.period->one(ex | ex.effectiveComponent() = c))

          or not self.getParentTestDescription().isLocallyOrdered

  -- Parameter of associated procedure signature

  inv AssignedProcedureParameter ('If the \'parameter\' is specified then it shall be contained in the \'ProcedureSignature\' that is referred in the \'signature\' ot the \'ProcedureCall\' containing this \'ValueAssignment\'.' + self.toString()):

  inv AssignedProcedureParameter ('If the \'parameter\' is specified then it shall be contained in the \'ProcedureSignature\' that is referred in the \'signature\' of the \'ProcedureCall\' containing this \'ValueAssignment\'.' + self.toString()):

        self.parameter.oclIsUndefined()

      or (self.container().container().oclIsKindOf(ProcedureCall) and

      self.container().container().oclAsType(ProcedureCall).signature.parameter->includes(self.parameter))