Fixing a bug in checkForConflict method in Conflict Tracker analysis!

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index c8bb079c07248c0633e5ac67caf59863f668cb36..75a16c277da75c149deacc850b47acdd1bbc5275 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -160,7 +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, Boolean> isManualMap = new HashMap<String, Boolean>(); // HashMap from varName to isManual
+       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++) {
@@ -181,22 +183,23 @@ public class ConflictTracker extends ListenerAdapter {
                }
                valueMap.put(varName, value);
                writerMap.put(varName, appNum);
-               isManualMap.put(varName, isManual);
             } else {
                valueMap.put(varName, value);
                writerMap.put(varName, appNum);
-               isManualMap.put(varName, isManual);
+               if (!isManual) {
+                       firstValueMap.put(varName, value);
+                       firstWriterMap.put(varName, appNum);
+               }
             }
        }
 
        // Check for conflict between outSet and this transition setSet
        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())
-                            &&!isManualMap.get(i.getVarName())) { 
+                        if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { 
                             // We have different values and different writers
                             errorMessage = createErrorMessage(i, valueMap, writerMap);
                             return true;