From e1366f95d8f9a1b026a255c6ed189bdb7d822485 Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Fri, 17 Jul 2020 11:54:05 +0200
Subject: [PATCH] Extended internal loops check for loops intersections
---
.../avatartranslator/AvatarSpecification.java | 25 +-
.../avatartranslator/AvatarStateMachine.java | 7 +-
.../modelchecker/AvatarModelChecker.java | 46 ++--
.../modelchecker/SpecificationActionLoop.java | 214 ++++++++++++++----
.../ui/window/JDialogUPPAALValidation.java | 10 +-
5 files changed, 219 insertions(+), 83 deletions(-)
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index d6b46e511c..532aa9ac1c 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -453,27 +453,6 @@ public class AvatarSpecification extends AvatarElement {
}
}
- public List<ArrayList<AvatarTransition>> checkStaticInternalLoops() {
- List<ArrayList<AvatarTransition>> loops = new ArrayList<ArrayList<AvatarTransition>>();
-
- //collect all the possible loops which do not contain signal communication
- for(AvatarBlock block: blocks) {
- block.getStateMachine().checkStaticInternalLoops(loops);
- }
-
- return loops;
-
-// //check presence of unguarded loops
-// for (ArrayList<AvatarTransition> trace : loops) {
-// boolean guarded = false;
-// for (AvatarTransition at : trace) {
-// guarded |= at.isGuarded();
-// }
-// if (!guarded) {
-// //no transition has a guard check --> reachability of first state
-// }
-// }
- }
//
// private void renameTimers() {
// // Check whether timers have the same name in different blocks
@@ -643,9 +622,9 @@ public class AvatarSpecification extends AvatarElement {
if (ancientGuard == null)
continue;
- //TraceManager.addDev("[[[[[[[[[[[[[[[ Guard before: " + ancientGuard.toString());
+ TraceManager.addDev("[[[[[[[[[[[[[[[ Guard before: " + ancientGuard.toString());
at.setGuard (ancientGuard.getRealGuard (asme));
- //TraceManager.addDev("]]]]]]]]]]]]]]] Guard after: " + at.getGuard().toString());
+ TraceManager.addDev("]]]]]]]]]]]]]]] Guard after: " + at.getGuard().toString());
}
}
}
diff --git a/src/main/java/avatartranslator/AvatarStateMachine.java b/src/main/java/avatartranslator/AvatarStateMachine.java
index 4c8b6310f3..8e2503ca02 100644
--- a/src/main/java/avatartranslator/AvatarStateMachine.java
+++ b/src/main/java/avatartranslator/AvatarStateMachine.java
@@ -1869,11 +1869,12 @@ public class AvatarStateMachine extends AvatarElement {
}
- public boolean checkStaticInternalLoops(List<ArrayList<AvatarTransition>> loops) {
+ public List<ArrayList<AvatarTransition>> checkStaticInternalLoops() {
if (allStates == null) {
- return false;
+ return null;
}
+ List<ArrayList<AvatarTransition>> loops = new ArrayList<ArrayList<AvatarTransition>>();
List<AvatarTransition> trace = new ArrayList<AvatarTransition>();
Set<AvatarStateMachineElement> visited= new HashSet<AvatarStateMachineElement>();
@@ -1881,7 +1882,7 @@ public class AvatarStateMachine extends AvatarElement {
checkStaticInternalLoopsRec(state, state, trace, visited, loops, 0);
visited.add(state); //avoid cycles permutations
}
- return true;
+ return loops;
}
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 1d79f836e4..84bbba7817 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -570,22 +570,44 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (studyAL) {
studySafety = true;
ignoreConcurrenceBetweenInternalActions = true;
- List<ArrayList<AvatarTransition>> internalLoops = spec.checkStaticInternalLoops();
- if (!internalLoops.isEmpty()) {
- actionLoops = new ArrayList<SpecificationActionLoop>();
- for (ArrayList<AvatarTransition> loop : internalLoops) {
- SpecificationActionLoop sap = new SpecificationActionLoop(loop, spec);
+ actionLoops = new ArrayList<SpecificationActionLoop>();
+ List<ArrayList<AvatarTransition>> internalLoops;
+ for(AvatarBlock block : spec.getListOfBlocks()) {
+ internalLoops = block.getStateMachine().checkStaticInternalLoops();
+ if (internalLoops != null && internalLoops.isEmpty() == false) {
+// for (ArrayList<AvatarTransition> loop : internalLoops) {
+// SpecificationActionLoop sap = new SpecificationActionLoop(loop, spec);
+// if (!sap.hasError()) {
+// actionLoops.add(sap);
+// safety = sap.getReachability();
+// startModelChecking(nbOfThreads);
+// resetModelChecking();
+// if (sap.hasProperty()) {
+// safety = sap.getProperty();
+// startModelChecking(nbOfThreads);
+// resetModelChecking();
+// }
+// sap.setResult();
+// }
+// }
+ SpecificationActionLoop sap = new SpecificationActionLoop(internalLoops, spec);
if (!sap.hasError()) {
actionLoops.add(sap);
- safety = sap.getReachability();
- startModelChecking(nbOfThreads);
- resetModelChecking();
- if (sap.hasProperty()) {
- safety = sap.getProperty();
+ do {
+ safety = sap.getReachability();
startModelChecking(nbOfThreads);
resetModelChecking();
- }
+ if (sap.hasProperty()) {
+ safety = sap.getProperty();
+ startModelChecking(nbOfThreads);
+ resetModelChecking();
+ }
+ if (sap.setCover()) {
+ break;
+ }
+ } while (sap.increasePointer());
sap.setResult();
+
}
}
}
@@ -833,8 +855,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
prepareTransitions();
prepareBlocks();
-
- spec.checkStaticInternalLoops();
nbOfThreads = Runtime.getRuntime().availableProcessors();
TraceManager.addDev("Starting the model checking with " + nbOfThreads + " threads");
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
index c5da755352..d49c6af052 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
@@ -1,53 +1,96 @@
package avatartranslator.modelchecker;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
import java.util.List;
+import java.util.Map;
+import java.util.Set;
import avatartranslator.AvatarBlock;
import avatartranslator.AvatarSpecification;
+import avatartranslator.AvatarStateMachineElement;
import avatartranslator.AvatarTransition;
public class SpecificationActionLoop {
- private List<AvatarTransition> path;
- private SafetyProperty reachability;
- private SafetyProperty property;
- private boolean hasProperty;
+ private List<ArrayList<AvatarTransition>> internalLoops;
+ private SafetyProperty [] reachabilities;
+ private SafetyProperty [] properties;
+ private AvatarStateMachineElement [] states;
+ private int [] cover; //0: non reachable; 1: reachable; 2: reachable with exit
private boolean result;
private boolean error;
+ private int pointer;
- public SpecificationActionLoop(List<AvatarTransition> path, AvatarSpecification spec) {
- this.path = path;
+
+ public SpecificationActionLoop(List<ArrayList<AvatarTransition>> paths, AvatarSpecification spec) {
+ //this.path = path;
this.error = false;
+ pointer = 0;
+ internalLoops = paths;
init(spec);
}
+
private void init(AvatarSpecification spec) {
- //check presence of unguarded loops
- boolean guarded = false;
- StringBuilder condition = new StringBuilder("!(");
- for (AvatarTransition at : path) {
- if (at.isGuarded()) {
- String guard = at.getGuard().toString().replaceAll("\\[", "").trim().replaceAll("\\]", "");
- if (guarded) {
- condition.append(" && " + guard);
+ Map<AvatarStateMachineElement, Set<AvatarTransition>> map = new HashMap<>();
+
+ for (List<AvatarTransition> list : internalLoops) {
+ AvatarStateMachineElement state = list.get(list.size() -1).getNext(0); //loop state
+ for (AvatarTransition at : list) {
+ if (map.containsKey(state)) {
+ map.get(state).add(at);
} else {
- condition.append(guard);
- }
- guarded = true;
+ Set<AvatarTransition> transitions = new HashSet<>();
+ transitions.add(at);
+ map.put(state, transitions);
+ }
+ state = at.getNext(0);
}
}
- condition.append(")");
- AvatarTransition at = path.get(path.size() - 1);
- //no transition has a guard check --> reachability of first state
- reachability = new SafetyProperty("E<> " + at.getBlock().getName() + "." + at.getNext(0).getName());
- reachability.analyzeProperty(spec);
- error = reachability.hasError();
- hasProperty = false;
- if (guarded) {
- hasProperty = true;
- property = new SafetyProperty("E<> " + at.getNext(0).getName() + " && " + condition.toString());
- property.analyzeProperty((AvatarBlock) at.getBlock(), spec);
- error |= property.hasError();
+
+ reachabilities = new SafetyProperty[map.keySet().size()];
+ properties = new SafetyProperty[map.keySet().size()];
+ states = new AvatarStateMachineElement[map.keySet().size()];
+ cover = new int[internalLoops.size()];
+
+ AvatarBlock block = (AvatarBlock) internalLoops.get(0).get(0).getBlock();
+
+ int i = 0;
+ for (AvatarStateMachineElement el : map.keySet()) {
+ Set<AvatarTransition> set = map.get(el);
+
+ states[i] = el;
+
+ SafetyProperty reachability = new SafetyProperty("E<> " + el.getName());
+ reachability.analyzeProperty(block, spec);
+ error |= reachability.hasError();
+ reachabilities[i] = reachability;
+
+ boolean guarded = false;
+ StringBuilder subCondition = new StringBuilder("!(");
+ for (AvatarTransition at : set) {
+ if (at.isGuarded()) {
+ String guard = at.getGuard().toString().replaceAll("\\[", "").trim().replaceAll("\\]", "");
+ if (guarded) {
+ subCondition.append(" || " + guard);
+ } else {
+ subCondition.append(guard);
+ }
+ guarded = true;
+ }
+ }
+ subCondition.append(")");
+ if (guarded) {
+ SafetyProperty property = new SafetyProperty("E<> " + el.getName() + " && " + subCondition.toString());
+ property.analyzeProperty(block, spec);
+ error |= property.hasError();
+ properties[i] = property;
+ }
+ i++;
}
+
+
}
public boolean hasError() {
@@ -55,21 +98,71 @@ public class SpecificationActionLoop {
}
public boolean hasProperty() {
- return hasProperty;
+ if (pointer < properties.length && reachabilities[pointer].result) {
+ return properties[pointer] != null;
+ }
+ return false;
}
public SafetyProperty getReachability() {
- return reachability;
+ if (pointer < reachabilities.length) {
+ return reachabilities[pointer];
+ }
+ return null;
}
public SafetyProperty getProperty() {
- return property;
+ if (pointer < properties.length && reachabilities[pointer].result) {
+ return properties[pointer];
+ }
+ return null;
+ }
+
+ public boolean increasePointer() {
+ if (pointer < states.length - 1) {
+ pointer++;
+ return true;
+ }
+ return false;
}
- public void setResult() {
- result = reachability.result;
- if (hasProperty) {
- result &= !property.result;
+ public boolean setCover() {
+ int i = 0;
+
+ if (reachabilities[pointer].result) {
+ AvatarStateMachineElement state = states[pointer];
+ for (List<AvatarTransition> list : internalLoops) {
+ if (cover[i] != 2) {
+ for (AvatarTransition at : list) {
+ if (at.getNext(0) == state) {
+ if (properties[pointer] != null && properties[pointer].result) {
+ cover[i] = 2;
+ } else {
+ cover[i] = 1;
+ }
+ break;
+ }
+ }
+ }
+ i++;
+ }
+ }
+
+ for (i = 0; i < internalLoops.size(); i++) {
+ if (cover[i] != 2) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ public void setResult() {
+ result = false;
+ for (int i = 0; i < internalLoops.size(); i++) {
+ if (cover[i] == 1) {
+ result = true;
+ break;
+ }
}
}
@@ -80,11 +173,54 @@ public class SpecificationActionLoop {
public String toString() {
StringBuilder s = new StringBuilder();
- s.append("In block " + path.get(path.size() - 1).getBlock().getName() + " : " + path.get(path.size() - 1).getNext(0).getName());
- for (AvatarTransition at : path) {
- s.append(" --> " + at.getNext(0).getName());
+ if(internalLoops == null) {
+ return "";
+ }
+
+ int i = 0;
+ for (List<AvatarTransition> list : internalLoops) {
+ if (cover[i] == 1) {
+ s.append("In block " + list.get(list.size() - 1).getBlock().getName() + " : " + list.get(list.size() - 1).getNext(0).getName());
+ for (AvatarTransition at : list) {
+ s.append(" --> " + at.getNext(0).getName());
+ }
+ }
+ i++;
+ s.append("\n");
}
return s.toString();
}
+
+// public static void findIntersectionSets(List<ArrayList<AvatarTransition>> internalLoops) {
+// if (internalLoops == null || internalLoops.size() <= 1) {
+// return;
+// }
+//
+// internalLoops.sort((x1, x2) -> {return x2.size() - x1.size();});
+//
+// Set<AvatarStateMachineElement> states = new HashSet<>();
+// Set<AvatarStateMachineElement> intersection = new HashSet<>();
+//
+// for (AvatarTransition at : internalLoops.get(0)) {
+// states.add(at.getNext(0));
+// }
+//
+// int i = 0;
+// for (List<AvatarTransition> list : internalLoops) {
+// if (i == 0) {
+// i++;
+// continue;
+// }
+// for (AvatarTransition at : list) {
+// if (states.contains(at.getNext(0))) {
+// intersection.add(at.getNext(0));
+// }
+// }
+// if (intersection.size() != 0) {
+// states = intersection;
+// intersection = new HashSet<>();
+// }
+// }
+// }
}
diff --git a/src/main/java/ui/window/JDialogUPPAALValidation.java b/src/main/java/ui/window/JDialogUPPAALValidation.java
index aee1119315..322db10b84 100644
--- a/src/main/java/ui/window/JDialogUPPAALValidation.java
+++ b/src/main/java/ui/window/JDialogUPPAALValidation.java
@@ -82,11 +82,11 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
"for UPPAALVerifierPath and UPPAALVerifierHost configurations.";
static {
- for (final String label : ConfigurationTTool.UPPAALPropertyVerifMessage.split(",")) {
- if (!label.trim().isEmpty()) {
- PROP_VERIFIED_LABELS.add(label.trim());
- }
- }
+// for (final String label : ConfigurationTTool.UPPAALPropertyVerifMessage.split(",")) {
+// if (!label.trim().isEmpty()) {
+// PROP_VERIFIED_LABELS.add(label.trim());
+// }
+// }
// Handle the case where nothing is defined in the configuration
if (PROP_VERIFIED_LABELS.isEmpty()) {
--
GitLab