tdl-constraints.ocl

import 'http://www.etsi.org/spec/TDL/1.4.1'

package tdl

context NamedElement
  -- Mandatory name
  inv MandatoryName ('A \'NamedElement\' shall have the \'name\' property set and the \'name\' shall be not an empty String.' + self.toString()):
        not self.name.oclIsUndefined() and self.name.size() > 0
  

  -- Distinguishable qualified names
  inv DistinquishableName ('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)
  

  -- [NOTE:	It is up to the concrete syntax definition and tooling to resolve any name clashes between instances of the same meta-class in the qualified name.]


context Package
  -- No cyclic imports
  inv CyclicImports ('A \'Package\' shall not import itself directly or indirectly.' + self.toString()):
        self.import->asOrderedSet()->closure(i | i.importedPackage.import)->forAll(i | 
              i.importedPackage <> self)
  



context ElementImport
  -- Consistency of imported elements
  inv ConsistentImports ('All imported \'PackageableElement\'s referenced by an \'ElementImport\' shall be directly owned by the imported \'Package\'.' + self.toString()):
        self.importedElement->forAll(e | self.importedPackage.packagedElement->includes(e))
  

  -- [Figure 5.2: Miscellaneous elements]


context Comment
  -- No nested comments
  inv CommentNestedComments ('A \'Comment\' shall not contain \'Comment\'s.' + self.toString()):
        self.comment->isEmpty()
  

  -- No annotations to comments
  inv CommentNestedAnnotations ('A \'Comment\' shall not contain \'Annotation\'s.' + self.toString()):
        self.annotation->isEmpty()
  



context Annotation
  -- No nested annotations
  inv AnnotationNestedAnnotations ('An \'Annotation\' shall not contain \'Annotation\'s' + self.toString()):
        self.annotation->isEmpty()
  

  -- No comments to annotations
  inv AnnotationNestedComments ('An \'Annotation\' shall not contain \'Comment\'s.' + self.toString()):
        self.comment->isEmpty()
  



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()):
        self.container().oclType()  = self.extending.oclType()
  



context Constraint
  -- Effectively static quantifiers 
  inv StaticQuantifiers ('All \'DataUse\'s specified as \'quantifier\'s shall be effectively static.' + self.toString()):
        self.quantifier->forAll(q | q.isEffectivelyStatic())
  

  -- Empty arguments for quantifiers 
  inv NoArgumentQuantifiers ('The \'argument\' sets for all \'DataUse\'s specified as \'quantifier\'s shall be empty.' + self.toString()):
        self.quantifier->forAll(q | q.argument->isEmpty())
  

  -- Constraint applicability for 'union' and 'uniontype' 
  inv ConstraintApplicabilityUnionUniontype ('The predefined \'ConstraintType\'s \'union\' and \'uniontype\' shall be applied to \'StructuredDataType\'s only. ' + self.toString()):
        (self.type.name = 'union' or self.type.name = 'uniontype') 
          implies self.container().oclIsTypeOf(StructuredDataType)
  

  -- Constraint applicability for 'range' and 'format'
  inv ConstraintApplicabilityRangeFormat ('The predefined \'ConstraintType\'s \'range\' and \'format\' shall be applied to \'SimpleDataType\'s and \'Member\'s with a \'SimpleDataType\' \'dataType\' only. ' + self.toString()):
        (self.type.name = 'range' or self.type.name = 'format') 
          implies (self.container().oclIsTypeOf(SimpleDataType)
             or (self.container().oclIsTypeOf(Member) 
                 and self.container().oclAsType(Member).dataType.oclIsTypeOf(SimpleDataType)))
  

  -- Constraint applicability for 'length', 'minLength', and 'maxLength' 
  inv ConstraintApplicabilityLength ('The predefined \'ConstraintType\'s \'length\', \'minLength\', and \'maxLength\' shall be applied to \'CollectionDataType\'s, \'SimpleDataType\'s and \'Member\'s with a \'SimpleDataType\' or a \'CollectionDataType\' \'dataType\' only. ' + self.toString()):
        (self.type.name = 'length' or self.type.name = 'minLength' or self.type.name = 'maxLength')
          implies (self.container().oclIsTypeOf(SimpleDataType)
              or self.container().oclIsTypeOf(CollectionDataType)
              or (self.container().oclIsTypeOf(Member) 
                 and self.container().oclAsType(Member).dataType.oclIsTypeOf(SimpleDataType))
                 and self.container().oclAsType(Member).dataType.oclIsTypeOf(CollectionDataType))
  

  -- Quantifiers for 'length', 'minLength', and 'maxLength'
  inv ConstraintQuantifierLength ('The predefined \'ConstraintType\'s \'length\', \'minLength\', and \'maxLength\' shall be used with exactly one \'quantifier\' resolved to an instance conforming to the predefined \'Integer\' \'DataType\'. ' + self.toString()):
        (self.type.name = 'length' or self.type.name = 'minLength' or self.type.name = 'maxLength') 
          implies (self.quantifier->size() = 1 
              and self.quantifier->forAll(q | q.resolveDataType().conformsTo('Integer')))
  

  -- Quantifiers for 'range' 
  inv ConstraintQuantifierRange ('The predefined \'ConstraintType\' \'range\' shall be used with exactly two \'quantifier\'s resolved to instance conforming to the predefined \'Integer\' \'DataType\'. ' + self.toString()):
        (self.type.name = 'length') 
          implies (self.quantifier->size() = 2 
              and self.quantifier->forAll(q | q.resolveDataType().conformsTo('Integer')))
  



context DataElementMapping
  -- Restricted use of 'ParameterMapping'
  inv ParameterMappingType ('A set of \'ParameterMapping\'s may only be provided if \'mappableDataElement\' refers to a \'StructuredDataType\', an \'Action\' or a \'Function\' definition and the \'mappableDataElement\' contains the mapped \'Parameters\'.' + self.toString()):
        self.parameterMapping->size() = 0
      or (self.mappableDataElement.oclIsTypeOf(StructuredDataType) 
      and self.parameterMapping->forAll(p | 
               self.mappableDataElement.oclAsType(StructuredDataType).allMembers()->includes(p.parameter))) 
      or (self.mappableDataElement.oclIsKindOf(Action) 
      and self.parameterMapping->forAll(p | 
               self.mappableDataElement.oclAsType(Action).formalParameter->includes(p.parameter)))
  

  -- 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.oclIsTypeOf(SimpleDataType)
      or (self.mappableDataElement.oclIsTypeOf(StructuredDataType)
      and self.mappableDataElement.oclAsType(StructuredDataType).member->forAll(p | 
               self.parameterMapping->exists(m | m.parameter = p)))
      or (self.mappableDataElement.oclIsKindOf(Action) 
      and self.mappableDataElement.oclAsType(Action).formalParameter->forAll(p | 
               self.parameterMapping->exists(m | m.parameter = p)))
      and self.parameterMapping->forAll(p | 
               self.mappableDataElement.oclAsType(Action).formalParameter->includes(p.parameter)))
  



context SimpleDataInstance
  -- SimpleDataInstance shall refer to SimpleDataType
  inv SimpleDataInstanceType ('The inherited reference \'dataType\' from \'DataInstance\' shall refer to instances of \'SimpleDataType\' solely.' + self.toString()):
        self.dataType.oclIsKindOf(SimpleDataType)
  

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


context StructuredDataType
  -- Different member names in a structured data type
  inv DistinguishableMemberNames ('All \'Member\' names of a \'StructuredDataType\' (including the names of inherited \'Members\') shall be distinguishable.' + self.toString()):
        self.allMembers()->isUnique(e | e.name)
  



context StructuredDataInstance
  -- StructuredDataInstance shall refer to StructuredDataType
  inv StructuredDataInstance ('The inherited reference \'dataType\' from \'DataInstance\' shall refer to instances of \'StructuredDataType\' solely.' + self.toString()):
        self.dataType.oclIsTypeOf(StructuredDataType)
  

  -- 'Member' of the 'StructuredDataType'
  inv ExistingMemberOfDataType ('The referenced \'Member\' shall be contained in or inherited by the \'StructuredDataType\' that the \'StructuredDataInstance\', which contains this \'MemberAssignment\', refers to.' + self.toString()):
        self.memberAssignment->forAll(a | self.dataType.oclAsType(StructuredDataType).allMembers()->includes(a.member))
  

  -- Unique assignments for each 'Member' of the 'StructuredDataType'
  inv UniqueMemberAssignments ('There shall be at most one \'memberAssignment\' for each \'Member\' of the \'StructuredDataType\' that the \'StructuredDataInstance\', which contains this \'MemberAssignment\', refers to.' + self.toString()):
        self.memberAssignment->isUnique(m | m.member)
  

  -- 'union' constraint on the type of the 'StructuredDataInstance'
  inv StructuredDataInstanceUnionConstraint ('If the \'dataType\' of the \'StructuredDataInstance\' has the predefined constraint \'union\' then the \'memberAssignment\' shall not contain more than one \'MemberAssignment\'.' + self.toString()):
        not self.dataType.allConstraints()->exists(c | c.type.name = 'union')
          or self.memberAssignment->size() <= 1
  

  -- 'uniontype' constraint on the type of the 'StructuredDataInstance'
  inv StructuredDataInstanceUniontypeConstraint ('If the \'dataType\' of \'StructuredDataInstance\' has the predefined constraint \'uniontype\' then there shall only be \'MemberAssignment\' for the \'Member\'s of the \'dataType\' itself or of at most one of the \'StructuredDataType\'s which the \'dataType\' is extending.' + self.toString()):
        not self.dataType.allConstraints()->exists(c | c.type.name = 'uniontype')
          or self.memberAssignment->forAll(m | self.dataType.oclAsType(StructuredDataType).member->includes(m)
              or self.dataType.oclAsType(StructuredDataType).extension->one(e | 
                  e.extending.oclAsType(StructuredDataType).allMembers()->includes(m)))
  



context MemberAssignment
  -- Type of a 'memberSpec' shall conform to the type of the 'member'
  inv MatchingMemberDataType ('The \'DataType\' of the \'DataUse\' of \'memberSpec\' shall conform to the \'DataType\' of the \'Member\' of the \'MemberAssignment\'.' + self.toString()):
        self.memberSpec.resolveDataType().conformsTo(self.member.dataType)
  

  -- Restricted use of 'OmitValue' for optional 'Member's only
  inv OmitValueUse ('A non-optional \'Member\' shall have a \'DataUse\' specification assigned to it that is different from \'OmitValue\' and \'AnyValueOrOmit\'.' + self.toString()):
        (self.memberSpec.oclIsTypeOf(OmitValue) or self.memberSpec.oclIsTypeOf(AnyValueOrOmit))
          implies self.member.isOptional = true
  

  -- Static data use in 'memberSpec' 
  inv StaticDataInMemberSpec ('The \'memberSpec\' and all of its \'ParameterBinding\'s shall be effectively static. ' + self.toString()):
        self.memberSpec.isEffectivelyStatic()
  

  -- [Figure 6.4: Collection data]


context CollectionDataType
  -- No multidimensional collections
  inv NoMultidimensionalCollections ('The \'itemType\' shall not be an instance of \'CollectionDataType\'. ' + self.toString()):
        not self.itemType.oclIsKindOf(CollectionDataType)
  



context CollectionDataInstance
  -- CollectionDataInstance shall refer to CollectionDataType
  inv  CollectionDataInstanceType ('The inherited reference \'dataType\' from \'DataInstance\' shall refer to instances of \'CollectionDataType\' solely.' + self.toString()):
        self.dataType.oclIsKindOf(CollectionDataType)
  

  -- Type of items in the 'CollectionDataInstance'
  inv CollectionDataInstanceItemType ('The items in \'CollectionDataInstance\' shall conform to the \'itemType\' of the \'CollectionDataType\' that is defined as the \'dataType\' of this \'CollectionDataInstance\'. ' + self.toString()):
        self.item->forAll(i | 
              i.resolveDataType().conformsTo(self.dataType.oclAsType(CollectionDataType).itemType))
  

  -- Static data use in 'item' 
  inv StaticDataInItem ('The DataUse\'s in \'item\' and all of the respective \'ParameterBinding\'s shall be effectively static. ' + self.toString()):
        self.item->forAll(i | i.isEffectivelyStatic())
  

  -- Length constraint of the 'CollectionDataInstance'
  inv CollectionDataInstanceLengthConstraint ('If the \'dataType\' \'CollectionType\' contains the predefined constraint \'length\' then the length of this \'CollectionDataInstance\' shall be equal to the \'quantifier\' of that \'Constraint\'.' + self.toString()):
        true --This constraint cannot be expressed formally.
  

  -- [Figure 6.5: Procedure and procedure parameter]


context EnumDataType
  -- SimpleDataInstance container in EnumDataType
  inv  EnumDataInstanceContainment ('A \'SimpleDataInstance\' whose \'dataType\' property refers to an \'EnumDataType\' shall be contained in that \'EnumDataType\'.' + self.toString()):
        OclInvalid
  

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



context DataUse
  -- Occurrence of 'argument' and 'reduction'
  inv ArgumentReductionLists ('Only in case of a \'FunctionCall\' both the \'argument\' list and the \'reduction\' list may be provided, otherwise either the \'argument\' list, the \'reduction\' list, or none of them shall be provided.' + self.toString()):
        self.argument->isEmpty() or self.reduction->isEmpty() or self.oclIsTypeOf(FunctionCall)
  

  -- Structured data types in 'reduction' set
  inv ReductionMembers ('The \'Member\' referenced by the \'MemberReference\' at index i of a \'reduction\' shall be contained in or inherited by the \'StructuredDataType\' of the \'Member\' referenced by the \'MemberReference\' at index (i - 1) of that \'reduction\'.' + self.toString()):
        not self.resolveDataType().oclIsKindOf(StructuredDataType)
      or self.reduction->isEmpty()
      or self.resolveDataType().oclAsType(StructuredDataType).allMembers()->includes(self.reduction->first().member)
      and self.reduction->select(m | self.reduction->indexOf(m) > 0)->forAll(m |
              self.reduction->at(self.reduction->indexOf(m)-1).member.dataType.oclIsKindOf(StructuredDataType)
          and self.reduction->at(self.reduction->indexOf(m)-1).member.dataType.oclAsType(StructuredDataType).allMembers()
      ->includes(m.member))
  

  -- No member with collection index in the first element in reduction
  inv FirstReduction ('The first \'MemberReference\' in reduction shall not specify both member and collectionIndex. ' + self.toString()):
        self.reduction->first().member.oclIsUndefined() or self.reduction->first().collectionIndex.oclIsUndefined()
  



context ParameterBinding
  -- Matching data type
  inv ParameterBindingTypes ('The provided \'DataUse\' shall conform to the \'DataType\' of the referenced \'Parameter\'.' + self.toString()):
        self.dataUse.resolveDataType().conformsTo(self.parameter.dataType)
  

  -- Use of a 'StructuredDataInstance' with non-optional 'Member's
  inv OmitValueParameter ('A non-optional \'Member\' of a \'StructuredDataType\' shall have a \'DataUse\' specification assigned to it that is different from \'OmitValue\' or \'AnyValueOrOmit\'.' + self.toString()):
        self.parameter.oclIsTypeOf(Member) and self.parameter.oclAsType(Member).isOptional = false
             implies not self.dataUse.oclIsTypeOf(OmitValue) and not self.dataUse.oclIsTypeOf(AnyValueOrOmit)
  



context MemberReference
  -- Collection index expressions for collections only
  inv CollectionIndex ('If the type of the related \'DataUse\' is not \'CollectionDataType\' then the collectionIndex shall be undefined. ' + self.toString()):
        self.collectionIndex.oclIsUndefined()
              or self.container().oclAsType(DataUse).resolveDataType().oclIsKindOf(CollectionDataType)
  

  -- Either member or collection index is required
  inv MemberOrReduction ('Either the member or collectionIndex shall be specified. ' + self.toString()):
        not self.member.oclIsUndefined() or not self.collectionIndex.oclIsUndefined()
  



context DataInstanceUse
  -- 'DataInstance' reference or non-empty 'argument' or non-empty 'item'
  inv DataInstanceOrArgumentsOrItems ('If a \'dataInstance\' is not specified, either a non-empty \'argument\' set or a non-empty \'item\' set shall be specified.' + self.toString()):
        not self.dataInstance.oclIsUndefined() or not self.argument->isEmpty() or not self.item->isEmpty()
  

  -- Valid 'DataType' for items
  inv DataTypeOfItemsInDataInstance ('The items in the \'item\' property shall conform to the \'itemType\' of the resolved \'CollectionDataType\'.' + self.toString()):
        self.item->forAll(i | i.resolveDataType().conformsTo(self.resolveDataType().oclAsType(CollectionDataType).itemType))
  

  -- No 'item' if 'dataInstance' is specified
  inv NoItemWithDataInstance ('The \'item\' property shall be empty if the \'dataInstance\' property is specified.' + self.toString()):
        not self.dataInstance.oclIsUndefined() and self.item->isEmpty()
  



context SpecialValueUse
  -- Empty 'argument' and 'reduction' sets
  inv SpecialValueArgumentReduction ('The \'argument\' and \'reduction\' sets shall be empty.' + self.toString()):
        self.reduction->isEmpty() and self.argument->isEmpty()
  



context FunctionCall
  -- Matching parameters
  inv FunctionCallParameters ('All \'FormalParameter\'s of the invoked \'Function\' shall be bound.' + self.toString()):
        self.function.formalParameter->forAll(p | self.argument->exists(a | a.parameter = p))
  



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.componentInstance.type.allVariables()->includes(self.variable)  
          and self.componentInstance.role = ComponentInstanceRole::Tester
  



context PredefinedFunctionCall
  -- Compatible actual parameters
  inv PredefinedFunctionCallParameters ('The number and type of actual parameters shall be compatible with the formal parameters of the invoked \'PredefinedFunction\' according to the specification of the \'PredefinedFunction\'.' + self.toString()):
        true --This constraint cannot be expressed formally.
  

  -- Empty 'argument' and 'reduction' sets
  inv PredefinedFunctionCallArgumentReduction ('The \'argument\' and \'reduction\' sets shall be empty.' + self.toString()):
        self.reduction->isEmpty() and self.argument->isEmpty()
  



context LiteralValueUse
  -- Exactly one value specification
  inv SpecifiedLiteralValue ('There shall be exactly one value specification, where either the \'value\', or the \'intValue\', or the \'boolValue\' property is be specified, but not more than one of them.' + self.toString()):
        not self.value.oclIsUndefined() 
          xor not self.intValue.oclIsUndefined() 
          xor not self.boolValue.oclIsUndefined()
  

  -- Empty 'argument' and 'reduction' sets if not 'dataType'
  inv LiteralValueArgumentReduction ('If \'dataType\' is not specified then the \'argument\' and \'reduction\' sets shall be empty.' + self.toString()):
        (self.dataType.oclIsUndefined()) 
              implies (self.reduction->isEmpty() and self.argument->isEmpty())
  

  -- Integer type for integer value
  inv LiteralValueIntType ('If \'intValue\' is specified then the \'dataType\' is either unspecified or the specified \'DataType\' conforms to predefined type \'Integer\'.' + self.toString()):
        not self.intValue.oclIsUndefined() 
          implies (self.dataType.oclIsUndefined() or self.dataType.conformsTo('Integer'))
  

  -- Boolean type for Boolean value
  inv LiteralValueBoolType ('If \'boolValue\' is specified then the \'dataType\' is either unspecified or the specified \'DataType\' conforms to predefined type \'Boolean\'.' + self.toString()):
        not self.boolValue.oclIsUndefined() 
          implies (self.dataType.oclIsUndefined() or self.dataType.conformsTo('Boolean'))
  



context DataElementUse
  -- 'DataElement' reference or non-empty 'argument' or non-empty 'item'
  inv DataInstanceOrArgumentsOrItemsInDataElementUse ('If a \'dataElement\' is not specified, or if the \'dataElement\' is resolved to a \'StructuredDataType\' or a \'CollectionDataType\', either a non-empty \'argument\' set or a non-empty \'item\' set shall be specified.' + self.toString()):
        not (self.dataElement.oclIsUndefined() and self.argument->isEmpty() and self.item->isEmpty())
          and not (self.dataElement.oclIsKindOf(StructuredDataType) and self.argument->isEmpty())
          and not (self.dataElement.oclIsKindOf(CollectionDataType) and self.item->isEmpty())
  

  -- Valid 'DataType' for items
  inv DataTypeOfItemsInDataInstance ('The items in the \'item\' property shall conform to the \'itemType\' of the resolved \'CollectionDataType\'.' + self.toString()):
        self.item->forAll(i | i.resolveDataType().conformsTo(self.resolveDataType().oclAsType(CollectionDataType).itemType))
  

  -- Only 'item' if the resolved data type is 'CollectionDataType'
  inv ItemOnlyWithCollectionDataType ('The \'item\' property shall be non-empty if the \'dataElement\' property is resolved to a \'CollectionDataType\'.' + self.toString()):
        (((self.dataElement.oclIsKindOf(CollectionDataType))
      or self.dataElement.oclIsUndefined())
      and not self.item->isEmpty())
      or self.item->isEmpty()
  

  -- Matching parameters for 'Function's
  inv FunctionCallParameters ('All \'FormalParameter\'s shall be bound if the \'dataElement\' refers to a \'Function\'.' + self.toString()):
        not self.dataElement.oclIsKindOf(Function)
      or self.dataElement.oclAsType(Function).formalParameter->forAll(p | self.argument->exists(a | a.parameter = p))
  



context TimeLabelUse
  -- Empty 'argument' and 'reduction' sets
  inv TimeLabelArgumentReduction ('The \'argument\' and \'reduction\' sets shall be empty.' + self.toString()):
        self.reduction->isEmpty() and self.argument->isEmpty()
  

  -- 'TimeLabel's only within the same 'TestDescription' when local ordering is used 
  inv TimeLabelLocallyOrdered ('When local ordering is used, \'TimeLabel\'s shall only be used within the same test description. ' + self.toString()):
        self.getParentTestDescription().isLocallyOrdered = true
      or self.timeLabel.getParentTestDescription() = self.getParentTestDescription()
  



context TimeConstraint
  -- Time constraint expression of type Boolean
  inv TimeConstraintType ('The expression given in the \'DataUse\' specification shall evaluate to predefined type \'Boolean\'.' + self.toString()):
        self.timeConstraintExpression.resolveDataType().name = 'Boolean'
  

  -- Use of local variables only
  inv TimeConstraintVariables ('The expression given in the \'DataUse\' specification shall contain only \'Variable\'s that are local to the \'AtomicBehaviour\' that contains this \'TimeConstraint\'. That is, all \'VariableUse\'s shall reference the \'ComponentInstance\'s which participate in the \'AtomicBehaviour\'.' + self.toString()):
        self.timeConstraintExpression.argument
              ->closure(a | a.dataUse.argument)->collect(pb | pb.dataUse)
              ->union(self.timeConstraintExpression.argument)
              ->select(du | du.oclIsKindOf(VariableUse))
              ->forAll(du | self.container().oclAsType(Behaviour).getParticipatingComponents()->includes(
                  du.oclAsType(VariableUse).componentInstance))
  

  -- Use of local time labels only
  inv TimeConstraintTimeLabels ('In case of locally ordered \'TestDescription\', the expression given in the \'DataUse\' specification shall contain only \'TimeLabel\'s that are local to the \'AtomicBehaviour\' that contains this \'TimeConstraint\'. That is, all \'TimeLabel\'s shall be contained in \'AtomicBehaviour\'s involving the \'ComponentInstance\'s which participate in the \'AtomicBehaviour\' that contains this \'TimeConstraint.' + self.toString()):
        self.timeConstraintExpression.argument
              ->closure(a | a.dataUse.argument)->collect(pb | pb.dataUse)
              ->union(self.timeConstraintExpression.argument)
              ->select(du | du.oclIsKindOf(TimeLabelUse))
              ->forAll(du | self.container().oclAsType(Behaviour).getParticipatingComponents()->includesAll(
                  du.oclAsType(TimeLabelUse).timeLabel.container().oclAsType(Behaviour).getParticipatingComponents()))
  

  -- [Figure 7.2: Time operations]


context TimeOperation
  -- Component required in locally ordered test description
  inv TimeOperationComponent ('If the \'TimeOperation\' is contained in a locally ordered \'TestDescription\' then the \'componentInstance\' shall be specified.' + self.toString()):
        self.getParentTestDescription().isLocallyOrdered 
          implies not self.componentInstance.oclIsUndefined()
  

  -- Time operations on tester components only
  inv TimeOperationComponentRole ('A \'TimeOperation\' shall be performed only on a \'ComponentInstance\' in the role \'Tester\'.' + self.toString()):
        (not self.componentInstance.oclIsUndefined()
           and self.componentInstance.role = ComponentInstanceRole::Tester)
      or (self.oclIsTypeOf(Quiescence)
           and not self.oclAsType(Quiescence).gateReference.oclIsUndefined()
           and self.oclAsType(Quiescence).gateReference.component.role = ComponentInstanceRole::Tester)
  

  -- 'Time' data type for period expression
  inv TimePeriodType ('The \'DataUse\' expression assigned to the \'period\' shall evaluate to a data instance of the \'Time\' data type.' + self.toString()):
        self.period.resolveDataType().oclIsKindOf(Time)
  



context Quiescence
  -- Exclusive use of gate reference or component instance
  inv QuiescenceTarget ('If a \'GateReference\' is provided, a \'ComponentInstance\' shall not be provided and vice versa.' + self.toString()):
        self.gateReference.oclIsUndefined() xor self.componentInstance.oclIsUndefined()
  

  -- [Figure 7.3: Timer and timer operations]


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.componentInstance.role = ComponentInstanceRole::Tester
  



context TimerStart
  -- 'Time' data type for period expression
  inv TimerPeriodType ('The \'DataUse\' expression assigned to the \'period\' shall evaluate to a data instance of the \'Time\' data type.' + self.toString()):
        self.period.resolveDataType().oclIsKindOf(Time)
  



context GateType
  -- Compatible 'DataType's. 
  inv GateType ('The \'DateType\'s specified for the \'GateType\' shall correspond the kind of the \'GateType\'. For \'GateType\' of kind \'Procedure\' only \'ProcedureSignature\'s shall be specified as data types. For \'GateType\' of kind \'Message\' only \'StructuredDataType\'s, \'SimpleDataType\'s and \'CollectionDataType\'s shall be specified as data types. ' + self.toString()):
        (self.kind = GateTypeKind::Procedure and self.allDataTypes()->forAll(t |
      t.oclIsTypeOf(ProcedureSignature)))
      or (self.kind = GateTypeKind::Message and self.allDataTypes()->forAll(t | t.oclIsTypeOf(StructuredDataType)
                  or t.oclIsKindOf(SimpleDataType) or t.oclIsTypeOf(CollectionDataType)))
  



context GateReference
  -- Gate instance of the referred component instance
  inv GateInstanceReference ('The referred \'GateInstance\' shall be contained in the \'ComponentType\' of the referred \'ComponentInstance\'.' + self.toString()):
        self.component.type.allGates()->includes(self.gate)
  



context Connection
  -- Self-loop connections are not permitted
  inv NoSelfLoop ('The \'endPoint\'s of a \'Connection\' shall not be the same. Two endpoints are the same if both, the referred \'ComponentInstance\'s and the referred \'GateInstance\'s, are identical.' + self.toString()):
        self.endPoint->forAll(e1 | self.endPoint->one(e2 | e1.gate = e2.gate
              and e1.component = e2.component))
  

  -- Consistent type of a connection
  inv ConsistentConnectionType ('The \'GateInstance\'s of the two \'endPoint\'s of a \'Connection\' shall refer to the same \'GateType\'.' + self.toString()):
        self. endPoint.gate.type->asSet()->size() = 1
  



context TestConfiguration
  -- 'TestConfiguration' and components roles
  inv ComponentRoles ('A \'TestConfiguration\' shall contain at least one \'Tester\' and one \'SUT\' \'ComponentInstance\'.' + self.toString()):
        self.componentInstance->exists(c | c.role = ComponentInstanceRole::Tester)
      and self.componentInstance->exists(c | c.role = ComponentInstanceRole::SUT)
  

  -- Only 'Connection's between own 'ComponentInstance's 
  inv OwnedComponents ('A \'TestConfiguration\' shall only contain \'Connection\'s between gates of its own \'ComponentInstance\'s. ' + self.toString()):
        self.connection->forAll(c |
              self.componentInstance->includesAll(c.endPoint.component))
  

  -- Minimal 'TestConfiguration'
  inv MinimalTestConfiguration ('Each \'TestConfiguration\' shall specify at least one \'Connection\' that connects a \'GateInstance\' of a \'ComponentInstance\' in the role \'Tester\' with a \'GateInstance\' of a \'ComponentInstance\' in the role \'SUT\'.' + self.toString()):
        self.connection->exists(c |
              c.endPoint.component.role->includesAll(Set{ComponentInstanceRole::SUT, ComponentInstanceRole::Tester}))
  

  -- At most one connection between any two 'GateInstance'/'ComponentInstance' pairs
  inv UniqueConnections ('Given the set of \'Connection\'s contained in a \'TestConfiguration\'. There shall be no two \'Connection\'s containing \'GateReference\'s that in turn refer to identical pairs of \'GateInstance\'/\'ComponentInstance\'.' + self.toString()):
        self.connection->forAll(c1 | self.connection->one(c2 |
              not c1.endPoint->reject(ep1 | not c2.endPoint->exists(ep2 |
                  ep1.component = ep2.component and ep1.gate = ep2.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().name = 'Boolean')
  

  -- 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 a 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.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT)
              ->forAll(c | self.guard->exists(ex | ex.componentInstance = c))
          or not self.getParentTestDescription().isLocallyOrdered
  

  -- Single guard in totally ordered test description
  inv SingleTotalGuard ('If the \'Block\' is contained in a totally ordered \'TestDescription\' then there shall not be more than one guard. ' + self.toString()):
        self.getParentTestDescription().isLocallyOrdered or self.guard->size() <= 1
  



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()):
        self.getParentTestDescription().isLocallyOrdered 
          implies not self.componentInstance.oclIsUndefined()
  

  -- Only local variables and time labels in case of locally ordered test description
  inv LocalVariablesAndTimersInExpression ('If the componentInstance is specified then all \'Variable\'s and \'TimeLabel\'s used in the expression shall be local to that \'ComponentInstance\'.' + self.toString()):
        self.expression.argument
              ->closure(a | a.dataUse.argument)->collect(pb | pb.dataUse)
              ->union(self.expression.argument)
              ->including(self.expression)
              ->select(du | du.oclIsKindOf(VariableUse))
              ->forAll(du | du.oclAsType(VariableUse).componentInstance = self.componentInstance)
          and self.expression.argument
              ->closure(a | a.dataUse.argument)->collect(pb | pb.dataUse)
              ->union(self.expression.argument)
              ->including(self.expression)
              ->select(du | du.oclIsKindOf(TimeLabelUse))
              ->forAll(du | du.oclAsType(TimeLabelUse).timeLabel.container().oclAsType(Behaviour)
                  .getParticipatingComponents()->includes(self.componentInstance))
  



context BoundedLoopBehaviour
  -- No guard constraint
  inv BoundedGuard ('The \'Block\' of a \'BoundedLoopBehaviour\' shall not have a \'guard\'.' + self.toString()):
        self.block->forAll(b | b.guard.oclIsUndefined())
  

  -- Iteration number shall be countable and positive
  inv LoopIteration ('The expression assigned to the \'numIteration\' property shall evaluate to a countable \'SimpleDataInstance\' of an arbitrary user-defined data type, e.g. a positive Integer value.' + self.toString()):
        self.numIteration->forAll(e | e.expression.resolveDataType().conformsTo('Integer'))
  

  -- 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.componentInstance = c))
          or not self.getParentTestDescription().isLocallyOrdered
  

  -- Single numIteration in totally ordered test description
  inv SingleTotalIterationCount ('If the \'BoundedLoopBehaviour\' is contained in a totally ordered \'TestDescription\' then there shall be exactly  one numIteration.' + self.toString()):
        self.getParentTestDescription().isLocallyOrdered or self.numIteration->size() = 1
  



context OptionalBehaviour
  -- First 'AtomicBehaviour' in block allowed
  inv OptionalBehaviourStart ('The block of an \'OptionalBehaviour\' shall start with a tester-to-tester \'Interaction\'. ' + self.toString()):
        self.block.behaviour->first().oclIsKindOf(Interaction) 
      and self.block.behaviour->first().oclAsType(Interaction) 
              ->collect(i | i.sourceGate.component->union(i.target.targetGate.component))
              ->forAll(c | c.role = ComponentInstanceRole::Tester)
  

  -- No other testers except the participants of starting 'Interaction' within 'OptionalBehaviour' in locally ordered 'TestDescription'
  inv OptionalBehaviourParticipation ('If an \'OptionalBehaviour\' is included in a locally ordered \'TestDescription\' then no other tester \'ComponentInstance\' shall participate in the block of the \'OptionalBehaviour\' than the source and target of the starting \'Interaction\' except when being a target of the starting \'Interaction\' in a nested \'OptionalBehaviour\'. ' + self.toString()):
        let initial = self.block.behaviour->first().oclAsType(Interaction),
          initialComponents = initial->collect(i | i.sourceGate.component->union(i.target.targetGate.component)),
          optionals = self.block->closure(
              b | b.behaviour
              ->select(oclIsKindOf(SingleCombinedBehaviour)).oclAsType(SingleCombinedBehaviour).block
              ->union(b.behaviour
              ->select(oclIsKindOf(MultipleCombinedBehaviour)).oclAsType(MultipleCombinedBehaviour).block)
          ).behaviour->select(oclIsKindOf(OptionalBehaviour)).oclAsType(OptionalBehaviour),
          optionalTargets = optionals.block->select(b | b.behaviour->select(i | i.oclIsKindOf(Interaction))->first().oclAsType(Interaction).target.targetGate.component)
          in
          self.block.getParticipatingComponents()
              ->forAll(c | initialComponents->includes(c) or optionalTargets->includes(c))
          or not self.getParentTestDescription().isLocallyOrdered
  



context AlternativeBehaviour
  -- Number of 'Block's
  inv AlternativeBlockCount ('An \'AlternativeBehaviour\' shall contain at least two \'Block\'s. ' + self.toString()):
        self.block->size() > 1
  

  -- First behaviour of 'Block's
  inv FirstBlockBehaviour ('Each block of an \'AlternativeBehaviour\' shall start with a tester-input event. ' + self.toString()):
        self.block->forAll(b | b.behaviour->first().isTesterInputEvent())
  

  -- Same component if locally ordered
  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{}
          ->including(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->including(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          -> including(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance)
          ->size() = 1 or not self.getParentTestDescription().isLocallyOrdered
  

  -- Tester participating in locally ordered case
  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{}
          ->including(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->including(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          -> including(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance),
          nonOptionalBlocks = self.block->closure(
              b | b.behaviour->reject(oclIsKindOf(OptionalBehaviour))
                  ->select(oclIsKindOf(SingleCombinedBehaviour)).oclAsType(SingleCombinedBehaviour).block
              ->union(b.behaviour->reject(oclIsKindOf(OptionalBehaviour))
                  ->select(oclIsKindOf(MultipleCombinedBehaviour)).oclAsType(MultipleCombinedBehaviour).block)
          )
          in
          targetComponent->includesAll(
              nonOptionalBlocks.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT))
          or not self.getParentTestDescription().isLocallyOrdered
  

  -- OptionalBehaviour in locally ordered case
  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{}
          ->including(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->including(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          -> including(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance)
          in
          self.block.behaviour->select(oclIsKindOf(OptionalBehaviour)) .oclAsType(OptionalBehaviour).block
              ->first().oclAsType(Interaction).sourceGate.component->forAll(c | targetComponent->includes(c))
          or not self.getParentTestDescription().isLocallyOrdered
  



context ConditionalBehaviour
  -- Guard for 'ConditionalBehaviour' with single block
  inv ConditionalFirstGuard ('If there is only one \'Block\' specified, it shall have a \'guard\'.' + self.toString()):
        self.block->size() > 1 or self.block->first().guard->size() > 1
  

  -- Possible else block for 'ConditionalBehaviour' with multiple blocks
  inv ConditionalLastGuard ('All \'Block\'s specified, except the last one, shall have a \'guard\'.' + self.toString()):
        self.block->size() = 1
      or self.block->forAll(b | b = self.block->last() or b.guard ->size() > 1)
  



context ParallelBehaviour
  -- Number of blocks in 'ParallelBehaviour'
  inv ParallelBlockCount ('There shall be at least two \'Block\'s specified.' + self.toString()):
        self.block->size() > 1
  

  -- [Figure 9.3: Exceptional and periodic behaviour]


context ExceptionalBehaviour
  -- First 'AtomicBehaviour' in block allowed
  inv FirstExceptionalBehaviour ('The block of an \'ExceptionalBehaviour\' shall start with a tester-input event.' + self.toString()):
        self.block.behaviour->first().isTesterInputEvent()
  

  -- Guarded component shall be a 'Tester' component
  inv ExceptionalGuardedComponent ('The \'guardedComponent\' shall refer to a \'ComponentInstance\' with the role of \'Tester\'.' + self.toString()):
        self.guardedComponent.oclIsUndefined() or self.guardedComponent.role = ComponentInstanceRole::Tester
  

  -- Same component if locally ordered and guarded component present
  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{}
          ->including(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->including(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          -> including(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance)
          in
          guardedComponent->includesAll(targetComponent)
          or not self.getParentTestDescription().isLocallyOrdered
  

  -- Tester participating in locally ordered case
  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{}
          ->including(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->including(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          -> including(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance),
          nonOptionalBlocks = self.block->closure(
              b | b.behaviour->reject(oclIsKindOf(OptionalBehaviour))
                  ->select(oclIsKindOf(SingleCombinedBehaviour)).oclAsType(SingleCombinedBehaviour).block
              ->union(b.behaviour->reject(oclIsKindOf(OptionalBehaviour))
                  ->select(oclIsKindOf(MultipleCombinedBehaviour)).oclAsType(MultipleCombinedBehaviour).block)
          )
          in
          targetComponent->includesAll(
              nonOptionalBlocks.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT))
          or not self.getParentTestDescription().isLocallyOrdered
  

  -- OptionalBehaviour in locally ordered case
  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{}
          ->including(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->including(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          -> including(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance)
          in
          self.block.behaviour->select(oclIsKindOf(OptionalBehaviour)).oclAsType(OptionalBehaviour).block
              ->first().oclAsType(Interaction).sourceGate.component->forAll(c | targetComponent->includes(c))
          or not self.getParentTestDescription().isLocallyOrdered
  



context PeriodicBehaviour
  -- 'Time' data type for period expression
  inv PeriodType ('The \'DataUse\' expression assigned to the \'period\' shall evaluate to a data instance of the \'Time\' data type.' + self.toString()):
        self.period->forAll(e | e.expression.resolveDataType().oclIsKindOf(Time))
  

  -- 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.componentInstance = c))
          or not self.getParentTestDescription().isLocallyOrdered
  



context Break
  -- Break in conditional behaviour only
  inv ConditionalBreak ('A \'Break\' shall be contained directly in the block of a \'ConditionalBehaviour\'. ' + self.toString()):
        self.container().container().oclIsKindOf(ConditionalBehaviour)
  

  -- No behaviours after break
  inv BreakIsLast ('A \'Break\' shall be the last behaviour in the containing \'Block\'. ' + self.toString()):
        self.container().oclAsType(Block).behaviour->last() = self
  



context VerdictAssignment
  -- Verdict of type 'Verdict'
  inv VerdictType ('The \'verdict\' shall evaluate to a, possibly predefined, instance of a \'SimpleDataInstance\' of data type \'Verdict\'.' + self.toString()):
        self.verdict.resolveDataType().name = 'Verdict'
  

  -- No 'SpecialValueUse'
  inv VerdictNoSpecialValueUse ('The \'verdict\' shall not evaluate to an instance of a \'SpecialValueUse\'.' + self.toString()):
        not self.verdict.oclIsKindOf(SpecialValueUse)
  



context Assertion
  -- Boolean condition
  inv AssertionOtherwise ('The \'condition\' shall evaluate to predefined \'DataType\' \'Boolean\'.' + self.toString()):
        self.condition.resolveDataType().name = 'Boolean'
  

  -- Otherwise of type 'Verdict'
  inv AssertionVerdict ('The \'otherwise\' shall evaluate to a, possibly predefined, instance of a \'SimpleDataInstance\' of data type \'Verdict\'.' + self.toString()):
        self.otherwise.oclIsUndefined() or self.otherwise.resolveDataType().name = 'Verdict'
  

  -- No 'SpecialValueUse'
  inv AssertionNoSpecialValueUse ('The \'otherwise\' shall not evaluate to an instance of a \'SpecialValueUse\'.' + self.toString()):
        not self.otherwise.oclIsKindOf(SpecialValueUse)
  

  -- [Figure 9.5: Interaction behaviour]


context Interaction
  -- Gate references of an interaction shall be connected
  inv ConnectedInteractionGates ('The \'GateReference\'s that act as source or target(s) of an \'Interaction\' shall be interconnected by a \'Connection\' which is contained in the \'TestConfiguration\' referenced by the \'TestDescription\' containing the \'Interaction\'.' + self.toString()):
        self.target->forAll(t |
              self.getParentTestDescription().testConfiguration.connection->exists(c |
                  not c.endPoint->reject(ep | 
                      (ep.component = self.sourceGate.component and ep.gate = self.sourceGate.component) or
                      (ep.component = t.targetGate.component and ep.gate = t.targetGate.gate)
                  )->isEmpty()))
  



context Message
  -- 'DataType' resolvable
  inv DataTypeResolvable ('If the \'argument\' is \'DataInstanceUse\', either the \'dataType\' property or the \'dataInstance\' property shall be provided. If the \'argument\' is a \'DataElementUse\', the \'dataElement\' property shall be provided.' + self.toString()):
        not self.argument.oclIsUndefined()
  

  -- Type of message argument
  inv MessageArgumentAndGateType ('The \'DataUse\' specification referred to in the \'argument\' shall match one of the \'DataType\'s referenced in the \'GateType\' definition of the \'GateInstance\'s referred to by the source and target \'GateReference\'s of the \'Interaction\'.' + self.toString()):
        (self.argument.oclIsKindOf(AnyValue)
      and self.argument. resolveDataType().oclIsUndefined())
      or (self.sourceGate.gate.type.allDataTypes()-> exists(t | self.argument.resolveDataType().conformsTo(t))
      and self.target->forAll(t | t.targetGate.gate.type.allDataTypes()->exists(t | self.argument.resolveDataType().conformsTo(t))))
  

  -- Use of variables in the 'argument' specification
  inv MessageArgumentVariableUse ('The use of \'Variable\'s in the \'DataUse\' specification shall be restricted to \'Variable\'s of \'ComponentInstance\'s that participate in this \'Message\' via the provided \'GateReference\'s.' + self.toString()):
        (not self.argument.oclIsKindOf(VariableUse)
          or (self.sourceGate.component = self.argument.oclAsType(VariableUse).componentInstance
          or self.target->exists(t | 
              t.targetGate.component = self.argument.oclAsType(VariableUse).componentInstance)))
      
      and self.argument.argument->forAll(a |
              not a.dataUse.oclIsKindOf(VariableUse)
              or (self.sourceGate.component = a.dataUse.oclAsType(VariableUse).componentInstance
              or self.target->exists(t | 
                  t.targetGate.component = a.dataUse.oclAsType(VariableUse).componentInstance)))
      
      and self.argument.argument->closure(a | a.dataUse.argument)->forAll(a |
              not a.dataUse.oclIsKindOf(VariableUse)
              or (self.sourceGate.component = a.dataUse.oclAsType(VariableUse).componentInstance
              or self.target->exists(t | 
                  t.targetGate.component = a.dataUse.oclAsType(VariableUse).componentInstance)))
  

  -- Conforming data type for 'argument' and 'variable'
  inv MessageArgumentAndVariableType ('If a \'Variable\' is specified for a \'Target\', the \'DataType\' of \'DataUse\' specification of the \'argument\' shall conform to the \'DataType\'s of referenced \'Variable\'s of all \'Target\'s.' + self.toString()):
        self.target->forAll(t | t.valueAssignment->size() = 0
              or not self.argument.resolveDataType().oclIsUndefined()
           and t.valueAssignment->forAll(v | self.argument.resolveDataType().conformsTo(v.variable.dataType)))
  



context ProcedureCall
  -- Only point-to-point procedure calls
  inv ProcedureCallTargetCount ('The \'target\' of \'ProcedureCall\' shall contain exactly one \'Target\'. ' + self.toString()):
        self.target->size() = 1
  

  -- Each call has a reply
  inv ProcedureCallHasReply ('For every \'ProcedureCall\' with empty \'replyTo\' there shall be one or more \'ProcedureCall\'s that have this \'ProcedureCall\' as \'replyTo\'. ' + self.toString()):
        ProcedureCall.allInstances()->exists(pc | pc.replyTo = self)
  

  -- Call and reply within the same 'TestDescription'
  inv ProcedureCallAndReply ('The \'ProcedureCall\' referenced in the \'replyTo\' shall be within the same \'TestDescription\' as this \'ProcedureCall\'. ' + self.toString()):
        self.replyTo.oclIsUndefined() 
          or self.replyTo.getParentTestDescription() = self.getParentTestDescription()
  

  -- Call and reply between same components
  inv ProcedureCallReplyGates ('The \'sourceGate\' and \'target\' of a \'ProcedureCall\' with \'replyTo\' shall match the \'target\' and \'sourceGate\' of the \'ProcedureCall\' in the \'replyTo\'. That is, corresponding \'GateReference\'s shall be the equal. ' + self.toString()):
        ProcedureCall.allInstances()->select(pc | pc.replyTo = self)->forAll(
      reply |
      reply.target->forAll(t | t.targetGate.component = self.sourceGate.component)
      and reply.target->forAll(t | t.targetGate.gate = self.sourceGate.gate)
      and self.target->forAll(t | t.targetGate.component = reply.sourceGate.component)
      and self.target->forAll(t | t.targetGate.gate  = reply.sourceGate.gate))
  

  -- Synchronous procedure calls
  inv ProcedureCallSynchronousCalling ('A \'ProcedureCall\' with empty \'replyTo\' shall not be followed by any behaviour in which the component specified in the \'sourceGate\' is participating, other than a \'ProcedureCall\' that specifies this \'ProcedureCall\' as \'replyTo\' or an \'AlternativeBehaviour\' that contains such a \'ProcedureCall\' in the beginning of a \'block\'. ' + self.toString()):
        let source = self.sourceGate.component,
          affectingBehaviours = self.container().oclAsType(Block).behaviour
             ->reject(b | b.oclIsKindOf(ActionBehaviour)
                  and b.oclAsType(ActionBehaviour).componentInstance <> source)
              ->reject(b | b.oclIsKindOf(Interaction)
                 and b.oclAsType(Interaction).sourceGate.component <> source
                 and b.oclAsType(Interaction).target->forAll(t | t.targetGate.component <> source))
              ->reject(b| b.oclIsKindOf(TestDescriptionReference)
                  and (not b.oclAsType(TestDescriptionReference).componentInstanceBinding->isEmpty()
                      and not b.oclAsType(TestDescriptionReference).componentInstanceBinding
                          .actualComponent->includes(self))),
          following = affectingBehaviours ->at(affectingBehaviours->indexOf(self) + 1)
          in (following.oclIsKindOf(ProcedureCall) and following.oclAsType(ProcedureCall).replyTo = self)
          or (following.oclIsKindOf(AlternativeBehaviour)
              and following.oclAsType(AlternativeBehaviour).block->exists(
                  b | b.behaviour->first().oclIsKindOf(ProcedureCall)
                 and b.behaviour->first().oclAsType(ProcedureCall).replyTo = self))
  

  -- Type of procedure call
  inv ProcedureCallSignatureInGateTypes ('The \'ProcedureSignature\' referred to in the \'procedure\' shall be one of the \'DataType\'s referenced in the \'GateType\' definition of the \'GateInstance\'s referred to by the source and target \'GateReference\'s of the \'ProcedureCall\'. ' + self.toString()):
        self.sourceGate.gate.type.allDataTypes()->includes(self.signature)
          and self.target->forAll(targetGate.gate.type.allDataTypes()->includes(self.signature))
  

  -- No mixing of parameters
  inv ProcedureParameterKind ('All \'ParameterBinding\'s specified in the \'argument\' shall refer to \'ProcedureParameter\'s of the same \'ParameterKind\'. ' + self.toString()):
        self.argument->collect(pb | pb.parameter.oclAsType(ProcedureParameter).kind)
              ->asSet()->size() <= 1
  

  -- Matching procedure arguments