From 6afd3f44baaefabd44cdf38486f96fa2f89a6b84 Mon Sep 17 00:00:00 2001 From: amiraj Date: Wed, 6 Nov 2019 16:06:15 -0800 Subject: [PATCH] Make some changes in ConflictTracker listener. --- .../nasa/jpf/listener/ConflictTracker.java | 96 ++++++++++--------- 1 file changed, 49 insertions(+), 47 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index 1aa50b9..435a29a 100644 --- 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 appSet = new HashSet(); // Apps we want to find their conflicts private final HashSet manualSet = new HashSet(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions private final HashMap nodes = new HashMap(); // Nodes of a graph - private HashSet tempSetSet = new HashSet(); + private ArrayList tempSetSet = new ArrayList(); 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 valueMap = new HashMap(); // HashMap from varName to value HashMap writerMap = new HashMap(); // 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 setSet = currentNode.getSetSetMap().get(parentNode); + ArrayList setSet = currentNode.getSetSetMap().get(parentNode); HashSet updatedVarNames = new HashSet(); HashMap lastWriter = new HashMap(); // 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 predecessors = new HashSet(); HashSet successors = new HashSet(); - HashSet setSet = new HashSet(); HashSet outSet = new HashSet(); - HashMap> setSetMap = new HashMap>(); + HashMap> setSetMap = new HashMap>(); + ArrayList setSet = new ArrayList(); 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 setSet, boolean isManual) { - if (isManual) - this.setSet = new HashSet(); - for (NameValuePair i : setSet) { - this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual())); - } + void setSetSet(ArrayList setSet, boolean isManual) { + if (isManual) + this.setSet = new ArrayList(); + + 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 getSetSet() { + ArrayList getSetSet() { return setSet; } @@ -237,7 +246,7 @@ public class ConflictTracker extends ListenerAdapter { return outSet; } - HashMap> getSetSetMap() { + HashMap> 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(); - isSet = false; - manual = false; - } + currentNode.setSetSet(tempSetSet, manual); + tempSetSet = new ArrayList(); + 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 -- 2.34.1