Fixing a bug

[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 06e6e4ae007b14c5e83932f7fe99bce59caddf64..1f2fa7d1b95eadb04adac11957017c8bc5c6ecbb 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -103,6 +103,7 @@ public class ConflictTracker extends ListenerAdapter {
                changed.remove(nodeToProcess);
 
                // Update the changed parents
+               parents.clear();
                parents = parentQueueMap.get(nodeToProcess);
                boolean isChanged = false;
 
@@ -124,7 +125,7 @@ public class ConflictTracker extends ListenerAdapter {
                }
 
                // Update the parents list for the successors of the current node
-               parents = new HashSet<Node>();
+               parents.clear();
                parents.add(nodeToProcess);
 
                // Checking if the out set has changed or not(Add its successors to the change list!)
@@ -159,6 +160,9 @@ public class ConflictTracker extends ListenerAdapter {
        ArrayList<NameValuePair> setSet = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap().get(currentTransition);
        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
+       HashMap<String, String> firstValueMap = new HashMap<String, String>(); // HashMap from varName to value - first instruction in transition
+       HashMap<String, Integer> firstWriterMap = new HashMap<String, Integer>(); // HashMap from varName to appNum - first instruction in transition
+       
 
        // Update the valueMap and writerMap + check for conflict between the elements of setSet
        for (int i = 0;i < setSet.size();i++) {
@@ -166,6 +170,7 @@ public class ConflictTracker extends ListenerAdapter {
            String varName = nameValuePair.getVarName();
            String value = nameValuePair.getValue();
            Integer appNum = nameValuePair.getAppNum();
+           Boolean isManual = nameValuePair.getIsManual();
 
            if (valueMap.containsKey(varName)) {
                // Check if we have a same writer
@@ -174,31 +179,29 @@ public class ConflictTracker extends ListenerAdapter {
                        if (!valueMap.get(varName).equals(value)) {
                                errorMessage = createErrorMessage(nameValuePair, valueMap, writerMap);
                                return true;
-                       } else { // We have two writers writing the same value
-                               writerMap.put(varName, 3); // 3 represents both apps
-                       }
-               } else {
-                       // Check if we have more than one value with the same writer
-                       if (!valueMap.get(varName).equals(value)) {
-                               // We have one writer writing more than one value in a same event
-                               valueMap.put(varName, "twoValue");
                        }
                }
+               valueMap.put(varName, value);
+               writerMap.put(varName, appNum);
             } else {
                valueMap.put(varName, value);
                writerMap.put(varName, appNum);
+               if (!isManual) {
+                       firstValueMap.put(varName, value);
+                       firstWriterMap.put(varName, appNum);
+               }
             }
        }
 
        // Check for conflict between outSet and this transition setSet
-       for (NameValuePair i : currentNode.getOutSet()) {
+       for (NameValuePair i : parentNode.getOutSet()) {
             if (valueMap.containsKey(i.getVarName())) {
-                String value = valueMap.get(i.getVarName());
-                Integer writer = writerMap.get(i.getVarName());
+                String value = firstValueMap.get(i.getVarName());
+                Integer writer = firstWriterMap.get(i.getVarName());
                     if ((value != null)&&(writer != null)) {
                         if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { 
                             // We have different values and different writers
-                            errorMessage = createErrorMessage(i, valueMap, writerMap);
+                            errorMessage = createErrorMessage(i, firstValueMap, firstWriterMap);
                             return true;
                         }
                     }
@@ -209,35 +212,46 @@ public class ConflictTracker extends ListenerAdapter {
   }
 
   boolean updateTheOutSet(Node parentNode, Node currentNode) {
-       HashMap<Transition, ArrayList<NameValuePair>> setSet = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap();
+       HashMap<Transition, ArrayList<NameValuePair>> setSets = parentNode.getOutgoingEdges().get(currentNode).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>();
        boolean isChanged = false;
 
-        for (Map.Entry mapElement : setSet.entrySet()) {
-            ArrayList<NameValuePair> value = (ArrayList<NameValuePair>)mapElement.getValue();
+        for (Map.Entry mapElement : setSets.entrySet()) {
+            ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
   
-            for (int i = 0;i < value.size();i++) {
-                       updatedVarNames.add(value.get(i).getVarName());
+            for (int i = 0;i < setSet.size();i++) {
+                       updatedVarNames.add(setSet.get(i).getVarName());
            }
         }
 
 
        for (NameValuePair i : parentNode.getOutSet()) {
+               outSetVarMap.put(i.getVarName(), i.getAppNum());
                if (!updatedVarNames.contains(i.getVarName()))
                        isChanged |= currentNode.getOutSet().add(i);
        }
 
 
-       for (Map.Entry mapElement : setSet.entrySet()) {
-            ArrayList<NameValuePair> value = (ArrayList<NameValuePair>)mapElement.getValue();
+       for (Map.Entry mapElement : setSets.entrySet()) {
+            ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
   
-            for (int i = 0;i < value.size();i++) {
-                       if (value.get(i).getAppNum().equals(lastWriter.get(value.get(i).getVarName())) 
-                           && value.get(i).getValue().equals(lastValue.get(value.get(i).getVarName()))) {
-                               isChanged |= currentNode.getOutSet().add(value.get(i));
+            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));
                        }
            }
         }
@@ -471,7 +485,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);
-    
+
     // Check if the outSet of this state has changed, update all of its successors' sets if any
     if (isChanged) {
        for (Node node : currentNode.getSuccessors()) {