Fix a bug in ConflictTracker.java

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 435a29a0a7505850384781699ab9d9b1d3cab8b7..fa940012e2194e18587fdd5b143f5a87bee7762b 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -128,6 +128,7 @@ 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);
@@ -174,12 +175,10 @@ 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;
 
        for (int i = 0;i < setSet.size();i++) {
                updatedVarNames.add(setSet.get(i).getVarName());
-               lastWriter.put(setSet.get(i).getVarName(), setSet.get(i).getAppNum());
        }
 
        for (NameValuePair i : parentNode.getOutSet()) {
@@ -188,8 +187,7 @@ public class ConflictTracker extends ListenerAdapter {
        }
 
        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));
+               isChanged |= currentNode.getOutSet().add(setSet.get(i));
        }
 
        return isChanged;
@@ -342,11 +340,10 @@ 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
@@ -386,6 +383,9 @@ public class ConflictTracker extends ListenerAdapter {
     // 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 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);