From: Seyed Amir Hossein Aqajari <saqajari@circinus-48.ics.uci.edu>
Date: Fri, 15 Nov 2019 19:44:01 +0000 (-0800)
Subject: Minor changes in ConflictTracker
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=70f667e8578c5c07681ab1c95485fd34ea4f2ea9;p=jpf-core.git

Minor changes in ConflictTracker
---

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index e99baed..3621a49 100644
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -90,20 +90,12 @@ public class ConflictTracker extends ListenerAdapter {
 
   boolean propagateTheChange(Node currentNode) {
 	HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
-	HashSet<Node> parentSet = new HashSet<Node>();
 
 	while(!changed.isEmpty()) {
         	// Get the first element of HashSet and remove it from the changed set
       		Node nodeToProcess = changed.iterator().next();
       		changed.remove(nodeToProcess);
 
-		// Change the parent node
-		if (!currentNode.getSuccessors().contains(nodeToProcess)) {
-			currentNode = parentSet.iterator().next();
-			parentSet.remove(currentNode);
-		}
-			
-
       		// Update the edge
       		boolean isChanged = updateEdge(currentNode, nodeToProcess);
 
@@ -113,10 +105,7 @@ public class ConflictTracker extends ListenerAdapter {
 
       		// Checking if the out set has changed or not(Add its successors to the change list!)
       		if (isChanged) {
-			parentSet.add(nodeToProcess);
-        		for (Node i : nodeToProcess.getSuccessors()) {
-            			changed.add(i);
-        		}
+			propagateTheChange(nodeToProcess);
       		}
       }
 
@@ -129,6 +118,7 @@ public class ConflictTracker extends ListenerAdapter {
 			 " to the variable: "+pair.getVarName()+" while App"+
 			 writerMap.get(pair.getVarName())+" is overwriting the value: "
 			 +valueMap.get(pair.getVarName())+" to the same variable!";
+	System.out.println(message);	
 	return message;
   }
 
@@ -169,7 +159,6 @@ public class ConflictTracker extends ListenerAdapter {
 			Integer writer = writerMap.get(i.getVarName());
 			if ((value != null)&&(writer != null)) {
 				if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { // We have different values
-					System.out.println("we are here!!!!");
 					errorMessage = createErrorMessage(i, valueMap, writerMap);
 					return true;
 				}
@@ -184,9 +173,11 @@ public class ConflictTracker extends ListenerAdapter {
 	ArrayList<NameValuePair> setSet = currentNode.getSetSetMap().get(parentNode);
 	HashSet<String> updatedVarNames = new HashSet<String>();
 	boolean isChanged = false;
-
-	for (int i = 0;i < setSet.size();i++) {
-		updatedVarNames.add(setSet.get(i).getVarName());
+	
+	if (setSet != null) {
+		for (int i = 0;i < setSet.size();i++) {
+			updatedVarNames.add(setSet.get(i).getVarName());
+		}
 	}
 
 	for (NameValuePair i : parentNode.getOutSet()) {
@@ -194,8 +185,10 @@ public class ConflictTracker extends ListenerAdapter {
 			isChanged |= currentNode.getOutSet().add(i);
 	}
 
-	for (int i = 0;i < setSet.size();i++) {
-		isChanged |= currentNode.getOutSet().add(setSet.get(i));
+	if (setSet != null) {
+		for (int i = 0;i < setSet.size();i++) {
+			isChanged |= currentNode.getOutSet().add(setSet.get(i));
+		}
 	}
 
 	return isChanged;
@@ -393,7 +386,7 @@ public class ConflictTracker extends ListenerAdapter {
 
     // Check for the conflict in this edge
     conflictFound = checkForConflict(currentNode);
-
+    
     // Check if the outSet of this state has changed, update all of its successors' sets if any
     if (isChanged)
 	conflictFound = conflictFound || propagateTheChange(currentNode);
@@ -606,6 +599,7 @@ public class ConflictTracker extends ListenerAdapter {
       } else {
         if (executedInsn instanceof WriteInstruction) {
           String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
+
           for (String var : conflictSet) {
             if (varId.contains(var)) {
               // Get variable info