Change in the Conflict Tracker analysis
[jpf-core.git] / src / main / gov / nasa / jpf / listener / ConflictTracker.java
index a0ecc4b..193d2f0 100644 (file)
@@ -37,7 +37,6 @@ import java.util.*;
  **/
 
 public class ConflictTracker extends ListenerAdapter {
-
   private final PrintWriter out;
   private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
   private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
@@ -90,22 +89,56 @@ public class ConflictTracker extends ListenerAdapter {
 
   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);
+
+       for (Node node : currentNode.getSuccessors()) {
+               parentQueueMap.put(node, parents);
+       }
 
        while(!changed.isEmpty()) {
-               // Get the first element of HashSet and remove it from the changed set
+               // Get the first element of the changed set and remove it
                Node nodeToProcess = changed.iterator().next();
                changed.remove(nodeToProcess);
 
-               // Update the edge
-               boolean isChanged = updateEdge(currentNode, nodeToProcess);
+               // Update the changed parents
+               parents = parentQueueMap.get(nodeToProcess);
+               boolean isChanged = false;
+
+               for (Node node : parents) {
+                       // Update the edge
+                       isChanged |= updateTheOutSet(node, nodeToProcess);
+               }
+
+               // Check for a conflict if the outSet of nodeToProcess is changed
+               if (isChanged) {
+                       for (Node node : nodeToProcess.getSuccessors()) {
+                               HashMap<Transition, ArrayList<NameValuePair>> setSets = nodeToProcess.getOutgoingEdges().get(node).getSetSetMap();
+                               for (Map.Entry mapElement : setSets.entrySet()) {
+                                       Transition transition = (Transition)mapElement.getKey();
+                                       if (checkForConflict(nodeToProcess, node, transition))
+                                               return true;
+                               }
+                       }
+               }
 
-               // Check for a conflict in this transition(currentNode -> nodeToProcess)
-               if (checkForConflict(nodeToProcess))
-                               return true;
+               // Update the parents list for the successors of the current node
+               parents = new HashSet<Node>();
+               parents.add(nodeToProcess);
 
                // Checking if the out set has changed or not(Add its successors to the change list!)
                if (isChanged) {
-                       propagateTheChange(nodeToProcess);
+                       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);
+                       }
                }
       }
 
@@ -115,110 +148,142 @@ public class ConflictTracker extends ListenerAdapter {
   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: "
+                        " to the variable: "+pair.getVarName()+" while App"
+                        +writerMap.get(pair.getVarName())+" is overwriting the value: "
                         +valueMap.get(pair.getVarName())+" to the same variable!";
        System.out.println(message);    
        return message;
   }
 
-  boolean checkForConflict(Node nodeToProcess) {
+  boolean checkForConflict(Node parentNode, Node currentNode, Transition currentTransition) {
+       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
-
-       // Update the valueMap
-       for (int i = 0;i < nodeToProcess.getSetSet().size();i++) {
-               NameValuePair nameValuePair = nodeToProcess.getSetSet().get(i);
-
-               if (valueMap.containsKey(nameValuePair.getVarName())) {
-                       // Check if we have a same writer
-                       if (!writerMap.get(nameValuePair.getVarName()).equals(nameValuePair.getAppNum())) {
-                               // Check if we have a conflict or not
-                               if (!valueMap.get(nameValuePair.getVarName()).equals(nameValuePair.getValue())) {
-                                       errorMessage = createErrorMessage(nameValuePair, valueMap, writerMap);
-                                       return true;
-                               } else { // We have two writers writing the same value
-                                       writerMap.put(nameValuePair.getVarName(), 3); // 3 represents both apps
-                               }       
-                       } else {
-                               // Check if we have more than one value with the same writer
-                               if (!valueMap.get(nameValuePair.getVarName()).equals(nameValuePair.getValue())) {
-                                       valueMap.put(nameValuePair.getVarName(), "twoValue"); // We have one writer writing more than one value in a same event
-                               }
-                       }       
+       HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); //  HashMap from varName to 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);
+           String varName = nameValuePair.getVarName();
+           String value = nameValuePair.getValue();
+           Integer appNum = nameValuePair.getAppNum();
+
+           if (valueMap.containsKey(varName)) {
+               // Check if we have a same writer
+               if (!writerMap.get(varName).equals(appNum)) {
+                       // Check if we have a conflict or not
+                       if (!valueMap.get(varName).equals(value)) {
+                               errorMessage = createErrorMessage(nameValuePair, valueMap, writerMap);
+                               return true;
+                       } else { // We have two writers writing the same value
+                               writerMap.put(varName, 3); // 3 represents both apps
+                       }
                } else {
-                       valueMap.put(nameValuePair.getVarName(), nameValuePair.getValue());
-                       writerMap.put(nameValuePair.getVarName(), nameValuePair.getAppNum());
-               }
-       }
-
-       // 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;
-                               }
+                       // Check if we have more than one value with the same writer
+                       if (!valueMap.get(varName).equals(value)) {
+                               // We have one writer writing more than one value in a same event
+                               valueMap.put(varName, "twoValue");
                        }
                }
+            } else {
+               valueMap.put(varName, value);
+               writerMap.put(varName, appNum);
+            }
        }
 
-       return false;
+       // Check for conflict between outSet and this transition setSet
+       for (NameValuePair i : currentNode.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 and different writers
+                            errorMessage = createErrorMessage(i, valueMap, writerMap);
+                            return true;
+                        }
+                    }
+            }
+       }
+
+       return false;
   }
 
-  boolean updateEdge(Node parentNode, Node currentNode) {
-       ArrayList<NameValuePair> setSet = currentNode.getSetSetMap().get(parentNode);
+  boolean updateTheOutSet(Node parentNode, Node currentNode) {
+       HashMap<Transition, ArrayList<NameValuePair>> setSet = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap();
        HashSet<String> updatedVarNames = new HashSet<String>();
-       HashMap<Integer, String> writerLastValue = new HashMap<Integer, String>();
-
+       Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+       HashMap<String, Integer> lastWriter = currentEdge.getLastWriter();
+       HashMap<String, String> lastValue = currentEdge.getLastValue();
        boolean isChanged = false;
-       
-       if (setSet != null) {
-               for (int i = 0;i < setSet.size();i++) {
-                       updatedVarNames.add(setSet.get(i).getVarName());
-                       writerLastValue.put(setSet.get(i).getAppNum(), setSet.get(i).getValue());
-               }
-       }
+
+        for (Map.Entry mapElement : setSet.entrySet()) {
+            ArrayList<NameValuePair> value = (ArrayList<NameValuePair>)mapElement.getValue();
+  
+            for (int i = 0;i < value.size();i++) {
+                       updatedVarNames.add(value.get(i).getVarName());
+           }
+        }
+
 
        for (NameValuePair i : parentNode.getOutSet()) {
                if (!updatedVarNames.contains(i.getVarName()))
                        isChanged |= currentNode.getOutSet().add(i);
        }
 
-       if (setSet != null) {
-               for (int i = 0;i < setSet.size();i++) {
-                       if (setSet.get(i).getValue().equals(writerLastValue.get(setSet.get(i).getAppNum()))) {
-                               isChanged |= currentNode.getOutSet().add(setSet.get(i));
+
+       for (Map.Entry mapElement : setSet.entrySet()) {
+            ArrayList<NameValuePair> value = (ArrayList<NameValuePair>)mapElement.getValue();
+  
+            for (int i = 0;i < value.size();i++) {
+                       if (value.get(i).getAppNum().equals(lastWriter.get(value.get(i).getVarName())) 
+                           && value.get(i).getValue().equals(lastValue.get(value.get(i).getVarName()))) {
+                               isChanged |= currentNode.getOutSet().add(value.get(i));
                        }
-               }
-       }
+           }
+        }
 
        return isChanged;
   }
 
+  void updateTheEdge(Node currentNode, Transition transition) {
+       if (parentNode.getOutgoingEdges().containsKey(currentNode)) {
+               Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+               if (currentEdge.getSetSetMap().containsKey(transition)) { // Update the transition
+                       if (manual)
+                               currentEdge.getSetSetMap().put(transition, tempSetSet);
+                       else
+                               currentEdge.getSetSetMap().get(transition).addAll(tempSetSet);
+               } else { // Add a new transition
+                       currentEdge.getSetSetMap().put(transition, tempSetSet);
+               }
+        } else {
+               parentNode.getOutgoingEdges().put(currentNode, new Edge(parentNode, currentNode));
+               Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+               currentEdge.getSetSetMap().put(transition, tempSetSet);
+        }
+
+       // Update the last writer and last value for this edge for each varName
+       Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+       ArrayList<NameValuePair> setSet = currentEdge.getSetSetMap().get(transition);
+       for (int i = 0;i < setSet.size();i++) {
+               NameValuePair nameValuePair = setSet.get(i);
+               currentEdge.getLastWriter().put(nameValuePair.getVarName(), nameValuePair.getAppNum());
+               currentEdge.getLastValue().put(nameValuePair.getVarName(), nameValuePair.getValue());
+       }
+  }
+
+  
+
   static class Node {
         Integer id;
        HashSet<Node> predecessors = new HashSet<Node>();
        HashSet<Node> successors = new HashSet<Node>();
        HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
-        ArrayList<NameValuePair> setSet = new ArrayList<NameValuePair>();
-       HashMap<Node, ArrayList<NameValuePair>> setSetMap = new HashMap<Node, ArrayList<NameValuePair>>();
+       HashMap<Node, Edge> outgoingEdges = new HashMap<Node, Edge>();
 
        Node(Integer id) {
          this.id = id;
        }
 
-       void addPredecessor(Node node) {
-         predecessors.add(node);
-       }
-
-       void addSuccessor(Node node) {
-         successors.add(node);
-       }
-
        Integer getId() {
                return id;
        }
@@ -235,13 +300,41 @@ public class ConflictTracker extends ListenerAdapter {
                return outSet;
        }
 
-        ArrayList<NameValuePair> getSetSet() {
-               return setSet;
-        }
+       HashMap<Node, Edge> getOutgoingEdges() {
+               return outgoingEdges;
+       }
+  }
+
+  static class Edge {
+       Node source, destination;
+       HashMap<String, Integer> lastWriter = new HashMap<String, Integer>();
+       HashMap<String, String> lastValue = new HashMap<String, String>();
+       HashMap<Transition, ArrayList<NameValuePair>> setSetMap = new HashMap<Transition, ArrayList<NameValuePair>>();
+
+       Edge(Node source, Node destination) {
+               this.source = source;
+               this.destination = destination;
+       }
+
+       Node getSource() {
+               return source;
+       }
 
-       HashMap<Node, ArrayList<NameValuePair>> getSetSetMap() {
+       Node getDestination() {
+               return destination;
+       }
+
+       HashMap<Transition, ArrayList<NameValuePair>> getSetSetMap() {
                return setSetMap;
        }
+
+       HashMap<String, Integer> getLastWriter() {
+               return lastWriter;
+       }
+
+       HashMap<String, String> getLastValue() {
+               return lastValue;
+       }
   }
 
   static class NameValuePair {
@@ -331,6 +424,7 @@ public class ConflictTracker extends ListenerAdapter {
   @Override
   public void stateAdvanced(Search search) {
     String theEnd = null;
+    Transition transition = search.getTransition();
     id = search.getStateId();
     depth = search.getDepth();
     operation = "forward";
@@ -341,17 +435,15 @@ public class ConflictTracker extends ListenerAdapter {
 
     Node currentNode = nodes.get(id);
 
-    if ((currentNode.getSetSetMap().get(parentNode) == null) || manual)
-       currentNode.getSetSetMap().put(parentNode, new ArrayList<NameValuePair>());
+    // Update the edge based on the current transition
+    updateTheEdge(currentNode, transition);
 
-    // Update the setSet for the edge
-    currentNode.getSetSetMap().get(parentNode).addAll(tempSetSet);
-    parentNode.getSetSet().addAll(tempSetSet);
+    // Reset the temporary variables and flags
     tempSetSet = new ArrayList<NameValuePair>();
     manual = false;
 
-    // Check for the conflict in this edge
-    conflictFound = checkForConflict(parentNode);
+    // Check for the conflict in this transition
+    conflictFound = checkForConflict(parentNode, currentNode, transition);
 
     if (search.isNewState()) {
       detail = "new";
@@ -369,15 +461,15 @@ public class ConflictTracker extends ListenerAdapter {
     // Updating the predecessors for this node
     // Check if parent node is already in successors of the current node or not
     if (!(currentNode.getPredecessors().contains(parentNode)))
-       currentNode.addPredecessor(parentNode);
+       currentNode.getPredecessors().add(parentNode);
 
     // Update the successors for this node
     // Check if current node is already in successors of the parent node or not
     if (!(parentNode.getSuccessors().contains(currentNode)))
-        parentNode.addSuccessor(currentNode);
+        parentNode.getSuccessors().add(currentNode);
 
-    // 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);
+    // 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)