Fixing a bug in ConflictTracker.java

[jpf-core.git] / src / main / gov / nasa / jpf / listener / ConflictTracker.java

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index e99baedfedd8b5da74b2d0b92005559d7ce4851d..ca405b25dacf78abaec4f885cbef1ef0c7852956 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -90,20 +90,12 @@ public class ConflictTracker extends ListenerAdapter {
 
   boolean propagateTheChange(Node currentNode) {
        HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
-       HashSet<Node> parentSet = new HashSet<Node>();
 
        while(!changed.isEmpty()) {
                // Get the first element of HashSet and remove it from the changed set
                Node nodeToProcess = changed.iterator().next();
                changed.remove(nodeToProcess);
 
-               // Change the parent node
-               if (!currentNode.getSuccessors().contains(nodeToProcess)) {
-                       currentNode = parentSet.iterator().next();
-                       parentSet.remove(currentNode);
-               }
-                       
-
                // Update the edge
                boolean isChanged = updateEdge(currentNode, nodeToProcess);
 
@@ -113,10 +105,7 @@ public class ConflictTracker extends ListenerAdapter {
 
                // Checking if the out set has changed or not(Add its successors to the change list!)
                if (isChanged) {
-                       parentSet.add(nodeToProcess);
-                       for (Node i : nodeToProcess.getSuccessors()) {
-                               changed.add(i);
-                       }
+                       propagateTheChange(nodeToProcess);
                }
       }
 
@@ -129,6 +118,7 @@ public class ConflictTracker extends ListenerAdapter {
                         " to the variable: "+pair.getVarName()+" while App"+
                         writerMap.get(pair.getVarName())+" is overwriting the value: "
                         +valueMap.get(pair.getVarName())+" to the same variable!";
+       System.out.println(message);    
        return message;
   }
 
@@ -169,7 +159,6 @@ public class ConflictTracker extends ListenerAdapter {
                        Integer writer = writerMap.get(i.getVarName());
                        if ((value != null)&&(writer != null)) {
                                if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { // We have different values
-                                       System.out.println("we are here!!!!");
                                        errorMessage = createErrorMessage(i, valueMap, writerMap);
                                        return true;
                                }
@@ -184,9 +173,11 @@ public class ConflictTracker extends ListenerAdapter {
        ArrayList<NameValuePair> setSet = currentNode.getSetSetMap().get(parentNode);
        HashSet<String> updatedVarNames = new HashSet<String>();
        boolean isChanged = false;
-
-       for (int i = 0;i < setSet.size();i++) {
-               updatedVarNames.add(setSet.get(i).getVarName());
+       
+       if (setSet != null) {
+               for (int i = 0;i < setSet.size();i++) {
+                       updatedVarNames.add(setSet.get(i).getVarName());
+               }
        }
 
        for (NameValuePair i : parentNode.getOutSet()) {
@@ -194,8 +185,12 @@ public class ConflictTracker extends ListenerAdapter {
                        isChanged |= currentNode.getOutSet().add(i);
        }
 
-       for (int i = 0;i < setSet.size();i++) {
-               isChanged |= currentNode.getOutSet().add(setSet.get(i));
+       if (setSet != null) {
+               for (int i = 0;i < setSet.size();i++) {
+                       if (currentNode.getOutSet().contains(setSet.get(i)))
+                               currentNode.getOutSet().remove(setSet.get(i));
+                       isChanged |= currentNode.getOutSet().add(setSet.get(i));
+               }
        }
 
        return isChanged;
@@ -393,7 +388,7 @@ public class ConflictTracker extends ListenerAdapter {
 
     // Check for the conflict in this edge
     conflictFound = checkForConflict(currentNode);
-
+    
     // Check if the outSet of this state has changed, update all of its successors' sets if any
     if (isChanged)
        conflictFound = conflictFound || propagateTheChange(currentNode);
@@ -606,6 +601,7 @@ public class ConflictTracker extends ListenerAdapter {
       } else {
         if (executedInsn instanceof WriteInstruction) {
           String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
+
           for (String var : conflictSet) {
             if (varId.contains(var)) {
               // Get variable info