Fix a bug in ConflictTracker

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index fa940012e2194e18587fdd5b143f5a87bee7762b..e99baedfedd8b5da74b2d0b92005559d7ce4851d 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -90,24 +90,32 @@ 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);
 
                // 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) {
+                       parentSet.add(nodeToProcess);
                        for (Node i : nodeToProcess.getSuccessors()) {
-                               if (!changed.contains(i))
-                                       changed.add(i);
+                               changed.add(i);
                        }
                }
       }
@@ -128,7 +136,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);
@@ -162,6 +169,7 @@ 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;
                                }
@@ -565,7 +573,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();