Make updates and not edges have manual property
[jpf-core.git] / src / main / gov / nasa / jpf / listener / ConflictTracker.java
index b28d65bf52a2dd377088091b1bda937f91ec7773..3ec1eea1b9b9d466a0d9db55e5d001e97dbb3de4 100644 (file)
@@ -42,21 +42,20 @@ 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 ArrayList<NameValuePair> tempSetSet = new ArrayList<NameValuePair>();
+  private HashSet<Transition> transitions = new HashSet<Transition>();
+  private ArrayList<Update> currUpdates = new ArrayList<Update>();
   private long timeout;
   private long startTime;
   private Node parentNode = new Node(-2);
   private String operation;
   private String detail;
-  private String errorMessage;
   private int depth;
   private int id;
-  private boolean conflictFound = false;
   private boolean manual = false;
 
   private final String SET_LOCATION_METHOD = "setLocationMode";
   private final String LOCATION_VAR = "locationMode";
-  
+
   public ConflictTracker(Config config, JPF jpf) {
     out = new PrintWriter(System.out, true);
 
@@ -87,329 +86,243 @@ public class ConflictTracker extends ListenerAdapter {
     startTime = System.currentTimeMillis();
   }
 
-  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 the changed set and remove it
-               Node nodeToProcess = changed.iterator().next();
-               changed.remove(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;
-                               }
-                       }
-               }
-
-               // 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) {
-                       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);
-                       }
-               }
-      }
+  void propagateChange(Edge newEdge) {
+    HashSet<Edge> changed = new HashSet<Edge>();
 
-      return false;
-  }
+    // Add the current node to the changed set
+    changed.add(newEdge);
 
-  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!";
-       System.out.println(message);    
-       return message;
-  }
+    while(!changed.isEmpty()) {
+      // Get the first element of the changed set and remove it
+      Edge edgeToProcess = changed.iterator().next();
+      changed.remove(edgeToProcess);
 
-  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 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 {
-                       // 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);
-            }
-       }
-
-       // 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;
+      //If propagating change on edge causes change, enqueue all the target node's out edges
+      if (propagateEdge(edgeToProcess)) {
+        Node dst = edgeToProcess.getDst();
+        for (Edge e : dst.getOutEdges()) {
+          changed.add(e);
+        }
+      }
+    }
   }
 
-  boolean updateTheOutSet(Node parentNode, Node currentNode) {
-       HashMap<Transition, ArrayList<NameValuePair>> setSets = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap();
-       HashSet<String> updatedVarNames = new HashSet<String>();
-       Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
-       HashMap<String, Integer> lastWriter = currentEdge.getLastWriter();
-       HashMap<String, String> lastValue = currentEdge.getLastValue();
-       HashMap<String, Integer> outSetVarMap = new HashMap<String, Integer>();
-       boolean isChanged = false;
-
-        for (Map.Entry mapElement : setSets.entrySet()) {
-            ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
-  
-            for (int i = 0;i < setSet.size();i++) {
-                       updatedVarNames.add(setSet.get(i).getVarName());
-           }
-        }
+  boolean propagateEdge(Edge e) {
+    HashMap<IndexObject, HashSet<Update>> srcUpdates = e.getSrc().getLastUpdates();
+    HashMap<IndexObject, HashSet<Update>> dstUpdates = e.getDst().getLastUpdates();
+    ArrayList<Update> edgeUpdates = e.getUpdates();
+    HashMap<IndexObject, Update> lastupdate = new HashMap<IndexObject, Update>();
+    boolean changed = false;
+    
+    //Go through each update on the current transition
+    for(int i=0; i<edgeUpdates.size(); i++) {
+      Update u = edgeUpdates.get(i);
+      IndexObject io = u.getIndex();
+      HashSet<Update> confupdates = null;
+
+      //See if we have already updated this device attribute
+      if (lastupdate.containsKey(io)) {
+        confupdates = new HashSet<Update>();
+        confupdates.add(lastupdate.get(io));
+      } else if (srcUpdates.containsKey(io)){
+        confupdates = srcUpdates.get(io);
+      }
 
+      //Check for conflict with the appropriate update set if we are not a manual transition
+      if (confupdates != null && !u.isManual()) {
+        for(Update u2: confupdates) {
+          if (conflicts(u, u2)) {
+            throw new RuntimeException(createErrorMessage(u, u2));
+          }
+        }
+      }
+      lastupdate.put(io, u);
+    }
+    for(IndexObject io: srcUpdates.keySet()) {
+      //Only propagate src changes if the transition doesn't update the device attribute
+      if (!lastupdate.containsKey(io)) {
+        //Make sure destination has hashset in map
+        if (!dstUpdates.containsKey(io))
+          dstUpdates.put(io, new HashSet<Update>());
+
+        changed |= dstUpdates.get(io).addAll(srcUpdates.get(io));
+      }
+    }
+    for(IndexObject io: lastupdate.keySet()) {
+      //Make sure destination has hashset in map
+      if (!dstUpdates.containsKey(io))
+        dstUpdates.put(io, new HashSet<Update>());
+      
+      changed |= dstUpdates.get(io).add(lastupdate.get(io));
+    }
+    return changed;
+  }
 
-       for (NameValuePair i : parentNode.getOutSet()) {
-               outSetVarMap.put(i.getVarName(), i.getAppNum());
-               if (!updatedVarNames.contains(i.getVarName()))
-                       isChanged |= currentNode.getOutSet().add(i);
-       }
+  //Method to check for conflicts between two updates
+  //Have conflict if same device, same attribute, different app, different vaalue
+  boolean conflicts(Update u, Update u2) {
+    return (!u.getApp().equals(u2.getApp())) &&
+      u.getDeviceId().equals(u2.getDeviceId()) &&
+      u.getAttribute().equals(u2.getAttribute()) &&
+      (!u.getValue().equals(u2.getValue()));
+  }
+  
+  String createErrorMessage(Update u, Update u2) {
+    String message = "Conflict found between the two apps. App"+u.getApp()+
+                    " has written the value: "+u.getValue()+
+      " to the attribute: "+u.getAttribute()+" while App"
+      +u2.getApp()+" is writing the value: "
+      +u2.getValue()+" to the same variable!";
+    System.out.println(message);       
+    return message;
+  }
 
+  Edge createEdge(Node parent, Node current, Transition transition) {
+    //Check if this transition is explored.  If so, just skip everything
+    if (transitions.contains(transition))
+      return null;
 
-       for (Map.Entry mapElement : setSets.entrySet()) {
-            ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
-  
-            for (int i = 0;i < setSet.size();i++) {
-                       String varName = setSet.get(i).getVarName();
-                       Integer writer = lastWriter.get(varName);
-                       String value = lastValue.get(varName);
-
-                       if (setSet.get(i).getAppNum().equals(writer) 
-                           && setSet.get(i).getValue().equals(value)) {
-                               if (outSetVarMap.containsKey(varName)) {
-                                       Integer hashCode = outSetVarMap.get(varName).hashCode() * 31 +
-                                                          varName.hashCode();
-                                       currentNode.getOutSet().remove(hashCode);
-                               }
-                               isChanged |= currentNode.getOutSet().add(setSet.get(i));
-                       }
-           }
-        }
+    //Create edge
+    Edge e = new Edge(parent, current, transition, currUpdates);
+    parent.addOutEdge(e);
 
-       return isChanged;
+    //Mark transition as explored
+    transitions.add(transition);
+    return e;
   }
 
-  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);
-        }
+  static class Node {
+    Integer id;
+    Vector<Edge> outEdges = new Vector<Edge>();
+    HashMap<IndexObject, HashSet<Update>> lastUpdates = new HashMap<IndexObject,  HashSet<Update>>();
+    
+    Node(Integer id) {
+      this.id = id;
+    }
 
-       // 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());
-       }
-  }
+    Integer getId() {
+      return id;
+    }
 
-  
+    Vector<Edge> getOutEdges() {
+      return outEdges;
+    }
 
-  static class Node {
-        Integer id;
-       HashSet<Node> predecessors = new HashSet<Node>();
-       HashSet<Node> successors = new HashSet<Node>();
-       HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
-       HashMap<Node, Edge> outgoingEdges = new HashMap<Node, Edge>();
-
-       Node(Integer id) {
-         this.id = id;
-       }
-
-       Integer getId() {
-               return id;
-       }
-
-       HashSet<Node> getPredecessors() {
-               return predecessors;
-       }
-
-       HashSet<Node> getSuccessors() {
-               return successors;
-       }
-
-       HashSet<NameValuePair> getOutSet() {
-               return outSet;
-       }
-
-       HashMap<Node, Edge> getOutgoingEdges() {
-               return outgoingEdges;
-       }
+    void addOutEdge(Edge e) {
+      outEdges.add(e);
+    }
+    
+    HashMap<IndexObject, HashSet<Update>> getLastUpdates() {
+      return lastUpdates;
+    }
   }
 
+  //Each Edge corresponds to a transition
   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;
-       }
-
-       Node getDestination() {
-               return destination;
-       }
-
-       HashMap<Transition, ArrayList<NameValuePair>> getSetSetMap() {
-               return setSetMap;
-       }
-
-       HashMap<String, Integer> getLastWriter() {
-               return lastWriter;
-       }
-
-       HashMap<String, String> getLastValue() {
-               return lastValue;
-       }
+    Node source, destination;
+    Transition transition;
+    ArrayList<Update> updates = new ArrayList<Update>();
+    
+    Edge(Node src, Node dst, Transition t, ArrayList<Update> _updates) {
+      this.source = src;
+      this.destination = dst;
+      this.transition = t;
+      this.updates.addAll(_updates);
+    }
+
+    Node getSrc() {
+      return source;
+    }
+
+    Node getDst() {
+      return destination;
+    }
+
+    Transition getTransition() {
+      return transition;
+    }
+
+    ArrayList<Update> getUpdates() {
+      return updates;
+    }
   }
 
-  static class NameValuePair {
-       Integer appNum;
-       String value;
-       String varName;
-       boolean isManual;
-
-       NameValuePair(Integer appNum, String value, String varName, boolean isManual) {
-               this.appNum = appNum;
-               this.value = value;
-               this.varName = varName;
-               this.isManual = isManual;
-       }
-
-       void setAppNum(Integer appNum) {
-               this.appNum = appNum;
-       }
-
-       void setValue(String value) {
-               this.value = value;
-       }
-
-       void setVarName(String varName) {
-               this.varName = varName;
-       }
-
-        void setIsManual(String varName) {
-               this.isManual = isManual;
-       }
-
-       Integer getAppNum() {
-               return appNum;
-       }
-
-       String getValue() {
-               return value;
-       }
-
-       String getVarName() {
-               return varName;
-       }
-
-       boolean getIsManual() {
-               return isManual;
-       }
-
-       @Override
-       public boolean equals(Object o) {
-      if (o instanceof NameValuePair) {
-        NameValuePair other = (NameValuePair) o;
-        if (varName.equals(other.getVarName()))
-          return appNum.equals(other.getAppNum());
-      }
-      return false;
-       }
+  static class Update {
+    String appName;
+    String deviceId;
+    String attribute;
+    String value;
+    boolean ismanual;
+    
+    Update(String _appName, String _deviceId, String _attribute, String _value, boolean _ismanual) {
+      this.appName = _appName;
+      this.deviceId = _deviceId;
+      this.attribute = _attribute;
+      this.value = _value;
+      this.ismanual = _ismanual;
+    }
+
+    boolean isManual() {
+      return ismanual;
+    }
+    
+    String getApp() {
+      return appName;
+    }
+
+    String getDeviceId() {
+      return deviceId;
+    }
+
+    String getAttribute() {
+      return attribute;
+    }
+    
+    String getValue() {
+      return value;
+    }
+
+    //Gets an index object for indexing updates by just device and attribute
+    IndexObject getIndex() {
+      return new IndexObject(this);
+    }
+
+    public boolean equals(Object o) {
+      if (!(o instanceof Update))
+        return false;
+      Update u=(Update)o;
+      return (getDeviceId().equals(u.getDeviceId()) &&
+              getAttribute().equals(u.getAttribute()) &&
+              getApp().equals(u.getApp()) &&
+              getValue().equals(u.getValue()));
+    }
 
-       @Override
-       public int hashCode() {
-               return appNum.hashCode() * 31 + varName.hashCode();
-       }
+    public int hashCode() {
+      return (getDeviceId().hashCode() << 3) ^
+        (getAttribute().hashCode() << 2) ^
+        (getApp().hashCode() << 1) ^
+        getValue().hashCode();
+    }
   }
 
+  static class IndexObject {
+    Update u;
+    IndexObject(Update _u) {
+      this.u = _u;
+    }
+    
+    public boolean equals(Object o) {
+      if (!(o instanceof IndexObject))
+        return false;
+      IndexObject io=(IndexObject)o;
+      return (u.getDeviceId().equals(io.u.getDeviceId()) &&
+              u.getAttribute().equals(io.u.getAttribute()));
+    }
+    public int hashCode() {
+      return (u.getDeviceId().hashCode() << 1) ^ u.getAttribute().hashCode();
+    }
+  }
+  
   @Override
   public void stateRestored(Search search) {
     id = search.getStateId();
@@ -420,18 +333,19 @@ public class ConflictTracker extends ListenerAdapter {
     out.println("The state is restored to state with id: "+id+", depth: "+depth);
   
     // Update the parent node
-    if (nodes.containsKey(id)) {
-         parentNode = nodes.get(id);
-    } else {
-         parentNode = new Node(id);
-    }
+    parentNode = getNode(id);
   }
 
   @Override
   public void searchStarted(Search search) {
     out.println("----------------------------------- search started");
   }
+
+  private Node getNode(Integer id) {
+    if (!nodes.containsKey(id))
+      nodes.put(id, new Node(id));
+    return nodes.get(id);
+  }
 
   @Override
   public void stateAdvanced(Search search) {
@@ -442,20 +356,18 @@ public class ConflictTracker extends ListenerAdapter {
     operation = "forward";
 
     // Add the node to the list of nodes
-    if (nodes.get(id) == null)
-       nodes.put(id, new Node(id));
+    Node currentNode = getNode(id);
 
-    Node currentNode = nodes.get(id);
-
-    // Update the edge based on the current transition
-    updateTheEdge(currentNode, transition);
+    // Create an edge based on the current transition
+    Edge newEdge = createEdge(parentNode, currentNode, transition);
 
     // Reset the temporary variables and flags
-    tempSetSet = new ArrayList<NameValuePair>();
+    currUpdates.clear();
     manual = false;
 
-    // Check for the conflict in this transition
-    conflictFound = checkForConflict(parentNode, currentNode, transition);
+    // If we have a new Edge, check for conflicts
+    if (newEdge != null)
+      propagateChange(newEdge);
 
     if (search.isNewState()) {
       detail = "new";
@@ -470,36 +382,8 @@ public class ConflictTracker extends ListenerAdapter {
 
     out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
     
-    // 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.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.getSuccessors().add(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()) {
-               HashMap<Transition, ArrayList<NameValuePair>> setSets = currentNode.getOutgoingEdges().get(node).getSetSetMap();
-               for (Map.Entry mapElement : setSets.entrySet()) {
-                       Transition currentTransition = (Transition)mapElement.getKey();
-                       conflictFound = conflictFound || checkForConflict(currentNode, node, currentTransition);
-               }
-       }
-       conflictFound = conflictFound || propagateTheChange(currentNode);
-    }
     // Update the parent node
-    if (nodes.containsKey(id)) {
-         parentNode = nodes.get(id);
-    } else {
-         parentNode = new Node(id);
-    }
+    parentNode = currentNode;
   }
 
   @Override
@@ -512,11 +396,7 @@ public class ConflictTracker extends ListenerAdapter {
     out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
 
     // Update the parent node
-    if (nodes.containsKey(id)) {
-         parentNode = nodes.get(id);
-    } else {
-         parentNode = new Node(id);
-    }
+    parentNode = getNode(id);
   }
 
   @Override
@@ -658,13 +538,9 @@ public class ConflictTracker extends ListenerAdapter {
     return null;
   }
 
-  private void writeWriterAndValue(String writer, String value, String var) {
-    // Update the temporary Set set.
-    NameValuePair temp = new NameValuePair(1, value, var, manual);
-    if (writer.equals("App2"))
-       temp = new NameValuePair(2, value, var, manual);
-    
-    tempSetSet.add(temp);
+  private void writeWriterAndValue(String writer, String attribute, String value) {
+    Update u = new Update(writer, "DEVICE", attribute, value, manual);
+    currUpdates.add(u);
   }
 
   @Override
@@ -678,47 +554,40 @@ public class ConflictTracker extends ListenerAdapter {
       }
     }
 
-    if (conflictFound) {
-      StringBuilder sb = new StringBuilder();
-      sb.append(errorMessage);
-      Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
-      ti.setNextPC(nextIns);
+    if (conflictSet.contains(LOCATION_VAR)) {
+      MethodInfo mi = executedInsn.getMethodInfo();
+      // Find the last load before return and get the value here
+      if (mi.getName().equals(SET_LOCATION_METHOD) &&
+          executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) {
+        byte type  = getType(ti, executedInsn);
+        String value = getValue(ti, executedInsn, type);
+        
+        // Extract the writer app name
+        ClassInfo ci = mi.getClassInfo();
+        String writer = ci.getName();
+        
+        // Update the temporary Set set.
+        writeWriterAndValue(writer, LOCATION_VAR, value);
+      }
     } else {
-      if (conflictSet.contains(LOCATION_VAR)) {
-        MethodInfo mi = executedInsn.getMethodInfo();
-        // Find the last load before return and get the value here
-        if (mi.getName().equals(SET_LOCATION_METHOD) &&
-                executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) {
-          byte type  = getType(ti, executedInsn);
-          String value = getValue(ti, executedInsn, type);
-
-          // Extract the writer app name
-          ClassInfo ci = mi.getClassInfo();
-          String writer = ci.getName();
-
-          // Update the temporary Set set.
-          writeWriterAndValue(writer, value, LOCATION_VAR);
-        }
-      } else {
-        if (executedInsn instanceof WriteInstruction) {
-          String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
-
-          for (String var : conflictSet) {
-            if (varId.contains(var)) {
-              // Get variable info
-              byte type = getType(ti, executedInsn);
-              String value = getValue(ti, executedInsn, type);
-              String writer = getWriter(ti.getStack(), appSet);
-              // Just return if the writer is not one of the listed apps in the .jpf file
-              if (writer == null)
-                return;
-
-              if (getWriter(ti.getStack(), manualSet) != null)
-                manual = true;
-
-              // Update the temporary Set set.
-              writeWriterAndValue(writer, value, var);
-            }
+      if (executedInsn instanceof WriteInstruction) {
+        String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
+        
+        for (String var : conflictSet) {
+          if (varId.contains(var)) {
+            // Get variable info
+            byte type = getType(ti, executedInsn);
+            String value = getValue(ti, executedInsn, type);
+            String writer = getWriter(ti.getStack(), appSet);
+            // Just return if the writer is not one of the listed apps in the .jpf file
+            if (writer == null)
+              return;
+            
+            if (getWriter(ti.getStack(), manualSet) != null)
+              manual = true;
+            
+            // Update the current updates
+            writeWriterAndValue(writer, var, value);
           }
         }
       }