Commit 45d3de63 authored by Martti Käärik's avatar Martti Käärik
Browse files

Convert OCL "let-in" blocks to "var" statement blocks for EVL.

parent fbc8bdd3
Loading
Loading
Loading
Loading
+14 −29
Original line number Diff line number Diff line
@@ -572,18 +572,10 @@ context TestConfiguration
  -- 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 |
           let c1_endPoints = c1.endPoint->asOrderedSet(),
                c2_endPoints = c2.endPoint->asOrderedSet()
           in
              (c1_endPoints->at(0).component = c2_endPoints->at(0).component
           and c1_endPoints->at(0).gate = c2_endPoints->at(0).gate
           and c1_endPoints->at(1).component = c2_endPoints->at(1).component
           and c1_endPoints->at(1).gate = c2_endPoints->at(1).gate)
      
           or (c1_endPoints->at(1).component = c2_endPoints->at(0).component
           and c1_endPoints->at(1).gate = c2_endPoints->at(0).gate
           and c1_endPoints->at(0).component = c2_endPoints->at(1).component
           and c1_endPoints->at(0).gate = c2_endPoints->at(1).gate)))
              not c1.endPoint->reject(ep1 | c2.endPoint->any(ep2 |
                  ep1.component = ep2.component and ep1.gate = ep2.gate
              ) = null)->isEmpty()
      ))
  


@@ -603,7 +595,7 @@ context Block
  -- 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.getParticipatingComponents()->reject(c | c.role = ComponentInstanceRole::SUT)
              ->forAll(c | self.guard->exists(ex | ex.componentInstance = c))
              ->forAll(c | self.guard->exists(ex | ex.scope = c))
          or not self.getParentTestDescription().isLocallyOrdered
  

@@ -618,7 +610,7 @@ 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()
          implies not self.scope.oclIsUndefined()
  

  -- Only local variables and time labels in case of locally ordered test description
@@ -628,14 +620,14 @@ context LocalExpression
              ->union(self.expression.argument)
              ->including(self.expression)
              ->select(du | du.oclIsKindOf(VariableUse))
              ->forAll(du | du.oclAsType(VariableUse).componentInstance = self.componentInstance)
              ->forAll(du | du.oclAsType(VariableUse).componentInstance = self.scope)
          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))
                  .getParticipatingComponents()->includes(self.scope))
  


@@ -654,7 +646,7 @@ context BoundedLoopBehaviour
  -- 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))
              ->forAll(c | self.numIteration->exists(ex | ex.scope = c))
          or not self.getParentTestDescription().isLocallyOrdered
  

@@ -837,7 +829,7 @@ context PeriodicBehaviour
  -- 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))
              ->forAll(c | self.period->exists(ex | ex.scope = c))
          or not self.getParentTestDescription().isLocallyOrdered
  

@@ -893,17 +885,10 @@ context Interaction
  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 |
              let c_endPoint = c.endPoint->asOrderedSet()
              in
                  (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)))
                  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()))
  


+30 −1
Original line number Diff line number Diff line
@@ -6,6 +6,9 @@ import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.StandardOpenOption;
import java.util.Arrays;
import java.util.Iterator;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

import org.etsi.mts.tdl.document.model.Content;
import org.etsi.mts.tdl.document.model.Document;
@@ -105,6 +108,8 @@ public class ConstraintExporter {
			return getEvlConstraint(cx);
	}
	
	Pattern letPattern = Pattern.compile("\\s*let(.+?)\\s*in\\s(.*)", Pattern.DOTALL);
	Pattern wsPattern = Pattern.compile("(\\s*)(.*)", Pattern.DOTALL);
	private String getEvlConstraint(Content cx) {
		String content = "context "
				+cx.getParent().getText()
@@ -141,9 +146,33 @@ public class ConstraintExporter {
				if (ocl.trim().startsWith("This")) {
					ocl = "    true"+" //"+ocl.trim();
				}

				Matcher m = letPattern.matcher(ocl);
				boolean isStatementBlock = false;
				if (m.matches()) {
					isStatementBlock = true;
					
					String vars = m.group(1);
					String expr = m.group(2);

					ocl = "{ ";
					String[] varDeclarations = vars.split(",");
					for (String v : varDeclarations) {
						// Not functional, just makes the output nicer
						Matcher wsm = wsPattern.matcher(v);
						if (wsm.matches())
							ocl += wsm.group(1) + "var " + wsm.group(2) + ";";
						else
							ocl += "var " + v + ";";
					}

					ocl += expr + ";";
					ocl += " }";
				}
				
				content+="  //"+title+"\n";
				content+="  constraint "+id + " {"+"\n";
				content+="    check: "+ocl+"\n";
				content+="    check" + (isStatementBlock ? " " : ": ") +ocl+"\n";
				content+="    message:   self.prefix() + \n"
						+"               \""+description+"\""+"\n";
				content+="  }\n"+"\n";