Modifying conflict tracker

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 134346775940c10aaf5acd5db90d67c8b16159b9..1aa50b92ef37ed2aad2b1b126e46fd1f706e5f40 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -93,104 +93,109 @@ public class ConflictTracker extends ListenerAdapter {
        HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
 
        while(!changed.isEmpty()) {
        HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
 
        while(!changed.isEmpty()) {

-      // Get the first element of HashSet and remove it from the changed set
-      Node nodeToProcess = changed.iterator().next();
-      changed.remove(nodeToProcess);
-
-      // Update the sets, store the outSet to temp before its changes
-      boolean isChanged = updateSets(nodeToProcess);
-
-      // Check for a conflict
-      if (checkForConflict(nodeToProcess))
-        return true;
-
-      // Checking if the out set has changed or not(Add its successors to the change list!)
-      if (isChanged) {
-        for (Node i : nodeToProcess.getSuccessors()) {
-          if (!changed.contains(i))
-            changed.add(i);
-        }
+               // Get the first element of HashSet and remove it from the changed set
+               Node nodeToProcess = changed.iterator().next();
+               changed.remove(nodeToProcess);
+
+               // Update the edge
+               boolean isChanged = updateEdge(currentNode, nodeToProcess);
+
+               // Check for a conflict in this transition(currentNode -> nodeToProcess)
+               if (checkForConflict(currentNode))
+                               return true;
+
+               // Checking if the out set has changed or not(Add its successors to the change list!)
+               if (isChanged) {
+                       for (Node i : nodeToProcess.getSuccessors()) {
+                               if (!changed.contains(i))
+                                       changed.add(i);
+                       }
+               }

       }
       }

-       }
-
-       return false;
-  }
-
-  boolean setOutSet(Node currentNode) {
-       Integer prevSize = currentNode.getOutSet().size();
-
-       // Update based on setSet
-       for (NameValuePair i : currentNode.getSetSet()) {
-      if (currentNode.getOutSet().contains(i))
-        currentNode.getOutSet().remove(i);
-      currentNode.getOutSet().add(i);
-       }

 
 

-       // Add all the inSet
-       currentNode.getOutSet().addAll(currentNode.getInSet());
-
-       // Check if the outSet is changed
-       if (!prevSize.equals(currentNode.getOutSet().size()))
-      return true;
-       
-       return false;
+      return false;

   }
 
   }
 

-  void setInSet(Node currentNode) {
-       for (Node i : currentNode.getPredecessors()) {
-      currentNode.getInSet().addAll(i.getOutSet());
-    }
+  String createErrorMessage(NameValuePair pair, HashMap<String, String> valueMap, HashMap<String, Integer> writerMap) {
+       String message = "Conflict found between the two apps. App"+pair.getAppNum()+
+                        " has written the value: "+pair.getValue()+
+                        " to the variable: "+pair.getVarName()+" while App"+
+                        writerMap.get(pair.getVarName())+" is overwriting the value: "
+                        +valueMap.get(pair.getVarName())+" to the same variable!";
+       return message;

   }
 
   }
 

-  boolean checkForConflict(Node currentNode) {
+  boolean checkForConflict(Node nodeToProcess) {

        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, String> valueMap = new HashMap<String, String>(); // HashMap from varName to value
        HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); // HashMap from varName to appNum
 

-       for (NameValuePair i : currentNode.getSetSet()) {
-      if (i.getIsManual()) // Manual input: we have no conflict
-        continue;
-
-      valueMap.put(i.getVarName(), i.getValue());
-      if (writerMap.containsKey(i.getVarName()))
-        writerMap.put(i.getVarName(), i.getAppNum()+writerMap.get(i.getVarName())); // We have two writers?
-      else
-        writerMap.put(i.getVarName(), i.getAppNum());
+       // Update the valueMap and check if we have conflict in the setSet
+       for (NameValuePair i : nodeToProcess.getSetSet()) {
+               if (i.getIsManual()) // Manual input: we have no conflict
+                       continue; // If this manual write is the last write, this is actually a break
+               
+               if (valueMap.containsKey(i.getVarName())) {
+                       if (!valueMap.get(i.getVarName()).equals(i.getValue())) { // Check if their value is different we have a conflict
+                               errorMessage = createErrorMessage(i, valueMap, writerMap);                              
+                               return true;
+                       }
+                       else // We have two writers writing the same value
+                               writerMap.put(i.getVarName(), i.getAppNum()+writerMap.get(i.getVarName()));
+               } else {
+                       valueMap.put(i.getVarName(), i.getValue());
+                       writerMap.put(i.getVarName(), i.getAppNum());
+               }

        }
 
        }
 

-       // Comparing the inSet and setSet to find the conflict
-       for (NameValuePair i : currentNode.getInSet()) {
-      if (valueMap.containsKey(i.getVarName())) {
-        String value = valueMap.get(i.getVarName());
-        Integer writer = writerMap.get(i.getVarName());
-        if ((value != null)&&(writer != null)) {
-          if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { // We have different values
-            errorMessage = "Conflict found between the two apps. App"+i.getAppNum()+" has written the value: "+i.getValue()+
-                    " to the variable: "+i.getVarName()+" while App"+writerMap.get(i.getVarName())+" is overwriting the value: "
-                    +valueMap.get(i.getVarName())+" to the same variable!";
-            return true;
-          }
-        }
-      }
+       // Comparing the outSet to setSet
+       for (NameValuePair i : nodeToProcess.getOutSet()) {
+               if (valueMap.containsKey(i.getVarName())) {
+                       String value = valueMap.get(i.getVarName());
+                       Integer writer = writerMap.get(i.getVarName());
+                       if ((value != null)&&(writer != null)) {
+                               if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { // We have different values
+                                       errorMessage = createErrorMessage(i, valueMap, writerMap);
+                                       return true;
+                               }
+                       }
+               }

        }
 
        return false;
   }
 
        }
 
        return false;
   }
 

-  boolean updateSets(Node currentNode) {
-       // Set input set according to output set of pred states of current state
-    setInSet(currentNode);
+  boolean updateEdge(Node parentNode, Node currentNode) {
+       HashSet<NameValuePair> setSet = currentNode.getSetSetMap().get(parentNode);
+       HashSet<String> updatedVarNames = new HashSet<String>();
+       HashMap<String, Integer> lastWriter = new HashMap<String, Integer>(); // Store the last writer of each variable
+       boolean isChanged = false;

 
 

-       // Set outSet according to inSet, and setSet of current node, check if there is a change
-    return setOutSet(currentNode);
+       for (NameValuePair i : setSet) {
+               updatedVarNames.add(i.getVarName());
+               lastWriter.put(i.getVarName(), i.getAppNum());
+       }
+
+       for (NameValuePair i : parentNode.getOutSet()) {
+               if (!updatedVarNames.contains(i.getVarName()))
+                       isChanged |= currentNode.getOutSet().add(i);
+       }
+
+       for (NameValuePair i : setSet) {
+               if (i.getAppNum().equals(lastWriter.get(i.getVarName()))) // Add the last writer of each variable to outSet
+                       isChanged |= currentNode.getOutSet().add(i);
+       }
+
+       return isChanged;

   }
 
   static class Node {
        Integer id;
        HashSet<Node> predecessors = new HashSet<Node>();
        HashSet<Node> successors = new HashSet<Node>();
   }
 
   static class Node {
        Integer id;
        HashSet<Node> predecessors = new HashSet<Node>();
        HashSet<Node> successors = new HashSet<Node>();

-       HashSet<NameValuePair> inSet = new HashSet<NameValuePair>();

        HashSet<NameValuePair> setSet = new HashSet<NameValuePair>();
        HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
        HashSet<NameValuePair> setSet = new HashSet<NameValuePair>();
        HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();

+       HashMap<Node, HashSet<NameValuePair>> setSetMap = new HashMap<Node, HashSet<NameValuePair>>();
+

 
        Node(Integer id) {
                this.id = id;
 
        Node(Integer id) {
                this.id = id;


@@ -205,11 +210,11 @@ public class ConflictTracker extends ListenerAdapter {
        }
 
        void setSetSet(HashSet<NameValuePair> setSet, boolean isManual) {
        }
 
        void setSetSet(HashSet<NameValuePair> setSet, boolean isManual) {

-      if (isManual)
-        this.setSet = new HashSet<NameValuePair>();
-      for (NameValuePair i : setSet) {
-        this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual()));
-      }
+             if (isManual)
+               this.setSet = new HashSet<NameValuePair>();
+             for (NameValuePair i : setSet) {
+               this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual()));
+             }

        }
 
        Integer getId() {
        }
 
        Integer getId() {


@@ -224,10 +229,6 @@ public class ConflictTracker extends ListenerAdapter {
                return successors;
        }
 
                return successors;
        }
 

-       HashSet<NameValuePair> getInSet() {
-               return inSet;
-       }
-

        HashSet<NameValuePair> getSetSet() {
                return setSet;
        }
        HashSet<NameValuePair> getSetSet() {
                return setSet;
        }


@@ -235,6 +236,10 @@ public class ConflictTracker extends ListenerAdapter {
        HashSet<NameValuePair> getOutSet() {
                return outSet;
        }
        HashSet<NameValuePair> getOutSet() {
                return outSet;
        }

+
+       HashMap<Node, HashSet<NameValuePair>> getSetSetMap() {
+               return setSetMap;
+       }

   }
 
   static class NameValuePair {
   }
 
   static class NameValuePair {


@@ -244,10 +249,10 @@ public class ConflictTracker extends ListenerAdapter {
        boolean isManual;
 
        NameValuePair(Integer appNum, String value, String varName, boolean isManual) {
        boolean isManual;
 
        NameValuePair(Integer appNum, String value, String varName, boolean isManual) {

-      this.appNum = appNum;
-      this.value = value;
-      this.varName = varName;
-      this.isManual = isManual;
+               this.appNum = appNum;
+               this.value = value;
+               this.varName = varName;
+               this.isManual = isManual;

        }
 
        void setAppNum(Integer appNum) {
        }
 
        void setAppNum(Integer appNum) {


@@ -328,6 +333,9 @@ public class ConflictTracker extends ListenerAdapter {
     depth = search.getDepth();
     operation = "forward";
 
     depth = search.getDepth();
     operation = "forward";
 

+    // Check for the conflict in this new transition
+    conflictFound = checkForConflict(parentNode);
+

     // Add the node to the list of nodes       
     nodes.put(id, new Node(id));
     Node currentNode = nodes.get(id);
     // Add the node to the list of nodes       
     nodes.put(id, new Node(id));
     Node currentNode = nodes.get(id);


@@ -363,11 +371,14 @@ public class ConflictTracker extends ListenerAdapter {
     if (!(parentNode.getSuccessors().contains(currentNode)))
         parentNode.addSuccessor(currentNode);
 
     if (!(parentNode.getSuccessors().contains(currentNode)))
         parentNode.addSuccessor(currentNode);
 

-    // Update the sets, check if the outSet is changed or not
-    boolean isChanged = updateSets(currentNode);
-   
-    // Check for a conflict
-    conflictFound = checkForConflict(currentNode);
+
+    // Update the setSetMap of the current node
+    for (Node i : currentNode.getPredecessors()) {
+       currentNode.getSetSetMap().put(i, i.getSetSet());
+    }
+
+    // Update the edge and check if the outset of the current node is changed or not to propagate the change
+    boolean isChanged = updateEdge(parentNode, currentNode);

 
     // Check if the outSet of this state has changed, update all of its successors' sets if any
     if (isChanged)
 
     // Check if the outSet of this state has changed, update all of its successors' sets if any
     if (isChanged)