From 864a3e68f2b8d298da2bc397a5ff154c4ec587ec Mon Sep 17 00:00:00 2001 From: tempiaa <tempiaa@eurecom.fr> Date: Tue, 21 Jul 2020 16:59:04 +0200 Subject: [PATCH] Remove random loops from internal action loop verification --- .../modelchecker/SpecificationActionLoop.java | 27 +++++++++++++++++++ .../AvatarExpressionTest.java | 3 +++ 2 files changed, 30 insertions(+) diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java index 0bab01b859..128ede76c8 100644 --- a/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java +++ b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java @@ -3,6 +3,7 @@ package avatartranslator.modelchecker; import java.util.ArrayList; import java.util.HashMap; import java.util.HashSet; +import java.util.Iterator; import java.util.List; import java.util.Map; import java.util.Set; @@ -34,6 +35,13 @@ public class SpecificationActionLoop { public void init(AvatarSpecification spec) { Map<AvatarStateMachineElement, Set<AvatarTransition>> map = new HashMap<>(); + removeForLoops(); + + if (internalLoops.size() == 0) { + error = true; + return; + } + for (List<AvatarTransition> list : internalLoops) { AvatarStateMachineElement state = list.get(list.size() -1).getNext(0); //loop state for (AvatarTransition at : list) { @@ -94,6 +102,13 @@ public class SpecificationActionLoop { public void initLeadsTo(AvatarSpecification spec) { Set<AvatarStateMachineElement> stateSet = new HashSet<>(); + removeForLoops(); + + if (internalLoops.size() == 0) { + error = true; + return; + } + for (List<AvatarTransition> list : internalLoops) { for (AvatarTransition at : list) { stateSet.add(at.getNext(0)); @@ -229,6 +244,18 @@ public class SpecificationActionLoop { return s.toString(); } + private void removeForLoops() { + Iterator<ArrayList<AvatarTransition>> iter = internalLoops.iterator(); + while(iter.hasNext()) { + List<AvatarTransition> list = iter.next(); + if (list.size() == 1 && list.get(0).getName().startsWith("Transition2ForRandom__")) { + //remove random for cycle + iter.remove(); + } + } + } + + // public static void findIntersectionSets(List<ArrayList<AvatarTransition>> internalLoops) { // if (internalLoops == null || internalLoops.size() <= 1) { // return; diff --git a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java index 7a8aab6f28..bd13777cc9 100644 --- a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java +++ b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java @@ -126,12 +126,15 @@ public class AvatarExpressionTest { assertTrue(e9.buildExpression()); AvatarExpressionSolver e10 = new AvatarExpressionSolver("true && 0 >= 1 || false"); assertTrue(e10.buildExpression()); + AvatarExpressionSolver e11 = new AvatarExpressionSolver("8/2*(2+2)"); + assertTrue(e11.buildExpression()); assertTrue(e1.getResult() == 1); assertTrue(e2.getResult() == 1); assertTrue(e3.getResult() == 0); assertTrue(e5.getResult() == 1); assertTrue(e9.getResult() == 1); assertTrue(e10.getResult() == 0); + assertTrue(e11.getResult() == 16); } @Test -- GitLab