Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 1aa50b92ef37ed2aad2b1b126e46fd1f706e5f40..435a29a0a7505850384781699ab9d9b1d3cab8b7 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -43,7 +43,7 @@ public class ConflictTracker extends ListenerAdapter {
   private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
   private final HashSet<String> manualSet = new HashSet<String>(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions
   private final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph
-  private HashSet<NameValuePair> tempSetSet = new HashSet<NameValuePair>();
+  private ArrayList<NameValuePair> tempSetSet = new ArrayList<NameValuePair>();
   private long timeout;
   private long startTime;
   private Node parentNode = new Node(-2);
@@ -53,7 +53,6 @@ public class ConflictTracker extends ListenerAdapter {
   private int depth;
   private int id;
   private boolean conflictFound = false;
-  private boolean isSet = false;
   private boolean manual = false;
 
   private final String SET_LOCATION_METHOD = "setLocationMode";
@@ -129,21 +128,29 @@ public class ConflictTracker extends ListenerAdapter {
        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 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()));
+       // 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
+                               }
+                       }       
                } else {
-                       valueMap.put(i.getVarName(), i.getValue());
-                       writerMap.put(i.getVarName(), i.getAppNum());
+                       valueMap.put(nameValuePair.getVarName(), nameValuePair.getValue());
+                       writerMap.put(nameValuePair.getVarName(), nameValuePair.getAppNum());
                }
        }
 
@@ -165,14 +172,14 @@ public class ConflictTracker extends ListenerAdapter {
   }
 
   boolean updateEdge(Node parentNode, Node currentNode) {
-       HashSet<NameValuePair> setSet = currentNode.getSetSetMap().get(parentNode);
+       ArrayList<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;
 
-       for (NameValuePair i : setSet) {
-               updatedVarNames.add(i.getVarName());
-               lastWriter.put(i.getVarName(), i.getAppNum());
+       for (int i = 0;i < setSet.size();i++) {
+               updatedVarNames.add(setSet.get(i).getVarName());
+               lastWriter.put(setSet.get(i).getVarName(), setSet.get(i).getAppNum());
        }
 
        for (NameValuePair i : parentNode.getOutSet()) {
@@ -180,41 +187,43 @@ public class ConflictTracker extends ListenerAdapter {
                        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);
+       for (int i = 0;i < setSet.size();i++) {
+               if (setSet.get(i).getAppNum().equals(lastWriter.get(setSet.get(i).getVarName()))) // Add the last writer of each variable to outSet
+                       isChanged |= currentNode.getOutSet().add(setSet.get(i));
        }
 
        return isChanged;
   }
 
   static class Node {
-       Integer id;
+        Integer id;
        HashSet<Node> predecessors = new HashSet<Node>();
        HashSet<Node> successors = new HashSet<Node>();
-       HashSet<NameValuePair> setSet = new HashSet<NameValuePair>();
        HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
-       HashMap<Node, HashSet<NameValuePair>> setSetMap = new HashMap<Node, HashSet<NameValuePair>>();
+       HashMap<Node, ArrayList<NameValuePair>> setSetMap = new HashMap<Node, ArrayList<NameValuePair>>();
+       ArrayList<NameValuePair> setSet = new ArrayList<NameValuePair>();
 
 
        Node(Integer id) {
-               this.id = id;
+         this.id = id;
        }
 
        void addPredecessor(Node node) {
-               predecessors.add(node);
+         predecessors.add(node);
        }
 
        void addSuccessor(Node node) {
-               successors.add(node);
+         successors.add(node);
        }
 
-       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()));
-             }
+       void setSetSet(ArrayList<NameValuePair> setSet, boolean isManual) {
+         if (isManual)
+           this.setSet = new ArrayList<NameValuePair>();
+
+         for (int i = 0;i < setSet.size();i++) {
+           this.setSet.add(new NameValuePair(setSet.get(i).getAppNum(), setSet.get(i).getValue(), 
+                                             setSet.get(i).getVarName(), setSet.get(i).getIsManual()));
+           }
        }
 
        Integer getId() {
@@ -229,7 +238,7 @@ public class ConflictTracker extends ListenerAdapter {
                return successors;
        }
 
-       HashSet<NameValuePair> getSetSet() {
+       ArrayList<NameValuePair> getSetSet() {
                return setSet;
        }
 
@@ -237,7 +246,7 @@ public class ConflictTracker extends ListenerAdapter {
                return outSet;
        }
 
-       HashMap<Node, HashSet<NameValuePair>> getSetSetMap() {
+       HashMap<Node, ArrayList<NameValuePair>> getSetSetMap() {
                return setSetMap;
        }
   }
@@ -341,12 +350,9 @@ public class ConflictTracker extends ListenerAdapter {
     Node currentNode = nodes.get(id);
 
     // Update the setSet for this new node
-    if (isSet) {
-      currentNode.setSetSet(tempSetSet, manual);
-      tempSetSet = new HashSet<NameValuePair>(); 
-      isSet = false;
-      manual = false;
-    }
+    currentNode.setSetSet(tempSetSet, manual);
+    tempSetSet = new ArrayList<NameValuePair>(); 
+    manual = false;
 
     if (search.isNewState()) {
       detail = "new";
@@ -554,11 +560,7 @@ public class ConflictTracker extends ListenerAdapter {
     if (writer.equals("App2"))
        temp = new NameValuePair(2, value, var, manual);
     
-    if (tempSetSet.contains(temp))
-       tempSetSet.remove(temp);
     tempSetSet.add(temp);
-    // Set isSet to true
-    isSet = true;
   }
 
   @Override