From ce44d7ee5314f2802829236785e93f1ef85f6e00 Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Mon, 20 Jul 2020 17:50:47 +0200
Subject: [PATCH] General internal action loop detector using leadsTo pragmas
---
.../modelchecker/AvatarModelChecker.java | 67 ++++++++++++++-----
.../modelchecker/SpecificationActionLoop.java | 45 +++++++++++--
.../modelchecker/SpecificationState.java | 4 ++
3 files changed, 96 insertions(+), 20 deletions(-)
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 84bbba7817..cf467c079f 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -114,6 +114,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// Internal-action loop
private boolean studyActionLoop;
+ private int partialHash;
private ArrayList<SpecificationActionLoop> actionLoops;
//Debug counterexample
@@ -159,6 +160,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
freeIntermediateStateCoding = true;
verboseInfo = true;
compressionFactor = 1;
+ partialHash = -1;
}
public AvatarSpecification getInitialSpec() {
@@ -545,7 +547,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
iter.remove();
}
}
- System.out.println("Dimensions of lead states to elaborate: " + safetyLeadStates.size());
+// System.out.println("Dimensions of lead states to elaborate: " + safetyLeadStates.size());
safetyLeadStates = null;
}
if (!stoppedBeforeEnd) {
@@ -572,6 +574,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ignoreConcurrenceBetweenInternalActions = true;
actionLoops = new ArrayList<SpecificationActionLoop>();
List<ArrayList<AvatarTransition>> internalLoops;
+ int i = 0;
for(AvatarBlock block : spec.getListOfBlocks()) {
internalLoops = block.getStateMachine().checkStaticInternalLoops();
if (internalLoops != null && internalLoops.isEmpty() == false) {
@@ -590,28 +593,56 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// sap.setResult();
// }
// }
- SpecificationActionLoop sap = new SpecificationActionLoop(internalLoops, spec);
- if (!sap.hasError()) {
+ SpecificationActionLoop sap = new SpecificationActionLoop(internalLoops);
+// sap.init(spec);
+// if (!sap.hasError()) {
+// actionLoops.add(sap);
+// 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();
+//
+// }
+ sap.initLeadsTo(spec);
+ if(!sap.hasError()) {
actionLoops.add(sap);
- do {
- safety = sap.getReachability();
- startModelChecking(nbOfThreads);
+ safety = sap.getPropertyLeadsTo();
+ safetyLeadStates = Collections.synchronizedMap(new HashMap<Integer, SpecificationState>());
+ ignoreEmptyTransitions = false;
+ partialHash = i; //restrict the hashing to only the current block
+ startModelChecking(nbOfThreads);
+ partialHash = -1;
+ safety.initLead();
+ Iterator<Map.Entry<Integer,SpecificationState>> iter = safetyLeadStates.entrySet().iterator();
+ while (iter.hasNext()) {
+ SpecificationState state = iter.next().getValue();
resetModelChecking();
- if (sap.hasProperty()) {
- safety = sap.getProperty();
- startModelChecking(nbOfThreads);
- resetModelChecking();
- }
- if (sap.setCover()) {
+ startModelChecking(state, nbOfThreads);
+ if (safety.result == false) {
break;
+ } else {
+ //free memory
+ iter.remove();
}
- } while (sap.increasePointer());
- sap.setResult();
-
+ }
+ safetyLeadStates = null;
+ sap.setResultLeadsTo();
}
}
+ i++;
}
ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
+ ignoreEmptyTransitions = emptyTr;
studySafety = false;
}
@@ -2178,7 +2209,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (!ignoreConcurrenceBetweenInternalActions) {
state = reduceCombinatorialExplosionProperty(state);
}
- safetyLeadStates.put(state.getHash(state.getBlockValues()), state);
+ if (partialHash == -1) {
+ safetyLeadStates.put(state.getHash(state.getBlockValues()), state);
+ } else {
+ safetyLeadStates.put(state.getPartialHash(partialHash), state);
+ }
newState.property = false;
}
addToPending = 1;
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
index d49c6af052..0bab01b859 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
@@ -23,16 +23,15 @@ public class SpecificationActionLoop {
private int pointer;
- public SpecificationActionLoop(List<ArrayList<AvatarTransition>> paths, AvatarSpecification spec) {
+ public SpecificationActionLoop(List<ArrayList<AvatarTransition>> paths) {
//this.path = path;
this.error = false;
pointer = 0;
internalLoops = paths;
- init(spec);
}
- private void init(AvatarSpecification spec) {
+ public void init(AvatarSpecification spec) {
Map<AvatarStateMachineElement, Set<AvatarTransition>> map = new HashMap<>();
for (List<AvatarTransition> list : internalLoops) {
@@ -89,8 +88,36 @@ public class SpecificationActionLoop {
}
i++;
}
-
+ }
+
+
+ public void initLeadsTo(AvatarSpecification spec) {
+ Set<AvatarStateMachineElement> stateSet = new HashSet<>();
+
+ for (List<AvatarTransition> list : internalLoops) {
+ for (AvatarTransition at : list) {
+ stateSet.add(at.getNext(0));
+ }
+ }
+
+ properties = new SafetyProperty[1];
+
+ AvatarBlock block = (AvatarBlock) internalLoops.get(0).get(0).getBlock();
+
+ int i = 0;
+ StringBuilder formula = new StringBuilder();
+ for (AvatarStateMachineElement el : stateSet) {
+ if (i != 0) {
+ formula.append("||");
+ }
+ formula.append(el.getName());
+ i++;
+ }
+ SafetyProperty property = new SafetyProperty(formula.toString() + "-->!(" + formula.toString() + ")");
+ property.analyzeProperty(block, spec);
+ error |= property.hasError();
+ properties[0] = property;
}
public boolean hasError() {
@@ -118,6 +145,10 @@ public class SpecificationActionLoop {
return null;
}
+ public SafetyProperty getPropertyLeadsTo() {
+ return properties[0];
+ }
+
public boolean increasePointer() {
if (pointer < states.length - 1) {
pointer++;
@@ -166,6 +197,10 @@ public class SpecificationActionLoop {
}
}
+ public void setResultLeadsTo() {
+ result = !properties[0].result;
+ }
+
public boolean getResult() {
return result;
}
@@ -175,6 +210,8 @@ public class SpecificationActionLoop {
if(internalLoops == null) {
return "";
+ } else if (cover == null) {
+ return "In block " + internalLoops.get(0).get(0).getBlock().getName();
}
int i = 0;
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationState.java b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
index 2d4533bad7..05d53ec188 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationState.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
@@ -95,6 +95,10 @@ public class SpecificationState implements Comparable<SpecificationState> {
}
return hashValue;
}
+
+ public int getPartialHash(int index) {
+ return Arrays.hashCode(blocks[index].values);
+ }
public void setInit(AvatarSpecification _spec, boolean _ignoreEmptyTransitions) {
int cpt = 0;
--
GitLab