Minor changes in ConflictTracker
authorSeyed Amir Hossein Aqajari <saqajari@circinus-48.ics.uci.edu>
Fri, 15 Nov 2019 19:44:01 +0000 (11:44 -0800)
committerSeyed Amir Hossein Aqajari <saqajari@circinus-48.ics.uci.edu>
Fri, 15 Nov 2019 19:44:01 +0000 (11:44 -0800)
src/main/gov/nasa/jpf/listener/ConflictTracker.java

index e99baedfedd8b5da74b2d0b92005559d7ce4851d..3621a49ac3598589be39941c1107a27b20a919c2 100644 (file)
@@ -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,10 @@ 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++) {
+                       isChanged |= currentNode.getOutSet().add(setSet.get(i));
+               }
        }
 
        return isChanged;
@@ -393,7 +386,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 +599,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