Fixing a bug in checkForConflict method in Conflict Tracker 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 4d185d00e42617cda0288878623d6ca66e3f3a30..75a16c277da75c149deacc850b47acdd1bbc5275 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,25 +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
-
-
-       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);
-        }
+       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++) {
@@ -185,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
@@ -193,27 +179,25 @@ 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
@@ -501,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()) {