Fixing a bug in Conflict Tracker + Make propagate method much simpler

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 8b4e28486c6bb972e14ba9834db430cb3c6b10ef..697761801bda64e244d88df4323e59e5123c7b21 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -193,12 +193,10 @@ public class ConflictTracker extends ListenerAdapter {
   }
 
   boolean updateTheOutSet(Node parentNode, Node currentNode) {
-    HashMap<Transition, ArrayList<NameValuePair>> setSets = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap();
+    Edge edge = parentNode.getOutgoingEdges().get(currentNode);
+    HashMap<Transition, ArrayList<NameValuePair>> setSets = edge.getSetSetMap();
     HashSet<String> updatedVarNames = new HashSet<String>();
-    Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
-    HashMap<String, Integer> lastWriter = currentEdge.getLastWriter();
-    HashMap<String, String> lastValue = currentEdge.getLastValue();
-    HashMap<String, Integer> outSetVarMap = new HashMap<String, Integer>();
+    HashSet<String> outSetVarMap = new HashSet<String>();
     boolean isChanged = false;
 
     for (Map.Entry mapElement : setSets.entrySet()) {
@@ -210,30 +208,20 @@ public class ConflictTracker extends ListenerAdapter {
     }
 
     for (NameValuePair i : parentNode.getOutSet()) {
-      outSetVarMap.put(i.getVarName(), i.getAppNum());
+      outSetVarMap.add(i.getVarName());
       if (!updatedVarNames.contains(i.getVarName()))
         isChanged |= currentNode.getOutSet().add(i);
     }
 
+    ArrayList<NameValuePair> lastSetSet = setSets.get(edge.getFinalTransition());
 
-    for (Map.Entry mapElement : setSets.entrySet()) {
-      ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
-  
-      for (int i = 0;i < setSet.size();i++) {
-        String varName = setSet.get(i).getVarName();
-       Integer writer = lastWriter.get(varName);
-       String value = lastValue.get(varName);
-
-       if (setSet.get(i).getAppNum().equals(writer) 
-         && setSet.get(i).getValue().equals(value)) {
-         if (outSetVarMap.containsKey(varName)) {
-           Integer hashCode = outSetVarMap.get(varName).hashCode() * 31 +
-                              varName.hashCode();
-           currentNode.getOutSet().remove(hashCode);
-         }
-          isChanged |= currentNode.getOutSet().add(setSet.get(i));
-       }
+    for (int i = 0;i < lastSetSet.size();i++) {
+      String var = lastSetSet.get(i).getVarName();
+
+      if (outSetVarMap.contains(var)) {
+        currentNode.getOutSet().remove(lastSetSet.get(i));
       }
+      isChanged |= currentNode.getOutSet().add(lastSetSet.get(i));
     }
     return isChanged;
   }
@@ -241,32 +229,23 @@ public class ConflictTracker extends ListenerAdapter {
   void updateTheEdge(Node currentNode, Transition transition) {
     if (parentNode.getOutgoingEdges().containsKey(currentNode)) {
       Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
-        if (currentEdge.getSetSetMap().containsKey(transition)) { // Update the transition
-         if (manual)
-           currentEdge.getSetSetMap().put(transition, tempSetSet);
-         else
-           currentEdge.getSetSetMap().get(transition).addAll(tempSetSet);
-       } else { // Add a new transition
-           currentEdge.getSetSetMap().put(transition, tempSetSet);
-        }
+      if (currentEdge.getSetSetMap().containsKey(transition)) { // Update the transition
+       if (manual)
+         currentEdge.getSetSetMap().put(transition, tempSetSet);
+       else
+         currentEdge.getSetSetMap().get(transition).addAll(tempSetSet);
+      } else { // Add a new transition
+       currentEdge.getSetSetMap().put(transition, tempSetSet);
+      }
+      currentEdge.setFinalTransition(transition);
     } else {
       parentNode.getOutgoingEdges().put(currentNode, new Edge(parentNode, currentNode));
       Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
       currentEdge.getSetSetMap().put(transition, tempSetSet);
-    }
-
-    // Update the last writer and last value for this edge for each varName
-    Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
-    ArrayList<NameValuePair> setSet = currentEdge.getSetSetMap().get(transition);
-    for (int i = 0;i < setSet.size();i++) {
-      NameValuePair nameValuePair = setSet.get(i);
-      currentEdge.getLastWriter().put(nameValuePair.getVarName(), nameValuePair.getAppNum());
-      currentEdge.getLastValue().put(nameValuePair.getVarName(), nameValuePair.getValue());
+      currentEdge.setFinalTransition(transition);
     }
   }
 
-  
-
   static class Node {
     Integer id;
     HashSet<Node> predecessors = new HashSet<Node>();
@@ -301,6 +280,7 @@ public class ConflictTracker extends ListenerAdapter {
 
   static class Edge {
     Node source, destination;
+    Transition finalTransition;
     HashMap<String, Integer> lastWriter = new HashMap<String, Integer>();
     HashMap<String, String> lastValue = new HashMap<String, String>();
     HashMap<Transition, ArrayList<NameValuePair>> setSetMap = new HashMap<Transition, ArrayList<NameValuePair>>();
@@ -318,6 +298,14 @@ public class ConflictTracker extends ListenerAdapter {
       return destination;
     }
 
+    Transition getFinalTransition() {
+      return finalTransition;
+    }
+
+    void setFinalTransition(Transition transition) {
+      finalTransition = transition;
+    }
+
     HashMap<Transition, ArrayList<NameValuePair>> getSetSetMap() {
       return setSetMap;
     }
@@ -401,11 +389,6 @@ public class ConflictTracker extends ListenerAdapter {
 
     out.println("The state is restored to state with id: "+id+", depth: "+depth);
   
-    if (id == 24 && depth == 5) {
-           System.out.println("*****************************************");
-           System.out.println("*****************************************");
-           System.out.println("*****************************************");
-    }
     // Update the parent node
     if (nodes.containsKey(id)) {
       parentNode = nodes.get(id);
@@ -469,14 +452,7 @@ public class ConflictTracker extends ListenerAdapter {
 
     // Update the outset of the current node and check if it is changed or not to propagate the change
     boolean isChanged = updateTheOutSet(parentNode, currentNode);
-
-
-    System.out.println("######################### The outset is:");
-    for (NameValuePair nvp : currentNode.getOutSet()) {
-       System.out.println("writer: "+nvp.getAppNum());
-       System.out.println("value: "+nvp.getValue());
-       System.out.println("var : "+nvp.getVarName());
-    }      
+           
     // Check if the outSet of this state has changed, update all of its successors' sets if any
     if (isChanged)
       conflictFound = conflictFound || checkAllSuccForConflict(currentNode) || propagateTheChange(currentNode);
@@ -498,12 +474,6 @@ public class ConflictTracker extends ListenerAdapter {
 
     out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
 
-    if (id == 24 && depth == 5) {
-            System.out.println("*****************************************");
-            System.out.println("*****************************************");
-            System.out.println("*****************************************");
-    }
-
     // Update the parent node
     if (nodes.containsKey(id)) {
       parentNode = nodes.get(id);
@@ -709,9 +679,6 @@ public class ConflictTracker extends ListenerAdapter {
               if (getWriter(ti.getStack(), manualSet) != null)
                 manual = true;
              
-             System.out.println("############################## writer: "+writer);
-             System.out.println("############################## value: "+value);
-             System.out.println("############################## var: "+var);
               // Update the temporary Set set.
               writeWriterAndValue(writer, value, var);
             }