From: Seyed Amir Hossein Aqajari <saqajari@circinus-48.ics.uci.edu>
Date: Thu, 5 Dec 2019 22:45:43 +0000 (-0800)
Subject: Fixing a bug in checkForConflict method in Conflict Tracker analysis!
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=a8c30c53e2fd8b1e25d259502e61c0fc06573e9c;ds=sidebyside

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 c8bb079..75a16c2 100644
--- 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;