From 35dd3606413ad1d309d77d5779199d9423be01a2 Mon Sep 17 00:00:00 2001 From: amiraj Date: Thu, 12 Dec 2019 12:34:21 -0800 Subject: [PATCH] Fixing a bug in Conflict Tracker + Make propagate method much simpler --- .../nasa/jpf/listener/ConflictTracker.java | 95 ++++++------------- 1 file changed, 31 insertions(+), 64 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index 8b4e284..6977618 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -193,12 +193,10 @@ public class ConflictTracker extends ListenerAdapter { } boolean updateTheOutSet(Node parentNode, Node currentNode) { - HashMap> setSets = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap(); + Edge edge = parentNode.getOutgoingEdges().get(currentNode); + HashMap> setSets = edge.getSetSetMap(); HashSet updatedVarNames = new HashSet(); - Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode); - HashMap lastWriter = currentEdge.getLastWriter(); - HashMap lastValue = currentEdge.getLastValue(); - HashMap outSetVarMap = new HashMap(); + HashSet outSetVarMap = new HashSet(); boolean isChanged = false; for (Map.Entry mapElement : setSets.entrySet()) { @@ -210,30 +208,20 @@ public class ConflictTracker extends ListenerAdapter { } for (NameValuePair i : parentNode.getOutSet()) { - outSetVarMap.put(i.getVarName(), i.getAppNum()); + outSetVarMap.add(i.getVarName()); if (!updatedVarNames.contains(i.getVarName())) isChanged |= currentNode.getOutSet().add(i); } + ArrayList lastSetSet = setSets.get(edge.getFinalTransition()); - for (Map.Entry mapElement : setSets.entrySet()) { - ArrayList setSet = (ArrayList)mapElement.getValue(); - - for (int i = 0;i < setSet.size();i++) { - String varName = setSet.get(i).getVarName(); - Integer writer = lastWriter.get(varName); - String value = lastValue.get(varName); - - if (setSet.get(i).getAppNum().equals(writer) - && setSet.get(i).getValue().equals(value)) { - if (outSetVarMap.containsKey(varName)) { - Integer hashCode = outSetVarMap.get(varName).hashCode() * 31 + - varName.hashCode(); - currentNode.getOutSet().remove(hashCode); - } - isChanged |= currentNode.getOutSet().add(setSet.get(i)); - } + for (int i = 0;i < lastSetSet.size();i++) { + String var = lastSetSet.get(i).getVarName(); + + if (outSetVarMap.contains(var)) { + currentNode.getOutSet().remove(lastSetSet.get(i)); } + isChanged |= currentNode.getOutSet().add(lastSetSet.get(i)); } return isChanged; } @@ -241,32 +229,23 @@ public class ConflictTracker extends ListenerAdapter { void updateTheEdge(Node currentNode, Transition transition) { if (parentNode.getOutgoingEdges().containsKey(currentNode)) { Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode); - if (currentEdge.getSetSetMap().containsKey(transition)) { // Update the transition - if (manual) - currentEdge.getSetSetMap().put(transition, tempSetSet); - else - currentEdge.getSetSetMap().get(transition).addAll(tempSetSet); - } else { // Add a new transition - currentEdge.getSetSetMap().put(transition, tempSetSet); - } + if (currentEdge.getSetSetMap().containsKey(transition)) { // Update the transition + if (manual) + currentEdge.getSetSetMap().put(transition, tempSetSet); + else + currentEdge.getSetSetMap().get(transition).addAll(tempSetSet); + } else { // Add a new transition + currentEdge.getSetSetMap().put(transition, tempSetSet); + } + currentEdge.setFinalTransition(transition); } else { parentNode.getOutgoingEdges().put(currentNode, new Edge(parentNode, currentNode)); Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode); currentEdge.getSetSetMap().put(transition, tempSetSet); - } - - // Update the last writer and last value for this edge for each varName - Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode); - ArrayList setSet = currentEdge.getSetSetMap().get(transition); - for (int i = 0;i < setSet.size();i++) { - NameValuePair nameValuePair = setSet.get(i); - currentEdge.getLastWriter().put(nameValuePair.getVarName(), nameValuePair.getAppNum()); - currentEdge.getLastValue().put(nameValuePair.getVarName(), nameValuePair.getValue()); + currentEdge.setFinalTransition(transition); } } - - static class Node { Integer id; HashSet predecessors = new HashSet(); @@ -301,6 +280,7 @@ public class ConflictTracker extends ListenerAdapter { static class Edge { Node source, destination; + Transition finalTransition; HashMap lastWriter = new HashMap(); HashMap lastValue = new HashMap(); HashMap> setSetMap = new HashMap>(); @@ -318,6 +298,14 @@ public class ConflictTracker extends ListenerAdapter { return destination; } + Transition getFinalTransition() { + return finalTransition; + } + + void setFinalTransition(Transition transition) { + finalTransition = transition; + } + HashMap> getSetSetMap() { return setSetMap; } @@ -401,11 +389,6 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is restored to state with id: "+id+", depth: "+depth); - if (id == 24 && depth == 5) { - System.out.println("*****************************************"); - System.out.println("*****************************************"); - System.out.println("*****************************************"); - } // Update the parent node if (nodes.containsKey(id)) { parentNode = nodes.get(id); @@ -469,14 +452,7 @@ public class ConflictTracker extends ListenerAdapter { // Update the outset of the current node and check if it is changed or not to propagate the change boolean isChanged = updateTheOutSet(parentNode, currentNode); - - - System.out.println("######################### The outset is:"); - for (NameValuePair nvp : currentNode.getOutSet()) { - System.out.println("writer: "+nvp.getAppNum()); - System.out.println("value: "+nvp.getValue()); - System.out.println("var : "+nvp.getVarName()); - } + // Check if the outSet of this state has changed, update all of its successors' sets if any if (isChanged) conflictFound = conflictFound || checkAllSuccForConflict(currentNode) || propagateTheChange(currentNode); @@ -498,12 +474,6 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is backtracked to state with id: "+id+", depth: "+depth); - if (id == 24 && depth == 5) { - System.out.println("*****************************************"); - System.out.println("*****************************************"); - System.out.println("*****************************************"); - } - // Update the parent node if (nodes.containsKey(id)) { parentNode = nodes.get(id); @@ -709,9 +679,6 @@ public class ConflictTracker extends ListenerAdapter { if (getWriter(ti.getStack(), manualSet) != null) manual = true; - System.out.println("############################## writer: "+writer); - System.out.println("############################## value: "+value); - System.out.println("############################## var: "+var); // Update the temporary Set set. writeWriterAndValue(writer, value, var); } -- 2.34.1