A minor change 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 435a29a0a7505850384781699ab9d9b1d3cab8b7..a0ecc4bb6721597ba8631d83deeb8929feb207f8 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;
   }
 
@@ -174,12 +172,15 @@ public class ConflictTracker extends ListenerAdapter {
   boolean updateEdge(Node parentNode, Node currentNode) {
        ArrayList<NameValuePair> setSet = currentNode.getSetSetMap().get(parentNode);
        HashSet<String> updatedVarNames = new HashSet<String>();
-       HashMap<String, Integer> lastWriter = new HashMap<String, Integer>(); // Store the last writer of each variable
-       boolean isChanged = false;
+       HashMap<Integer, String> writerLastValue = new HashMap<Integer, String>();
 
-       for (int i = 0;i < setSet.size();i++) {
-               updatedVarNames.add(setSet.get(i).getVarName());
-               lastWriter.put(setSet.get(i).getVarName(), setSet.get(i).getAppNum());
+       boolean isChanged = false;
+       
+       if (setSet != null) {
+               for (int i = 0;i < setSet.size();i++) {
+                       updatedVarNames.add(setSet.get(i).getVarName());
+                       writerLastValue.put(setSet.get(i).getAppNum(), setSet.get(i).getValue());
+               }
        }
 
        for (NameValuePair i : parentNode.getOutSet()) {
@@ -187,9 +188,12 @@ public class ConflictTracker extends ListenerAdapter {
                        isChanged |= currentNode.getOutSet().add(i);
        }
 
-       for (int i = 0;i < setSet.size();i++) {
-               if (setSet.get(i).getAppNum().equals(lastWriter.get(setSet.get(i).getVarName()))) // Add the last writer of each variable to outSet
-                       isChanged |= currentNode.getOutSet().add(setSet.get(i));
+       if (setSet != null) {
+               for (int i = 0;i < setSet.size();i++) {
+                       if (setSet.get(i).getValue().equals(writerLastValue.get(setSet.get(i).getAppNum()))) {
+                               isChanged |= currentNode.getOutSet().add(setSet.get(i));
+                       }
+               }
        }
 
        return isChanged;
@@ -200,9 +204,8 @@ public class ConflictTracker extends ListenerAdapter {
        HashSet<Node> predecessors = new HashSet<Node>();
        HashSet<Node> successors = new HashSet<Node>();
        HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
+        ArrayList<NameValuePair> setSet = new ArrayList<NameValuePair>();
        HashMap<Node, ArrayList<NameValuePair>> setSetMap = new HashMap<Node, ArrayList<NameValuePair>>();
-       ArrayList<NameValuePair> setSet = new ArrayList<NameValuePair>();
-
 
        Node(Integer id) {
          this.id = id;
@@ -216,16 +219,6 @@ public class ConflictTracker extends ListenerAdapter {
          successors.add(node);
        }
 
-       void setSetSet(ArrayList<NameValuePair> setSet, boolean isManual) {
-         if (isManual)
-           this.setSet = new ArrayList<NameValuePair>();
-
-         for (int i = 0;i < setSet.size();i++) {
-           this.setSet.add(new NameValuePair(setSet.get(i).getAppNum(), setSet.get(i).getValue(), 
-                                             setSet.get(i).getVarName(), setSet.get(i).getIsManual()));
-           }
-       }
-
        Integer getId() {
                return id;
        }
@@ -238,14 +231,14 @@ public class ConflictTracker extends ListenerAdapter {
                return successors;
        }
 
-       ArrayList<NameValuePair> getSetSet() {
-               return setSet;
-       }
-
        HashSet<NameValuePair> getOutSet() {
                return outSet;
        }
 
+        ArrayList<NameValuePair> getSetSet() {
+               return setSet;
+        }
+
        HashMap<Node, ArrayList<NameValuePair>> getSetSetMap() {
                return setSetMap;
        }
@@ -276,7 +269,7 @@ public class ConflictTracker extends ListenerAdapter {
                this.varName = varName;
        }
 
-    void setIsManual(String varName) {
+        void setIsManual(String varName) {
                this.isManual = isManual;
        }
 
@@ -342,18 +335,24 @@ public class ConflictTracker extends ListenerAdapter {
     depth = search.getDepth();
     operation = "forward";
 
-    // Check for the conflict in this new transition
-    conflictFound = checkForConflict(parentNode);
+    // Add the node to the list of nodes
+    if (nodes.get(id) == null)
+       nodes.put(id, new Node(id));
 
-    // Add the node to the list of nodes       
-    nodes.put(id, new Node(id));
     Node currentNode = nodes.get(id);
 
-    // Update the setSet for this new node
-    currentNode.setSetSet(tempSetSet, manual);
-    tempSetSet = new ArrayList<NameValuePair>(); 
+    if ((currentNode.getSetSetMap().get(parentNode) == null) || manual)
+       currentNode.getSetSetMap().put(parentNode, new ArrayList<NameValuePair>());
+
+    // Update the setSet for the edge
+    currentNode.getSetSetMap().get(parentNode).addAll(tempSetSet);
+    parentNode.getSetSet().addAll(tempSetSet);
+    tempSetSet = new ArrayList<NameValuePair>();
     manual = false;
 
+    // Check for the conflict in this edge
+    conflictFound = checkForConflict(parentNode);
+
     if (search.isNewState()) {
       detail = "new";
     } else {
@@ -377,15 +376,9 @@ public class ConflictTracker extends ListenerAdapter {
     if (!(parentNode.getSuccessors().contains(currentNode)))
         parentNode.addSuccessor(currentNode);
 
-
-    // Update the setSetMap of the current node
-    for (Node i : currentNode.getPredecessors()) {
-       currentNode.getSetSetMap().put(i, i.getSetSet());
-    }
-
     // Update the edge and check if the outset of the current node is changed or not to propagate the change
     boolean isChanged = updateEdge(parentNode, 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 +558,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 +591,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