Fixing a bug in Conflict Tracker analysis
authorSeyed Amir Hossein Aqajari <saqajari@circinus-48.ics.uci.edu>
Thu, 5 Dec 2019 19:47:54 +0000 (11:47 -0800)
committerSeyed Amir Hossein Aqajari <saqajari@circinus-48.ics.uci.edu>
Thu, 5 Dec 2019 19:47:54 +0000 (11:47 -0800)
src/main/gov/nasa/jpf/listener/ConflictTracker.java

index 4d185d0..831442b 100644 (file)
@@ -103,6 +103,7 @@ public class ConflictTracker extends ListenerAdapter {
                changed.remove(nodeToProcess);
 
                // Update the changed parents
                changed.remove(nodeToProcess);
 
                // Update the changed parents
+               parents.clear();
                parents = parentQueueMap.get(nodeToProcess);
                boolean isChanged = false;
 
                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
                }
 
                // 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!)
                parents.add(nodeToProcess);
 
                // Checking if the out set has changed or not(Add its successors to the change list!)
@@ -161,24 +162,6 @@ public class ConflictTracker extends ListenerAdapter {
        HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); //  HashMap from varName to appNum
 
 
        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);
-        }
-
        // Update the valueMap and writerMap + check for conflict between the elements of setSet
        for (int i = 0;i < setSet.size();i++) {
             NameValuePair nameValuePair = setSet.get(i);
        // Update the valueMap and writerMap + check for conflict between the elements of setSet
        for (int i = 0;i < setSet.size();i++) {
             NameValuePair nameValuePair = setSet.get(i);
@@ -210,7 +193,7 @@ public class ConflictTracker extends ListenerAdapter {
        }
 
        // Check for conflict between outSet and this transition setSet
        }
 
        // 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 (valueMap.containsKey(i.getVarName())) {
                 String value = valueMap.get(i.getVarName());
                 Integer writer = writerMap.get(i.getVarName());
@@ -501,7 +484,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);
 
     // 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()) {
     // Check if the outSet of this state has changed, update all of its successors' sets if any
     if (isChanged) {
        for (Node node : currentNode.getSuccessors()) {