Fixing a bug in manual_write-non_conflict + setSet conflicts

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 831442b16f345f60e4f1f6ce3f000def8fc7f789..c8bb079c07248c0633e5ac67caf59863f668cb36 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -160,7 +160,7 @@ 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
        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

 
        // Update the valueMap and writerMap + check for conflict between the elements of setSet
        for (int i = 0;i < setSet.size();i++) {
 
        // Update the valueMap and writerMap + check for conflict between the elements of setSet
        for (int i = 0;i < setSet.size();i++) {


@@ -168,6 +168,7 @@ public class ConflictTracker extends ListenerAdapter {
            String varName = nameValuePair.getVarName();
            String value = nameValuePair.getValue();
            Integer appNum = nameValuePair.getAppNum();
            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
 
            if (valueMap.containsKey(varName)) {
                // Check if we have a same writer


@@ -176,19 +177,15 @@ public class ConflictTracker extends ListenerAdapter {
                        if (!valueMap.get(varName).equals(value)) {
                                errorMessage = createErrorMessage(nameValuePair, valueMap, writerMap);
                                return true;
                        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);
+               isManualMap.put(varName, isManual);

             } else {
                valueMap.put(varName, value);
                writerMap.put(varName, appNum);
             } else {
                valueMap.put(varName, value);
                writerMap.put(varName, appNum);

+               isManualMap.put(varName, isManual);

             }
        }
 
             }
        }
 


@@ -198,7 +195,8 @@ public class ConflictTracker extends ListenerAdapter {
                 String value = valueMap.get(i.getVarName());
                 Integer writer = writerMap.get(i.getVarName());
                     if ((value != null)&&(writer != null)) {
                 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())) { 
+                        if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())
+                            &&!isManualMap.get(i.getVarName())) { 

                             // We have different values and different writers
                             errorMessage = createErrorMessage(i, valueMap, writerMap);
                             return true;
                             // We have different values and different writers
                             errorMessage = createErrorMessage(i, valueMap, writerMap);
                             return true;