From f6351cd09edfd6d0f2bee6a1cb11ce56a2291d59 Mon Sep 17 00:00:00 2001
From: Seyed Amir Hossein Aqajari <saqajari@circinus-28.ics.uci.edu>
Date: Thu, 14 Nov 2019 13:31:16 -0800
Subject: [PATCH] Fix a bug in ConflictTracker

---
 .../gov/nasa/jpf/listener/ConflictTracker.java  | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index fa94001..e99baed 100644
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -90,24 +90,32 @@ 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);
 
       		// Check for a conflict in this transition(currentNode -> nodeToProcess)
-      		if (checkForConflict(currentNode))
+      		if (checkForConflict(nodeToProcess))
        			return true;
 
       		// 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()) {
-          			if (!changed.contains(i))
-            				changed.add(i);
+            			changed.add(i);
         		}
       		}
       }
@@ -128,7 +136,6 @@ public class ConflictTracker extends ListenerAdapter {
 	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
 
-
 	// Update the valueMap
 	for (int i = 0;i < nodeToProcess.getSetSet().size();i++) {
 		NameValuePair nameValuePair = nodeToProcess.getSetSet().get(i);
@@ -162,6 +169,7 @@ 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;
 				}
@@ -565,7 +573,6 @@ public class ConflictTracker extends ListenerAdapter {
 
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
-    // Instantiate timeoutTimer
     if (timeout > 0) {
       if (System.currentTimeMillis() - startTime > timeout) {
         StringBuilder sbTimeOut = new StringBuilder();
-- 
2.34.1