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 fa940012e2194e18587fdd5b143f5a87bee7762b..ca405b25dacf78abaec4f885cbef1ef0c7852956 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -100,15 +100,12 @@ public class ConflictTracker extends ListenerAdapter {
                boolean isChanged = updateEdge(currentNode, nodeToProcess);
 
                // Check for a conflict in this transition(currentNode -> nodeToProcess)
-               if (checkForConflict(currentNode))
+               if (checkForConflict(nodeToProcess))
                                return true;
 
                // Checking if the out set has changed or not(Add its successors to the change list!)
                if (isChanged) {
-                       for (Node i : nodeToProcess.getSuccessors()) {
-                               if (!changed.contains(i))
-                                       changed.add(i);
-                       }
+                       propagateTheChange(nodeToProcess);
                }
       }
 
@@ -121,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;
   }
 
@@ -128,7 +126,6 @@ public class ConflictTracker extends ListenerAdapter {
        HashMap<String, String> valueMap = new HashMap<String, String>(); // HashMap from varName to value
        HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); // HashMap from varName to appNum
 
-
        // Update the valueMap
        for (int i = 0;i < nodeToProcess.getSetSet().size();i++) {
                NameValuePair nameValuePair = nodeToProcess.getSetSet().get(i);
@@ -176,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()) {
@@ -186,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;
@@ -385,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);
@@ -565,7 +568,6 @@ public class ConflictTracker extends ListenerAdapter {
 
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
-    // Instantiate timeoutTimer
     if (timeout > 0) {
       if (System.currentTimeMillis() - startTime > timeout) {
         StringBuilder sbTimeOut = new StringBuilder();
@@ -599,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