X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FConflictTracker.java;h=c8bb079c07248c0633e5ac67caf59863f668cb36;hp=4d185d00e42617cda0288878623d6ca66e3f3a30;hb=fb03d04f1c3952b9ea983ac73fa8f7daa64e1307;hpb=cce97885c97afca1c3d8ef741d3251f4080d1539

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 4d185d0..c8bb079 100644
--- 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,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
-
-
-	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, 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++) {
@@ -185,6 +168,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,29 +177,26 @@ 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);
+		isManualMap.put(varName, isManual);
 	     } else {
 		valueMap.put(varName, value);
 		writerMap.put(varName, appNum);
+		isManualMap.put(varName, isManual);
 	     }
 	}
 
 	// 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());
 		     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;
@@ -501,7 +482,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()) {