import "../library/common.eol";
import "../library/helper.eol";
import "../library/debug.eol";

context Element {
  //[There are no constraints specified.]
}

context NamedElement {
  //Mandatory name
  constraint MandatoryName {
    check:     not self.name.oclIsUndefined() and self.name.size() > 0
    message:   self.prefix() + 
               "A 'NamedElement' shall have the 'name' property set and the 'name' shall be not an empty String."
  }

  //Distinguishable qualified names
  constraint DistinquishableName {
    check:     NamedElement.allInstances()->one(e | e.qualifiedName = self.qualifiedName)
    message:   self.prefix() + 
               "All qualified names of instances of 'NamedElement's shall be distinguishable within a TDL model."
  }

  //[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 PackageableElement {
  //[There are no constraints specified.]
}

context Package {
  //No cyclic imports
  constraint CyclicImports {
    check:     self.`import`->asOrderedSet()->closure(i | i.importedPackage.`import`)->forAll(i | 
              i.importedPackage <> self)
    message:   self.prefix() + 
               "A 'Package' shall not import itself directly or indirectly."
  }

}

context ElementImport {
  //Consistency of imported elements
  constraint ConsistentImports {
    check:     self.importedElement->forAll(e | self.importedPackage.packagedElement->includes(e))
    message:   self.prefix() + 
               "All imported 'PackageableElement's referenced by an 'ElementImport' shall be directly owned by the imported 'Package'."
  }

  //[Figure 5.2: Miscellaneous elements]
}

context Comment {
  //No nested comments
  constraint CommentNestedComments {
    check:     self.comment->isEmpty()
    message:   self.prefix() + 
               "A 'Comment' shall not contain 'Comment's."
  }

  //No annotations to comments
  constraint CommentNestedAnnotations {
    check:     self.annotation->isEmpty()
    message:   self.prefix() + 
               "A 'Comment' shall not contain 'Annotation's."
  }

}

context Annotation {
  //No nested annotations
  constraint AnnotationNestedAnnotations {
    check:     self.annotation->isEmpty()
    message:   self.prefix() + 
               "An 'Annotation' shall not contain 'Annotation's"
  }

  //No comments to annotations
  constraint AnnotationNestedComments {
    check:     self.comment->isEmpty()
    message:   self.prefix() + 
               "An 'Annotation' shall not contain 'Comment's."
  }

}

context AnnotationType {
  //[There are no constraints specified.]
}

context TestObjective {
  //[There are no constraints specified.]
}

context Extension {
  //Inherit from element of the same meta-class
  constraint Extension {
    check:     self.container().oclIsTypeOf(self.extending.oclType())
    message:   self.prefix() + 
               "The element containing an 'Extension' and the element in the 'extending' property shall have the same meta-class."
  }

}

context ConstraintType {
  //[There are no constraints specified.]
}

context Constraint {
  //Effectively static quantifiers 
  constraint StaticQuantifiers {
    check:     self.quantifer.forAll(q | q.isEffectivelyStatic())
    message:   self.prefix() + 
               "All 'DataUse's specified as 'quantifier's shall be effectively static."
  }

  //Empty arguments for quantifiers 
  constraint StaticQuantifiers {
    check:     self.quantifer.forAll(q | q.argument.isEmpty())
    message:   self.prefix() + 
               "The 'argument' sets for all 'DataUse's specified as 'quantifier's shall be empty."
  }

  //Constraint applicability for 'union' and 'uniontype' 
  constraint ConstraintApplicabilityUnionUniontype {
    check:     (self.type.name = 'union' or self.type.name = 'uniontype') 
          implies self.container().oclIsTypeOf(StructuredDataType)
    message:   self.prefix() + 
               "The predefined 'ConstraintType's 'union' and 'uniontype' shall be applied to 'StructuredDataType's only. "
  }

  //Constraint applicability for 'range' and 'format'
  constraint ConstraintApplicabilityRangeFormat {
    check:     (self.type.name = 'range' or self.type.name = 'format') 
          implies (self.container().oclIsTypeOf(SimpleDataType)
             or (self.container().oclIsTypeOf(Member) 
                 and self.container().oclAsTypeOf(Member).dataType.oclIsTypeOf(SimpleDataType)))
    message:   self.prefix() + 
               "The predefined 'ConstraintType's 'range' and 'format' shall be applied to 'SimpleDataType's and 'Member's with a 'SimpleDataType' 'dataType' only. "
  }

  //Constraint applicability for 'length', 'minLength', and 'maxLength' 
  constraint ConstraintApplicabilityLength {
    check:     (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().oclAsTypeOf(Member).dataType.oclIsTypeOf(SimpleDataType))
                 and self.container().oclAsTypeOf(Member).dataType.oclIsTypeOf(CollectionDataType)))
    message:   self.prefix() + 
               "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. "
  }

  //Quantifiers for 'length', 'minLength', and 'maxLength'
  constraint ConstraintQuantifierLength {
    check:     (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.resloveDataType().conformsTo('Integer')))
    message:   self.prefix() + 
               "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'. "
  }

  //Quantifiers for 'range' 
  constraint ConstraintQuantifierRange {
    check:     (self.type.name = 'length') 
          implies (self.quantifier->size() = 2 
              and self.quantifier->forAll(q | q.resloveDataType().conformsTo('Integer')))
    message:   self.prefix() + 
               "The predefined 'ConstraintType' 'range' shall be used with exactly two 'quantifier's resolved to instance conforming to the predefined 'Integer' 'DataType'. "
  }

}

context DataResourceMapping {
  //[There are no constraints specified.]
}

context MappableDataElement {
  //[There are no constraints specified.]
}

context DataElementMapping {
  //Restricted use of 'ParameterMapping'
  constraint ParameterMappingType {
    check:     self.parameterMapping->size() = 0
      or (self.mappableDataElement.oclIsTypeOf(StructuredDataType) 
      and self.parameterMapping->forAll(p | 
               self.mappableDataElement.allMembers()->includes(p.parameter))) 
      or (self.mappableDataElement.oclIsKindOf(Action) 
      and self.parameterMapping->forAll(p | 
               self.mappableDataElement.formalParameter->includes(p.parameter)))
    message:   self.prefix() + 
               "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'."
  }

  //All parameters shall be mapped
  constraint ParameterMappingType {
    check:     (self.mappableDataElement.oclIsTypeOf(SimpleDataType)
      or (self.mappableDataElement.oclIsTypeOf(StructuredDataType)
      and self.mappableDataElement.member->forAll(p | 
               self.parameterMapping->exists(m | m.parameter = p)))
      or (self.mappableDataElement.oclIsKindOf(Action) 
      and self.mappableDataElement.formalParameter->forAll(p | 
               self.parameterMapping->exists(m | m.parameter = p)))
      and self.parameterMapping->forAll(p | 
               self.mappableDataElement.formalParameter->includes(p.parameter)))
    message:   self.prefix() + 
               "If the 'mappableDataElement' refers to a 'StructuredDataType', an 'Action' or a 'Function' definition, all the 'Parameters' contained in the 'mappableDataElement' shall be mapped."
  }

}

context ParameterMapping {
  //[There are no constraints specified.]
  //[Figure 6.2: Basic data concepts and simple data]
}

context DataType {
  //[There are no constraints specified.]
}

context DataInstance {
  //[There are no constraints specified.]
}

context SimpleDataType {
  //[There are no constraints specified.]
}

context SimpleDataInstance {
  //SimpleDataInstance shall refer to SimpleDataType
  constraint SimpleDataInstanceType {
    check:     self.dataType.oclIsKindOf(SimpleDataType)
    message:   self.prefix() + 
               "The inherited reference 'dataType' from 'DataInstance' shall refer to instances of 'SimpleDataType' solely."
  }

  //[Figure 6.3: Structured data type and instance]
}

context StructuredDataType {
  //Different member names in a structured data type
  constraint DistinguishableMemberNames {
    check:     self.allMembers()->isUnique(e | e.name)
    message:   self.prefix() + 
               "All 'Member' names of a 'StructuredDataType' (including the names of inherited 'Members') shall be distinguishable."
  }

}

context Member {
  //[There are no constraints specified.]
}

context StructuredDataInstance {
  //StructuredDataInstance shall refer to StructuredDataType
  constraint StructuredDataInstance {
    check:     self.dataType.oclIsTypeOf(StructuredDataType)
    message:   self.prefix() + 
               "The inherited reference 'dataType' from 'DataInstance' shall refer to instances of 'StructuredDataType' solely."
  }

  //'Member' of the 'StructuredDataType'
  constraint ExistingMemberOfDataType {
    check:     self.memberAssignment->forAll(a | self.dataType.allMembers()->includes(a.member))
    message:   self.prefix() + 
               "The referenced 'Member' shall be contained in or inherited by the 'StructuredDataType' that the 'StructuredDataInstance', which contains this 'MemberAssignment', refers to."
  }

  //Unique assignments for each 'Member' of the 'StructuredDataType'
  constraint UniqueMemberAssignments {
    check:     self.memberAssignment->isUnique(m | m.member)
    message:   self.prefix() + 
               "There shall be at most one 'memberAssignment' for each 'Member' of the 'StructuredDataType' that the 'StructuredDataInstance', which contains this 'MemberAssignment', refers to."
  }

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

  //'uniontype' constraint on the type of the 'StructuredDataInstance'
  constraint StructuredDataInstanceUniontypeConstraint {
    check:     not self.dataType.allConstraints->exists(c | c.type.name = 'uniontype')
          or self.memberAssignment->forAll(m | self.dataType.member.contains(m)
              or self.dataType.extension->one(e | 
                  e.extending.oclAsType(StructuredDataType).allMembers()->contains(m)))
    message:   self.prefix() + 
               "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."
  }

}

context MemberAssignment {
  //Type of a 'memberSpec' shall conform to the type of the 'member'
  constraint MatchingMemberDataType {
    check:     self.memberSpec.resolveDataType().conformsTo(self.member.dataType)
    message:   self.prefix() + 
               "The 'DataType' of the 'DataUse' of 'memberSpec' shall conform to the 'DataType' of the 'Member' of the 'MemberAssignment'."
  }

  //Restricted use of 'OmitValue' for optional 'Member's only
  constraint OmitValueUse {
    check:     (self.memberSpec.oclIsTypeOf(OmitValue) or self.memberSpec.oclIsTypeOf(AnyValueOrOmit))
          implies self.member.isOptional = true
    message:   self.prefix() + 
               "A non-optional 'Member' shall have a 'DataUse' specification assigned to it that is different from 'OmitValue' and 'AnyValueOrOmit'."
  }

  //Static data use in 'memberSpec' 
  constraint StaticDataInMemberSpec {
    check:     self.memberSpec.isEffectivelyStatic()
    message:   self.prefix() + 
               "The 'memberSpec' and all of its 'ParameterBinding's shall be effectively static. "
  }

  //[Figure 6.4: Collection data]
}

context CollectionDataType {
  //No multidimensional collections
  constraint NoMultidimensionalCollections {
    check:     not self.itemType.oclIsKindOf(CollectionDataType)
    message:   self.prefix() + 
               "The 'itemType' shall not be an instance of 'CollectionDataType'. "
  }

}

context CollectionDataInstance {
  //CollectionDataInstance shall refer to CollectionDataType
  constraint  CollectionDataInstanceType {
    check:     self.dataType.oclIsKindOf(CollectionDataType)
    message:   self.prefix() + 
               "The inherited reference 'dataType' from 'DataInstance' shall refer to instances of 'CollectionDataType' solely."
  }

  //Type of items in the 'CollectionDataInstance'
  constraint CollectionDataInstanceItemType {
    check:     self.item.forAll(i | 
              i.resolveDataType().conformsTo(self.dataType.oclAsType(CollectionDataType).itemType))
    message:   self.prefix() + 
               "The items in 'CollectionDataInstance' shall conform to the 'itemType' of the 'CollectionDataType' that is defined as the 'dataType' of this 'CollectionDataInstance'. "
  }

  //Static data use in 'item' 
  constraint StaticDataInItem {
    check:     self.item.forAll(i | i.isEffectivelyStatic())
    message:   self.prefix() + 
               "The DataUse's in 'item' and all of the respective 'ParameterBinding's shall be effectively static. "
  }

  //Length constraint of the 'CollectionDataInstance'
  constraint CollectionDataInstanceLengthConstraint {
    check:     true //This constraint cannot be expressed formally.
    message:   self.prefix() + 
               "If the 'dataType' 'CollectionType' contains the predefined constraint 'length' then the length of this 'CollectionDataInstance' shall be equal to the 'quantifier' of that 'Constraint'."
  }

  //[Figure 6.5: Procedure and procedure parameter]
}

context ProcedureSignature {
  //[There are no constraints specified.]
}

context ProcedureParameter {
  //[There are no constraints specified.]
}

context ParameterKind {
  //[There are no constraints specified.]
  //[Figure 6.6: Action, function, parameter and variable]
}

context Parameter {
  //[There are no constraints specified.]
}

context FormalParameter {
  //[There are no constraints specified.]
}

context Variable {
  //[There are no constraints specified.]
}

context Action {
  //[There are no constraints specified.]
}

context Function {
  //[There are no constraints specified.]
}

context UnassignedMemberTreatment {
  //[There are no constraints specified.]
}

context PredefinedFunction {
  //[There are no constraints specified.]
}

context EnumDataType {
  //SimpleDataInstance container in EnumDataType
  constraint  EnumDataInstanceContainment {
    check:     OclInvalid
    message:   self.prefix() + 
               "A 'SimpleDataInstance' whose 'dataType' property refers to an 'EnumDataType' shall be contained in that 'EnumDataType'."
  }

  //No extensions for EnumDataType
  constraint  EnumDataTypeExtensions {
    check:     OclInvalid
    message:   self.prefix() + 
               "The 'extension' property of an 'EnumDataType' shall be empty."
  }

}

context DataUse {
  //Occurrence of 'argument' and 'reduction'
  constraint ArgumentReductionLists {
    check:     self.argument.isEmpty() or self.reduction.isEmpty() or self.oclIsTypeOf(FunctionCall)
    message:   self.prefix() + 
               "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."
  }

  //Structured data types in 'reduction' set
  constraint ReductionMembers {
    check:     not self.resolveDataType().isKindOf(StructuredDataType)
      or self.reduction->isEmpty()
      or self.resolveDataType().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.isKindOf(StructuredDataType)
          and self.reduction->at(self.reduction->indexOf(m)-1).member.dataType.allMembers()
      ->includes(m.member))
    message:   self.prefix() + 
               "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'."
  }

  //No member with collection index in the first element in reduction
  constraint FirstReduction {
    check:     self.reduction->first().member.oclIsUndefined() or self.reduction->first().collectionIndex.oclIsUndefined()
    message:   self.prefix() + 
               "The first 'MemberReference' in reduction shall not specify both member and collectionIndex. "
  }

}

context ParameterBinding {
  //Matching data type
  constraint ParameterBindingTypes {
    check:     self.dataUse.resolveDataType().conformsTo(self.parameter.dataType)
    message:   self.prefix() + 
               "The provided 'DataUse' shall conform to the 'DataType' of the referenced 'Parameter'."
  }

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

}

context MemberReference {
  //Collection index expressions for collections only
  constraint CollectioinIndex {
    check:     self.collectionIndex.oclIsUndefined()
              or self.container().oclAsType(DataUse).resolveDataType().oclIsKindOf(CollectionDataType)
    message:   self.prefix() + 
               "If the type of the related 'DataUse' is not 'CollectionDataType' then the collectionIndex shall be undefined. "
  }

  //Either member or collection index is required
  constraint MemberOrReduction {
    check:     not self.member.oclIsUndefined() or not self.collectionIndex.oclIsUndefined()
    message:   self.prefix() + 
               "Either the member or collectionIndex shall be specified. "
  }

}

context StaticDataUse {
  //[There are no constraints specified.]
}

context DataInstanceUse {
  //'DataInstance' reference or non-empty 'argument' or non-empty 'item'
  constraint DataInstanceOrArgumentsOrItems {
    check:     not self.dataInstance.oclIsUndefined() or not self.argument->isEmpty() or not self.item->isEmpty()
    message:   self.prefix() + 
               "If a 'dataInstance' is not specified, either a non-empty 'argument' set or a non-empty 'item' set shall be specified."
  }

  //Valid 'DataType' for items
  constraint DataTypeOfItemsInDataInstance {
    check:     self.item.forAll(i | i.resolveDataType().conformsTo(self.resolveDataType().oclAsType(CollectionDataType).itemType))
    message:   self.prefix() + 
               "The items in the 'item' property shall conform to the 'itemType' of the resolved 'CollectionDataType'."
  }

  //No 'item' if 'dataInstance' is specified
  constraint NoItemWithDataInstance {
    check:     not self.dataInstance.oclIsUndefined() and self.item->isEmpty()
    message:   self.prefix() + 
               "The 'item' property shall be empty if the 'dataInstance' property is specified."
  }

}

context SpecialValueUse {
  //Empty 'argument' and 'reduction' sets
  constraint SpecialValueArgumentReduction {
    check:     self.reduction->isEmpty() and self.argument->isEmpty()
    message:   self.prefix() + 
               "The 'argument' and 'reduction' sets shall be empty."
  }

}

context AnyValue {
  //[There are no constraints specified.]
}

context AnyValueOrOmit {
  //[There are no constraints specified.]
}

context OmitValue {
  //[There are no constraints specified.]
  //[Figure 6.8: Dynamic data use]
}

context DynamicDataUse {
  //[There are no constraints specified.]
}

context FunctionCall {
  //Matching parameters
  constraint FunctionCallParameters {
    check:     self.`function`.formalParameter->forAll(p | self.argument->exists(a | a.parameter = p))
    message:   self.prefix() + 
               "All 'FormalParameter's of the invoked 'Function' shall be bound."
  }

}

context FormalParameterUse {
  //[There are no constraints specified.]
}

context VariableUse {
  //Local variables of tester components only
  constraint VariableUseComponentRole {
    check:     self.componentInstance.type.allVariables()->includes(self.variable)  
          and self.componentInstance.role = ComponentInstanceRole::Tester
    message:   self.prefix() + 
               "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'."
  }

}

context PredefinedFunctionCall {
  //Compatible actual parameters
  constraint PredefinedFunctionCallParameters {
    check:     true //This constraint cannot be expressed formally.
    message:   self.prefix() + 
               "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'."
  }

  //Empty 'argument' and 'reduction' sets
  constraint PredefinedFunctionCallArgumentReduction {
    check:     self.reduction->isEmpty() and self.argument->isEmpty()
    message:   self.prefix() + 
               "The 'argument' and 'reduction' sets shall be empty."
  }

}

context LiteralValueUse {
  //Exactly one value specification
  constraint SpecifiedLiteralValue {
    check:     not self.value.oclIsUndefined() 
          xor not self.intValue.oclIsUndefined() 
          xor not self.boolValue.oclIsUndefined()
    message:   self.prefix() + 
               "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."
  }

  //Empty 'argument' and 'reduction' sets if not 'dataType'
  constraint LiteralValueArgumentReduction {
    check:     (self.dataType.oclIsUndefined()) 
              implies (self.reduction->isEmpty() and self.argument->isEmpty())
    message:   self.prefix() + 
               "If 'dataType' is not specified then the 'argument' and 'reduction' sets shall be empty."
  }

  //Integer type for integer value
  constraint LiteralValueIntType {
    check:     not self.intValue.oclIsUndefined() 
          implies (self.dataType.oclIsUndefined() or self.dataType.conformsTo('Integer'))
    message:   self.prefix() + 
               "If 'intValue' is specified then the 'dataType' is either unspecified or the specified 'DataType' conforms to predefined type 'Integer'."
  }

  //Boolean type for Boolean value
  constraint LiteralValueBoolType {
    check:     not self.intValue.oclIsUndefined() 
          implies (self.dataType.oclIsUndefined() or self.dataType.conformsTo('Boolean'))
    message:   self.prefix() + 
               "If 'boolValue' is specified then the 'dataType' is either unspecified or the specified 'DataType' conforms to predefined type 'Boolean'."
  }

}

context DataElementUse {
  //'DataElement' reference or non-empty 'argument' or non-empty 'item'
  constraint DataInstanceOrArgumentsOrItemsInDataElementUse {
    check:     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())
    message:   self.prefix() + 
               "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."
  }

  //Valid 'DataType' for items
  constraint DataTypeOfItemsInDataInstance {
    check:     self.item.forAll(i | i.resolveDataType().conformsTo(self.resolveDataType().oclAsType(CollectionDataType).itemType))
    message:   self.prefix() + 
               "The items in the 'item' property shall conform to the 'itemType' of the resolved 'CollectionDataType'."
  }

  //Only 'item' if the resolved data type is 'CollectionDataType'
  constraint ItemOnlyWithCollectionDataType {
    check:     ((self.dataElement.oclIsKindOf(CollectionDataType))
      or self.dataElement.oclIsUndefined())
      and not self.item->isEmpty())
      or self.item->isEmpty()
    message:   self.prefix() + 
               "The 'item' property shall be non-empty if the 'dataElement' property is resolved to a 'CollectionDataType'."
  }

  //Matching parameters for 'Function's
  constraint FunctionCallParameters {
    check:     not self.dataElement.oclIsKindOf(Function)
      or self.dataElement.oclAsType(Function).formalParameter->forAll(p | self.argument->exists(a | a.parameter = p))
    message:   self.prefix() + 
               "All 'FormalParameter's shall be bound if the 'dataElement' refers to a a 'Function'."
  }

}

context Time {
  //[There are no constraints specified.]
}

context TimeLabel {
  //[There are no constraints specified.]
}

context TimeLabelUse {
  //Empty 'argument' and 'reduction' sets
  constraint TimeLabelArgumentReduction {
    check:     self.reduction->isEmpty() and self.argument->isEmpty()
    message:   self.prefix() + 
               "The 'argument' and 'reduction' sets shall be empty."
  }

  //'TimeLabel's only within the same 'TestDescription' when local ordering is used 
  constraint TimeLabelLocallyOrdered {
    check:     self.getParentTestDescription.isLocallyOrdered = true
      or self.timeLabel.getParentTestDescription() = self.getParentTestDescription()
    message:   self.prefix() + 
               "When local ordering is used, 'TimeLabel's shall only be used within the same test description. "
  }

}

context TimeLabelUseKind {
  //[There are no constraints specified.]
}

context TimeConstraint {
  //Time constraint expression of type Boolean
  constraint TimeConstraintType {
    check:     self.timeConstraintExpression.resolveDataType().name = 'Boolean'
    message:   self.prefix() + 
               "The expression given in the 'DataUse' specification shall evaluate to predefined type 'Boolean'."
  }

  //Use of local variables only
  constraint TimeConstraintVariables {
    check:     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().getParticipatingComponents().includes(
                  du.oclAsType(VariableUse).componentInstance))
    message:   self.prefix() + 
               "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'."
  }

  //Use of local time labels only
  constraint TimeConstraintTimeLabels {
    check:     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().getParticipatingComponents().includesAll(
                  du.oclAsType(TimeLabelUse).timeLabel.container().getParticipatingComponents()))
    message:   self.prefix() + 
               "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."
  }

  //[Figure 7.2: Time operations]
}

context TimeOperation {
  //Component required in locally ordered test description
  constraint TimeOperationComponent {
    check:     self.getParentTestDescription.isLocallyOrdered 
          implies not self.componentInstance.oclIsUndefined()
    message:   self.prefix() + 
               "If the 'TimeOperation' is contained in a locally ordered 'TestDescription' then the 'componentInstance' shall be specified."
  }

  //Time operations on tester components only
  constraint TimeOperationComponentRole {
    check:     (not self.componentInstance.oclIsUndefined()
           and self.componentInstance.role = ComponentInstanceRole::Tester)
      or (self.oclIsTypeOf(Quiescence)
           and not self.gateReference.oclIsUndefined()
           and self.gateReference.component.role.name = ComponentInstanceRole::Tester)
    message:   self.prefix() + 
               "A 'TimeOperation' shall be performed only on a 'ComponentInstance' in the role 'Tester'."
  }

  //'Time' data type for period expression
  constraint TimePeriodType {
    check:     self.period.resolveDataType().oclIsKindOf(Time)
    message:   self.prefix() + 
               "The 'DataUse' expression assigned to the 'period' shall evaluate to a data instance of the 'Time' data type."
  }

}

context Wait {
  //[There are no constraints specified.]
}

context Quiescence {
  //Exclusive use of gate reference or component instance
  constraint QuiescenceTarget {
    check:     self.gateReference.oclIsUndefined() xor self.componentInstance.oclIsUndefined()
    message:   self.prefix() + 
               "If a 'GateReference' is provided, a 'ComponentInstance' shall not be provided and vice versa."
  }

  //[Figure 7.3: Timer and timer operations]
}

context Timer {
  //[There are no constraints specified.]
}

context TimerOperation {
  //Timer operations on tester components only
  constraint TimerOperationComponentRole {
    check:     self.componentInstance.role = ComponentInstanceRole::Tester
    message:   self.prefix() + 
               "A 'TimerOperation' shall be performed only on a 'ComponentInstance' in the role 'Tester'."
  }

}

context TimerStart {
  //'Time' data type for period expression
  constraint TimerPeriodType {
    check:     self.period.resolveDataType().oclIsKindOf(Time)
    message:   self.prefix() + 
               "The 'DataUse' expression assigned to the 'period' shall evaluate to a data instance of the 'Time' data type."
  }

}

context TimerStop {
  //[There are no constraints specified.]
}

context TimeOut {
  //[There are no constraints specified.]
}

context GateType {
  //Compatible 'DataType's. 
  constraint GateType {
    check:     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))
    message:   self.prefix() + 
               "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. "
  }

}

context GateTypeKind {
  //[There are no constraints specified.]
}

context GateInstance {
  //[There are no constraints specified.]
}

context ComponentType {
  //[There are no constraints specified.]
  //[Figure 8.2: Test configuration]
}

context ComponentInstance {
  //[There are no constraints specified.]
}

context ComponentInstanceRole {
  //[There are no constraints specified.]
}

context GateReference {
  //Gate instance of the referred component instance
  constraint GateInstanceReference {
    check:     self.component.type.allGates()->includes(self.gate)
    message:   self.prefix() + 
               "The referred 'GateInstance' shall be contained in the 'ComponentType' of the referred 'ComponentInstance'."
  }

}

context Connection {
  //Self-loop connections are not permitted
  constraint NoSelfLoop {
    check:     self.endPoint->forAll(e1 | self.endPoint->one(e2 | e1.gate = e2.gate
              and e1.component = e2.component))
    message:   self.prefix() + 
               "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."
  }

  //Consistent type of a connection
  constraint ConsistentConnectionType {
    check:     self.endPoint->at(0).gate.type = self.endPoint->at(1).gate.type
    message:   self.prefix() + 
               "The 'GateInstance's of the two 'endPoint's of a 'Connection' shall refer to the same 'GateType'."
  }

}

context TestConfiguration {
  //'TestConfiguration' and components roles
  constraint ComponentRoles {
    check:     self.componentInstance->exists(c | c.role = ComponentInstanceRole::Tester)
      and self.componentInstance->exists(c | c.role = ComponentInstanceRole::SUT)
    message:   self.prefix() + 
               "A 'TestConfiguration' shall contain at least one 'Tester' and one 'SUT' 'ComponentInstance'."
  }

  //Only 'Connection's between own 'ComponentInstance's 
  constraint OwnedComponents {
    check:     self.connection->forAll(c |
              self.componentInstance->includes(c.endPoint->at(0).component)
          and self.componentInstance->includes(c.endPoint->at(1).component))
    message:   self.prefix() + 
               "A 'TestConfiguration' shall only contain 'Connection's between gates of its own 'ComponentInstance's. "
  }

  //Minimal 'TestConfiguration'
  constraint MinimalTestConfiguration {
    check:     self.connection->exists(c |
              (c.endPoint->at(0).component.role = ComponentInstanceRole::Tester
           and c.endPoint->at(1).component.role = ComponentInstanceRole::SUT)    
           or (c.endPoint->at(0).component.role = ComponentInstanceRole::SUT
           and c.endPoint->at(1).component.role = ComponentInstanceRole::Tester))
    message:   self.prefix() + 
               "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'."
  }

  //At most one connection between any two 'GateInstance'/'ComponentInstance' pairs
  constraint UniqueConnections {
    check:     self.connection->forAll(c1 | self.connection->one(c2 |
              (c1.endPoint->at(0).component = c2.endPoint->at(0).component
           and c1.endPoint->at(0).gate = c2.endPoint->at(0).gate
           and c1.endPoint->at(1).component = c2.endPoint->at(1).component
           and c1.endPoint->at(1).gate = c2.endPoint->at(1).gate)
      
           or (c1.endPoint->at(1).component = c2.endPoint->at(0).component
           and c1.endPoint->at(1).gate = c2.endPoint->at(0).gate
           and c1.endPoint->at(0).component = c2.endPoint->at(1).component
           and c1.endPoint->at(0).gate = c2.endPoint->at(1).gate)))
    message:   self.prefix() + 
               "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'."
  }

}

context TestDescription {
  //[There are no constraints specified.]
}

context BehaviourDescription {
  //[There are no constraints specified.]
}

context Behaviour {
  //[There are no constraints specified.]
}

context Block {
  //Guard shall evaluate to Boolean
  constraint GuardType {
    check:     self.`guard`.oclIsUndefined() or self.`guard`.resolveDataType().name = 'Boolean'
    message:   self.prefix() + 
               "The type of 'guard' shall be 'Boolean'."
  }

  //No directly contained 'ExceptionalBehaviour's and 'PeriodicBehaviour's.
  constraint AllowedBehaviourTypes {
    check: self.behaviour.forAll(b |
         not b.oclIsTypeOf(ExceptionalBehaviour) and not b.oclIsTypeOf(PeriodicBehaviour))
    message:   self.prefix() + 
               "A 'Block' shall not contain 'ExceptionalBehaviour's and 'PeriodicBehaviour's."
  }

  //Guard for each participating tester in locally ordered test descriptions
  constraint GuardsForParticipatingComponents {
    check:     self.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT)
              ->forAll(c | self.`guard`->exists(ex | ex.componentInstance = c))
          or not self.getParentTestDescription().isLocallyOrdered
    message:   self.prefix() + 
               "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. "
  }

  //Single guard in totally ordered test description
  constraint SingleTotalGuard {
    check:     self.getParentTestDescription().isLocallyOrdered or self.`guard`->size() <= 1
    message:   self.prefix() + 
               "If the 'Block' is contained in a totally ordered 'TestDescription' then there shall not be more than one guard. "
  }

}

context LocalExpression {
  //Local expressions in locally ordered test descriptions have 'ComponentInstance' specified
  constraint LocalExpressionComponent {
    check:     self.getParentTestDescription().isLocallyOrdered 
          implies not self.componentInstance.oclIsUndefined()
    message:   self.prefix() + 
               "If the 'LocalExpression' is contained in a locally ordered 'TestDescription' then the componentInstance shall be specified. "
  }

  //Only local variables and time labels in case of locally ordered test description
  constraint LocalVariablesAndTimersInExpression {
    check:     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()
                  .getParticipatingComponents.includes(self.componentInstance))
    message:   self.prefix() + 
               "If the componentInstance is specified then all 'Variable's and 'TimeLabel's used in the expression shall be local to that 'ComponentInstance'."
  }

}

context CombinedBehaviour {
  //[There are no constraints specified.]
}

context SingleCombinedBehaviour {
  //[There are no constraints specified.]
}

context CompoundBehaviour {
  //[There are no constraints specified.]
}

context BoundedLoopBehaviour {
  //No guard constraint
  constraint BoundedGuard {
    check:     self.block.`guard`.oclIsUndefined()
    message:   self.prefix() + 
               "The 'Block' of a 'BoundedLoopBehaviour' shall not have a 'guard'."
  }

  //Iteration number shall be countable and positive
  constraint LoopIteration {
    check:     self.numIteration.forAll(e | e.expression.resolveDataType().conformsTo('Integer'))
    message:   self.prefix() + 
               "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."
  }

  //Iteration count in locally ordered test descriptions
  constraint  IterationCountsForParticipatingComponents {
    check:     self.block.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT)
              ->forAll(c | self.numIteration->exists(ex | ex.componentInstance = c))
          or not self.getParentTestDescription().isLocallyOrdered
    message:   self.prefix() + 
               "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'."
  }

  //Single numIteration in totally ordered test description
  constraint SingleTotalIterationCount {
    check:     self.getParentTestDescription().isLocallyOrdered or self.numIteration->size() = 1
    message:   self.prefix() + 
               "If the 'BoundedLoopBehaviour' is contained in a totally ordered 'TestDescription' then there shall be exactly  one numIteration."
  }

}

context UnboundedLoopBehaviour {
  //[There are no constraints specified.]
}

context OptionalBehaviour {
  //First 'AtomicBehaviour' in block allowed
  constraint OptionalBehaviourStart {
    check:     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)
    message:   self.prefix() + 
               "The block of an 'OptionalBehaviour' shall start with a tester-to-tester 'Interaction'. "
  }

  //No other testers except the participants of starting 'Interaction' within 'OptionalBehaviour' in locally ordered 'TestDescription'
  constraint OptionalBehaviourParticipation {
    check:     let initial = self.block.behaviour->first().oclAsTypeOf(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->first().target.targetGate.component
          in
          self.block.getParticipatingComponents()
              ->forAll(c | initialComponents->includes(c) or optionalTargets->includes(c))
          or not self.getParentTestDescription().isLocallyOrdered
    message:   self.prefix() + 
               "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'. "
  }

}

context MultipleCombinedBehaviour {
  //[There are no constraints specified.]
}

context AlternativeBehaviour {
  //Number of 'Block's
  constraint AlternativeBlockCount {
    check:     self.block->size() > 1
    message:   self.prefix() + 
               "An 'AlternativeBehaviour' shall contain at least two 'Block's. "
  }

  //First behaviour of 'Block's
  constraint FirstBlockBehaviour {
    check:     self.block->forAll(b | b.behaviour->first().isTesterInputEvent())
    message:   self.prefix() + 
               "Each block of an 'AlternativeBehaviour' shall start with a tester-input event. "
  }

  //Same component if locally ordered
  constraint AlternativeBlocksComponent {
    check:     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
    message:   self.prefix() + 
               "If the containing 'TestDescription' is locally ordered then all 'Block's shall start with a tester-input event of the same 'ComponentInstance'. "
  }

  //Tester participating in locally ordered case
  constraint AlternativeBehaviourParticipation {
    check:     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
    message:   self.prefix() + 
               "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. "
  }

  //OptionalBehaviour in locally ordered case
  constraint OptionalAlternativeBehaviour {
    check:     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)).block
              ->first().oclAsType(Interaction).sourceGate.component->forAll(c | c = targetComponent)
          or not self.getParentTestDescription().isLocallyOrdered
    message:   self.prefix() + 
               "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'. "
  }

}

context ConditionalBehaviour {
  //Guard for 'ConditionalBehaviour' with single block
  constraint ConditionalFirstGuard {
    check:     self.block->size() > 1 or not self.block->first().`guard`.oclIsUndefined()
    message:   self.prefix() + 
               "If there is only one 'Block' specified, it shall have a 'guard'."
  }

  //Possible else block for 'ConditionalBehaviour' with multiple blocks
  constraint ConditionalLastGuard {
    check:     self.block->size() = 1
      or self.block->forAll(b | b = self.block->last() or not b.`guard`.oclIsUndefined())
    message:   self.prefix() + 
               "All 'Block's specified, except the last one, shall have a 'guard'."
  }

}

context ParallelBehaviour {
  //Number of blocks in 'ParallelBehaviour'
  constraint ParallelBlockCount {
    check:     self.block->size() > 1
    message:   self.prefix() + 
               "There shall be at least two 'Block's specified."
  }

  //[Figure 9.3: Exceptional and periodic behaviour]
}

context ExceptionalBehaviour {
  //First 'AtomicBehaviour' in block allowed
  constraint FirstExceptionalBehaviour {
    check:     self.block.behaviour->first().isTesterInputEvent()
    message:   self.prefix() + 
               "The block of an 'ExceptionalBehaviour' shall start with a tester-input event."
  }

  //Guarded component shall be a 'Tester' component
  constraint ExceptionalGuardedComponent {
    check:     self.guardedComponent.oclIsUndefined() or self.guardedComponent.role = ComponentInstanceRole::Tester
    message:   self.prefix() + 
               "The 'guardedComponent' shall refer to a 'ComponentInstance' with the role of 'Tester'."
  }

  //Same component if locally ordered and guarded component present
  constraint ExceptionalGuardedandTargetComponent {
    check:     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
    message:   self.prefix() + 
               "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. "
  }

  //Tester participating in locally ordered case
  constraint ExceptionalBehaviourParticipation {
    check:     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
    message:   self.prefix() + 
               "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 . "
  }

  //OptionalBehaviour in locally ordered case
  constraint OptionalExceptionalBehaviour {
    check:     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)).block
              ->first().oclAsType(Interaction).sourceGate.component->forAll(c | c = targetComponent)
          or not self.getParentTestDescription().isLocallyOrdered
    message:   self.prefix() + 
               "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'. "
  }

}

context DefaultBehaviour {
  //[There are no constraints specified.]
}

context InterruptBehaviour {
  //[There are no constraints specified.]
}

context PeriodicBehaviour {
  //'Time' data type for period expression
  constraint PeriodType {
    check:     self.period.resolveDataType().oclIsKindOf(Time)
    message:   self.prefix() + 
               "The 'DataUse' expression assigned to the 'period' shall evaluate to a data instance of the 'Time' data type."
  }

  //Period for each tester in locally ordered test descriptions
  constraint PeriodForParticipatingComponents {
    check:     self.block.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT)
              ->forAll(c | self.period->exists(ex | ex.componentInstance = c))
          or not self.getParentTestDescription().isLocallyOrdered
    message:   self.prefix() + 
               "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'. "
  }

}

context AtomicBehaviour {
  //[There are no constraints specified.]
}

context Break {
  //Break in conditional behaviour only
  constraint ConditionalBreak {
    check:     self.container().container().oclIsKindOf(ConditionalBehaviour)
    message:   self.prefix() + 
               "A 'Break' shall be contained directly in the block of a 'ConditionalBehaviour'. "
  }

  //No behaviours after break
  constraint ConditionalBreak {
    check:     self.container().oclAsType(Block).behaviour->last() = self
    message:   self.prefix() + 
               "A 'Break' shall be the last behaviour in the containing 'Block'. "
  }

}

context Stop {
  //[There are no constraints specified.]
}

context VerdictAssignment {
  //Verdict of type 'Verdict'
  constraint VerdictType {
    check:     self.verdict.resolveDataType().name = 'Verdict'
    message:   self.prefix() + 
               "The 'verdict' shall evaluate to a, possibly predefined, instance of a 'SimpleDataInstance' of data type 'Verdict'."
  }

  //No 'SpecialValueUse'
  constraint VerdictNoSpecialValueUse {
    check:     not self.verdict.oclIsKindOf(SpecialValueUse)
    message:   self.prefix() + 
               "The 'verdict' shall not evaluate to an instance of a 'SpecialValueUse'."
  }

}

context Assertion {
  //Boolean condition
  constraint AssertionOtherwise {
    check:     self.condition.resolveDataType().name = 'Boolean'
    message:   self.prefix() + 
               "The 'condition' shall evaluate to predefined 'DataType' 'Boolean'."
  }

  //Otherwise of type 'Verdict'
  constraint AssertionVerdict {
    check:     self.otherwise.oclIsUndefined() or self.otherwise.resolveDataType().name = 'Verdict'
    message:   self.prefix() + 
               "The 'otherwise' shall evaluate to a, possibly predefined, instance of a 'SimpleDataInstance' of data type 'Verdict'."
  }

  //No 'SpecialValueUse'
  constraint AssertionNoSpecialValueUse {
    check:     not self.otherwise.oclIsKindOf(SpecialValueUse)
    message:   self.prefix() + 
               "The 'otherwise' shall not evaluate to an instance of a 'SpecialValueUse'."
  }

  //[Figure 9.5: Interaction behaviour]
}

context Interaction {
  //Gate references of an interaction shall be connected
  constraint ConnectedInteractionGates {
    check:     self.target.forAll(t |
              self.getParentTestDescription().testConfiguration.connection->exists(c |
                  (c.endPoint->at(0).gate = self.sourceGate.gate
               and c.endPoint->at(0).component = self.sourceGate.component
               and c.endPoint->at(1).gate = t.targetGate.gate
               and c.endPoint->at(1).component = t.targetGate.component)
      
               or (c.endPoint->at(1).gate = self.sourceGate.gate
               and c.endPoint->at(1).component = self.sourceGate.component
               and c.endPoint->at(0).gate = t.targetGate.gate
               and c.endPoint->at(0).component = t.targetGate.component)))
    message:   self.prefix() + 
               "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'."
  }

}

context Message {
  //'DataType' resolvable
  constraint DataTypeResolvable {
    check:     not self.argument.oclIsUndefined()
    message:   self.prefix() + 
               "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."
  }

  //Type of message argument
  constraint MessageArgumentAndGateType {
    check:     (self.argument.oclIsKindOf(AnyValue)
      and self.argument.dataType.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))))
    message:   self.prefix() + 
               "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'."
  }

  //Use of variables in the 'argument' specification
  constraint MessageArgumentVariableUse {
    check:     (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)))
    message:   self.prefix() + 
               "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."
  }

  //Conforming data type for 'argument' and 'variable'
  constraint MessageArgumentAndVariableType {
    check:     self.target.forAll(t | t.variable.oclIsUndefined()
              or not self.argument.resolveDataType().oclIsUndefined()
           and self.argument.resolveDataType().conformsTo(t.variable.dataType))
    message:   self.prefix() + 
               "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."
  }

}

context ProcedureCall {
  //Only point-to-point procedure calls
  constraint ProcedureCallTargetCount {
    check:     self.target->size() = 1
    message:   self.prefix() + 
               "The 'target' of 'ProcedureCall' shall contain exactly one 'Target'. "
  }

  //Each call has a reply
  constraint ProcedureCallHasReply {
    check:     ProcedureCall.allInstances()->exists(pc | pc.replyTo = self)
    message:   self.prefix() + 
               "For every 'ProcedureCall' with empty 'replyTo' there shall be one or more 'ProcedureCall's that have this 'ProcedureCall' as 'replyTo'. "
  }

  //Call and reply within the same 'TestDescription'
  constraint ProcedureCallHasReply {
    check:     self.replyTo.oclIsUndefined() 
          or self.replyTo.getTestDescription() = self.getTestDescription()
    message:   self.prefix() + 
               "The 'ProcedureCall' referenced in the 'replyTo' shall be within the same 'TestDescription' as this 'ProcedureCall'. "
  }

  //Call and reply between same components
  constraint ProcedureCallReplyGates {
    check:     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))
    message:   self.prefix() + 
               "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. "
  }

  //Synchronous procedure calls
  constraint ProcedureCallSynchronousCalling {
    check:     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))
    message:   self.prefix() + 
               "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'. "
  }

  //Type of procedure call
  constraint ProcedureCallSignatureInGateTypes {
    check:     self.sourceGate.gate.type.allDataTypes()->includes(self.signature)
          and self.target->forAll(targetGate.gate.type.allDataTypes()->includes(self.signature))
    message:   self.prefix() + 
               "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'. "
  }

  //No mixing of parameters
  constraint ProcedureParameterKind {
    check:     self.argument->collect(pb | pb.parameter.oclAsType(ProcedureParameter).kind)
              ->asSet()->size() <= 1
    message:   self.prefix() + 
               "All 'ParameterBinding's specified in the 'argument' shall refer to 'ProcedureParameter's of the same 'ParameterKind'. "
  }

  //Matching procedure arguments
  constraint ProcedureCallArguments {
    check:     (self.replyTo.oclIsUndefined() and self.signature.parameter->select(p | p.kind = ParameterKind::In)
              ->forAll(p | self.argument.parameter->includes(p)))
          or (not self.replyTo.oclIsUndefined() and self.signature.parameter->reject(p | p.kind = ParameterKind::In)
              ->forAll(p | self.argument.parameter->includes(p)))
    message:   self.prefix() + 
               "For a 'ProcedureCall' with empty 'replyTo' there shall be one 'ParameterBinding' instance in the 'argument' for each 'ProcedureParameter' with kind 'In' in the associated 'ProcedureSignature'. For a 'ProcedureCall' with 'replyTo' there shall be one 'ParameterBinding' instance in the 'argument' for each 'ProcedureParameter' with kind 'Out' or 'Exception' in the associated 'ProcedureSignature'. "
  }

  //Use of variables in the 'argument' specification
  constraint ProcedureCallVariableUse {
    check:     self.argument
              ->closure(pb | pb.dataUse.argument)->union(self.argument)->collect(pb | pb.dataUse)
              ->select(du | du.oclIsKindOf(VariableUse))
              ->forAll(du | self.getParticipatingComponents().includes(
                  du.oclAsType(VariableUse).componentInstance))
    message:   self.prefix() + 
               "The use of 'Variable's in the 'DataUse' specifications in 'ParameterBinding's shall be restricted to 'Variable's of 'ComponentInstance's that participate in this 'ProcedureCall' via the provided 'GateReference's. "
  }

  //Reply not starting event of exceptional behaviour
  constraint ProcedureCallReplyNotInExceptional {
    check:     self.replyTo.oclIsUndefined() or not self.container().container().oclIsKindOf(ExceptionalBehaviour)
    message:   self.prefix() + 
               "A 'ProcedureCall' that specifies replyTo shall not be the first behaviour of a block in an 'ExceptionalBehaviour'. "
  }

}

context Target {
  //Variable and target gate of the same component instance
  constraint TargetComponent {
    check:     self.valueAssignment->isEmpty()
      or self.targetGate.component.type.allVariables()->includesAll(self.valueAssignment.variable)
    message:   self.prefix() + 
               "The 'Variable's referenced by 'valueAssignment' shall exist in the same 'ComponentType' as the 'GateInstance' that is referred to by the 'GateReference' of the 'targetGate'."
  }

  //Variable of a tester component only
  constraint TargetVariableComponentRole {
    check:     self.valueAssignment->isEmpty () or self.targetGate.component.role = ComponentInstanceRole::Tester
    message:   self.prefix() + 
               "If a 'ValueAssignment' is specified, the 'ComponentInstance' referenced by 'targetGate' shall be in the role 'Tester'."
  }

}

context ValueAssignment {
  //Conforming data type for 'parameter' and 'variable'
  constraint AssignedParamterType {
    check:     self.parameter.oclIsUndefined() or self.parameter.dataType.conformsTo(self.variable.dataType)
    message:   self.prefix() + 
               "If the 'parameter' is specified then its type shall conform to the type of the 'variable'. "
  }

  //Parameter of associated procedure signature
  constraint AssignedProcedureParameter {
    check:     self.parameter.oclIsUndefined()
      or (self.container().container().oclIsKindOf(ProcedureCall) and
      self.container().container().oclAsType(ProcedureCall).signature.parameter->includes(self.parameter))
    message:   self.prefix() + 
               "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'."
  }

  //[Figure 9.6: Test description reference]
}

context TestDescriptionReference {
  //All test description parameters bound 
  constraint AllTestDescriptionParametersBound {
    check:       self.testDescription.formalParameter->forAll(p | self.argument->exists(a | a.parameter = p))
    message:   self.prefix() + 
               "For each 'FormalParameter' defined in 'formalParameter of' the referenced 'TestDescription' there shall be a 'ParameterBinding' in 'argument' that refers to that 'FormalParameter' in 'parameter'."
  }

  //No use of variables in arguments
  constraint NoVariablesInLocallyOrderedTestDescriptionReference {
    check:     self.argument.collect(pb | pb.dataUse).forAll(du |
              not du.oclIsKindOf(VariableUse)
          and du.argument->forAll(a | not a.dataUse.oclIsKindOf(VariableUse))
          and du.argument->closure(a | a.dataUse.argument)->forAll(a |
                  not a.dataUse.oclIsKindOf(VariableUse)))
    message:   self.prefix() + 
               "In locally ordered 'TestDescription's, 'DataUse' expressions used to describe arguments shall not contain variables directly or indirectly in 'TestDescriptionReference's."
  }

  //No use of time labels in arguments
  constraint NoTimeLabelsInLocallyOrderedTestDescriptionReference {
    check:     self.argument.collect(pb | pb.dataUse).forAll(du |
              not du.oclIsKindOf(TimeLabelUse)
          and du.argument->forAll(a | not a.dataUse.oclIsKindOf(TimeLabelUse))
          and du.argument->closure(a | a.dataUse.argument)->forAll(a |
                  not a.dataUse.oclIsKindOf(TimeLabelUse)))
    message:   self.prefix() + 
               "In locally ordered 'TestDescription's, 'DataUse' expressions used to describe arguments shall not contain time labels directly or indirectly in 'TestDescriptionReference's."
  }

  //Restriction to 1:1 component instance bindings
  constraint UniqueComponentBindings {
    check:     self.componentInstanceBinding->isEmpty()
      or self.componentInstanceBinding->forAll(b |
              self.componentInstanceBinding->one(c |
                  c.formalComponent = b.formalComponent or c.actualComponent = b.actualComponent))
    message:   self.prefix() + 
               "If component instance bindings are provided, the component instances referred to in the bindings shall occur at most once for the given test description reference."
  }

  //Compatible test configurations 
  constraint CompatibleConfiguration {
    check:     self.testDescription.testConfiguration.compatibleWith(
              self.getParentTestDescription().testConfiguration, self.componentInstanceBinding)
    message:   self.prefix() + 
               "The 'TestConfiguration' of the referenced (invoked) 'TestDescription' shall be compatible with the 'TestConfiguration' of the referencing (invoking) 'TestDescription' under the provided 'ComponentInstanceBinding's between the 'ComponentInstance's of the 'TestConfiguration's of referenced and referencing 'TestDescription's. "
  }

  //No combining of local and total ordering 
  constraint LocalAndTotalOrdering {
    check:     self.getParentTestDescription().isLocallyOrdered = self.testDescription.isLocallyOrdered
    message:   self.prefix() + 
               "The referenced 'TestDescription' shall have the same ordering assumption as the referencing 'TestDescription'."
  }

}

context ComponentInstanceBinding {
  //Conforming component types
  constraint BindingComponentTypes {
    check:     self.actualComponent.type.conformsTo(self.formalComponent.type)
    message:   self.prefix() + 
               "The 'ComponentType' of the actual 'ComponentInstance' shall conform to 'ComponentType' of the formal 'ComponentInstance."
  }

  //Matching component instance roles
  constraint BindingComponentRoles {
    check:     self.formalComponent.role = self.actualComponent.role
    message:   self.prefix() + 
               "Both, the formal and the actual component instances, shall have the same 'ComponentInstanceRole' assigned to."
  }

  //[Figure 9.7: Action behaviour concepts]
}

context ActionBehaviour {
  //'ActionBehaviour' on 'Tester' components only
  constraint ActionBehaviourComponentRole {
    check:     self.componentInstance.oclIsUndefined() or self.componentInstance.role = ComponentInstanceRole::Tester
    message:   self.prefix() + 
               "The 'ComponentInstance' that an 'ActionBehaviour' refers to shall be of role 'Tester'."
  }

  //Known 'componentInstance' with locally-ordered behaviour 
  constraint ActionBehaviourComponentInstance {
    check:     not self.componentInstance.oclIsUndefined() or not self.getParentTestDescription().isLocallyOrdered
    message:   self.prefix() + 
               "The 'ComponentInstance' that an 'ActionBehaviour' refers to shall be specified if the 'ActionBehaviour' is used within a locally-ordered 'TestDescription'."
  }

}

context ActionReference {
  //All action parameters bound 
  constraint AllActionParametersBound {
    check:     self.action.formalParameter->forAll(p | self.argument.parameter->includes(p))
    message:   self.prefix() + 
               "For each 'FormalParameter' defined in 'formalParameter of' the referenced 'Action' there shall be a 'ParameterBinding' in 'argument' that refers to that 'FormalParameter' in 'parameter'. "
  }

  //No 'Function's in 'ActionReference' 
  constraint ActionReferenceFunction {
    check:     not self.action.oclIsTypeOf(Function)
    message:   self.prefix() + 
               "The referenced 'Action' shall not be a 'Function'."
  }

}

context InlineAction {
  //[There are no constraints specified.]
}

context Assignment {
  //Conforming data type
  constraint AssignmentDataType {
    check:     self.expression.resolveDataType().conformsTo(self.variable.variable.dataType)
    message:   self.prefix() + 
               "The provided 'DataUse' expression shall conform to the 'DataType' of the referenced 'Variable'."
  }

  //Empty 'argument' set for 'variable'
  constraint AssignmentVariableArgument {
    check:     self.variable.argument->isEmpty()
    message:   self.prefix() + 
               "The 'argument' and 'reduction' sets shall be empty."
  }

}
