Change in Analysis

[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 193d2f0497097714243ec835d4c2e943d021e7fc..4d185d00e42617cda0288878623d6ca66e3f3a30 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -160,6 +160,25 @@ 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
 
+
+       System.out.println("#########################Set Set:");
+       for (int i = 0;i < setSet.size();i++) {
+            NameValuePair nameValuePair = setSet.get(i);
+            String varName = nameValuePair.getVarName();
+            String value = nameValuePair.getValue();
+            Integer appNum = nameValuePair.getAppNum();
+
+           System.out.println("varName="+varName+", value="+value+", appNum="+appNum);
+       }
+       System.out.println("+++++++++++++++++++++++++Out Set:");
+       for (NameValuePair nameValuePair : currentNode.getOutSet()) {
+            String varName = nameValuePair.getVarName();
+            String value = nameValuePair.getValue();
+            Integer appNum = nameValuePair.getAppNum();
+
+            System.out.println("varName="+varName+", value="+value+", appNum="+appNum);
+        }
+
        // Update the valueMap and writerMap + check for conflict between the elements of setSet
        for (int i = 0;i < setSet.size();i++) {
             NameValuePair nameValuePair = setSet.get(i);
@@ -196,7 +215,8 @@ public class ConflictTracker extends ListenerAdapter {
                 String value = valueMap.get(i.getVarName());
                 Integer writer = writerMap.get(i.getVarName());
                     if ((value != null)&&(writer != null)) {
-                        if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { // We have different values and different writers
+                        if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { 
+                            // We have different values and different writers
                             errorMessage = createErrorMessage(i, valueMap, writerMap);
                             return true;
                         }
@@ -208,35 +228,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));
                        }
            }
         }
@@ -472,9 +503,16 @@ public class ConflictTracker extends ListenerAdapter {
     boolean isChanged = updateTheOutSet(parentNode, currentNode);
     
     // Check if the outSet of this state has changed, update all of its successors' sets if any
-    if (isChanged)
+    if (isChanged) {
+       for (Node node : currentNode.getSuccessors()) {
+               HashMap<Transition, ArrayList<NameValuePair>> setSets = currentNode.getOutgoingEdges().get(node).getSetSetMap();
+               for (Map.Entry mapElement : setSets.entrySet()) {
+                       Transition currentTransition = (Transition)mapElement.getKey();
+                       conflictFound = conflictFound || checkForConflict(currentNode, node, currentTransition);
+               }
+       }
        conflictFound = conflictFound || propagateTheChange(currentNode);
-
+    }
     // Update the parent node
     if (nodes.containsKey(id)) {
          parentNode = nodes.get(id);