Commit 900da81f authored by Martti Käärik's avatar Martti Käärik
Browse files

Corrected AlternativeBehaviour constraints.

parent ed18f569
Loading
Loading
Loading
Loading
+24 −19
Original line number Original line Diff line number Diff line
@@ -695,30 +695,31 @@ context AlternativeBehaviour


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


  -- Same component if locally ordered
  -- 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()):
  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
        let initials = self.block->reject(b | b.behaviour->first()->isEmpty() or b.behaviour->first().oclIsKindOf(OptionalBehaviour)).behaviour->first()
          in
          Set{}
          Set{}
          ->including(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->union(initials->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->including(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          ->union(initials->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          -> including(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance)
          ->union(initials->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance)
          ->size() = 1 or not self.getParentTestDescription().isLocallyOrdered
          ->size() = 1 or not self.getParentTestDescription().isLocallyOrdered
  
  


  -- Tester participating in locally ordered case
  -- 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()):
  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(),
        let initials = self.block->reject(b | b.behaviour->first()->isEmpty() or b.behaviour->first().oclIsKindOf(OptionalBehaviour)).behaviour->first(),
          targetComponent = Set{}
          targetComponent = Set{}
          ->including(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->union(initials->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->including(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          ->union(initials->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          -> including(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance),
          -> union(initials->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance),
          nonOptionalBlocks = self.block->closure(
          nonOptionalBlocks = self.block->closure(
              b | b.behaviour->reject(oclIsKindOf(OptionalBehaviour))
              b | b.behaviour->reject(oclIsKindOf(OptionalBehaviour))
                  ->select(oclIsKindOf(SingleCombinedBehaviour)).oclAsType(SingleCombinedBehaviour).block
                  ->select(oclIsKindOf(SingleCombinedBehaviour)).oclAsType(SingleCombinedBehaviour).block
              ->union(b.behaviour->reject(oclIsKindOf(OptionalBehaviour))
              ->union(b.behaviour
                  ->select(oclIsKindOf(MultipleCombinedBehaviour)).oclAsType(MultipleCombinedBehaviour).block)
                  ->select(oclIsKindOf(MultipleCombinedBehaviour)).oclAsType(MultipleCombinedBehaviour).block)
          )
          )
          in
          in
@@ -729,14 +730,18 @@ context AlternativeBehaviour


  -- OptionalBehaviour in locally ordered case
  -- 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()):
  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(),
        let initials = self.block->reject(b | b.behaviour->first()->isEmpty() or b.behaviour->first().oclIsKindOf(OptionalBehaviour)).behaviour->first(),
          targetComponent = Set{}
          targetComponent = Set{}
          ->including(initial->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->union(initials->select(oclIsKindOf(Interaction)).oclAsType(Interaction).target.targetGate.component)
          ->including(initial->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          ->union(initials->select(oclIsKindOf(Quiescence)).oclAsType(Quiescence).componentInstance)
          -> including(initial->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance)
          -> union(initials->select(oclIsKindOf(TimeOut)).oclAsType(TimeOut).componentInstance),
          optionalBlocks = self.block->closure(
            b | b.behaviour->select(oclIsKindOf(SingleCombinedBehaviour)).oclAsType(SingleCombinedBehaviour).block
            ->union(b.behaviour->select(oclIsKindOf(MultipleCombinedBehaviour)).oclAsType(MultipleCombinedBehaviour).block)
          )->select(oclIsKindOf(OptionalBehaviour))
          in
          in
          self.block.behaviour->select(oclIsKindOf(OptionalBehaviour)) .oclAsType(OptionalBehaviour).block
            optionalBlocks->isEmpty()
              ->first().oclAsType(Interaction).sourceGate.component->forAll(c | targetComponent->includes(c))
            or optionalBlocks->first().oclAsType(Interaction).sourceGate.component->forAll(c | targetComponent->includes(c))
            or not self.getParentTestDescription().isLocallyOrdered
            or not self.getParentTestDescription().isLocallyOrdered