Make a change in ConflictTracker analysis

[jpf-core.git] / src / main / gov / nasa / jpf / listener / ConflictTracker.java

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 82a71147943f905265e4113ee6b204a8b3f38d29..8b4e28486c6bb972e14ba9834db430cb3c6b10ef 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -89,12 +89,13 @@ public class ConflictTracker extends ListenerAdapter {
 
   boolean propagateTheChange(Node currentNode) {
     HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
 
   boolean propagateTheChange(Node currentNode) {
     HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());

-    HashMap<Node, HashSet<Node>> parentQueueMap = new HashMap<Node, HashSet<Node>>();
-    HashSet<Node> parents = new HashSet<Node>();
-    parents.add(currentNode);
+    boolean isChanged = false;

 
     for (Node node : currentNode.getSuccessors()) {
 
     for (Node node : currentNode.getSuccessors()) {

-      parentQueueMap.put(node, parents);
+      isChanged = false;
+      isChanged = updateTheOutSet(currentNode, node);
+      if (isChanged)
+        changed.add(node);

     }
 
     while(!changed.isEmpty()) {
     }
 
     while(!changed.isEmpty()) {


@@ -102,40 +103,15 @@ public class ConflictTracker extends ListenerAdapter {
       Node nodeToProcess = changed.iterator().next();
       changed.remove(nodeToProcess);
 
       Node nodeToProcess = changed.iterator().next();
       changed.remove(nodeToProcess);
 

-      // Update the changed parents
-      parents.clear();
-      parents = parentQueueMap.get(nodeToProcess);
-      boolean isChanged = false;
-
-      for (Node node : parents) {
-        // Update the edge
-       isChanged |= updateTheOutSet(node, nodeToProcess);
-      }
-
-      // All the changes in current parents are propagated
-      parentQueueMap.get(nodeToProcess).clear();
-
-      // Check if the node has changed or not
-      if (isChanged) {
-       // Check for a conflict in all the transition out of this node
-       if (checkAllSuccForConflict(nodeToProcess))
-         return true;
-        
-       // Update the parents list for the successors of the current node
-       parents.clear();
-       parents.add(nodeToProcess);
-
-       // For all the successors of the current node
-       for (Node i : nodeToProcess.getSuccessors()) {
-          if (!changed.contains(i))
-            changed.add(i);
-
-          // Update the list of updated parents for the current node
-          if (parentQueueMap.containsKey(i))
-            parentQueueMap.get(i).add(nodeToProcess);
-          else
-            parentQueueMap.put(i, parents);
-        }
+      // Update all the successors of the node
+      for (Node node : nodeToProcess.getSuccessors()) {
+       isChanged = false;
+       isChanged = updateTheOutSet(nodeToProcess, node);
+       if (isChanged) {
+          changed.add(node);
+          if (checkAllSuccForConflict(node))
+            return true;
+       }

       }
     }
     return false;
       }
     }
     return false;


@@ -425,6 +401,11 @@ public class ConflictTracker extends ListenerAdapter {
 
     out.println("The state is restored to state with id: "+id+", depth: "+depth);
   
 
     out.println("The state is restored to state with id: "+id+", depth: "+depth);
   

+    if (id == 24 && depth == 5) {
+           System.out.println("*****************************************");
+           System.out.println("*****************************************");
+           System.out.println("*****************************************");
+    }

     // Update the parent node
     if (nodes.containsKey(id)) {
       parentNode = nodes.get(id);
     // Update the parent node
     if (nodes.containsKey(id)) {
       parentNode = nodes.get(id);


@@ -489,6 +470,13 @@ 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);
 

+
+    System.out.println("######################### The outset is:");
+    for (NameValuePair nvp : currentNode.getOutSet()) {
+       System.out.println("writer: "+nvp.getAppNum());
+       System.out.println("value: "+nvp.getValue());
+       System.out.println("var : "+nvp.getVarName());
+    }      

     // Check if the outSet of this state has changed, update all of its successors' sets if any
     if (isChanged)
       conflictFound = conflictFound || checkAllSuccForConflict(currentNode) || propagateTheChange(currentNode);
     // Check if the outSet of this state has changed, update all of its successors' sets if any
     if (isChanged)
       conflictFound = conflictFound || checkAllSuccForConflict(currentNode) || propagateTheChange(currentNode);


@@ -510,6 +498,12 @@ public class ConflictTracker extends ListenerAdapter {
 
     out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
 
 
     out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
 

+    if (id == 24 && depth == 5) {
+            System.out.println("*****************************************");
+            System.out.println("*****************************************");
+            System.out.println("*****************************************");
+    }
+

     // Update the parent node
     if (nodes.containsKey(id)) {
       parentNode = nodes.get(id);
     // Update the parent node
     if (nodes.containsKey(id)) {
       parentNode = nodes.get(id);


@@ -714,7 +708,10 @@ public class ConflictTracker extends ListenerAdapter {
 
               if (getWriter(ti.getStack(), manualSet) != null)
                 manual = true;
 
               if (getWriter(ti.getStack(), manualSet) != null)
                 manual = true;

-
+             
+             System.out.println("############################## writer: "+writer);
+             System.out.println("############################## value: "+value);
+             System.out.println("############################## var: "+var);

               // Update the temporary Set set.
               writeWriterAndValue(writer, value, var);
             }
               // Update the temporary Set set.
               writeWriterAndValue(writer, value, var);
             }