From: amiraj Date: Wed, 9 Oct 2019 22:00:34 +0000 (-0700) Subject: Make changes to ConflictTracker.java + Adding having different variables feature X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=f1ef12fe48a0c24f8e5c4c6d90cee34316ce60d8;p=jpf-core.git Make changes to ConflictTracker.java + Adding having different variables feature --- diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index 307463e..c3e0e2f 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -42,19 +42,16 @@ public class ConflictTracker extends ListenerAdapter { private final HashSet conflictSet = new HashSet(); // Variables we want to track private final HashSet appSet = new HashSet(); // Apps we want to find their conflicts private final HashMap nodes = new HashMap(); // Nodes of a graph - private final DataSet tempSetSet = new DataSet(false, "NA", false, "NA"); + private final HashSet tempSetSet = new HashSet(); private long timeout; private long startTime; - volatile private Node parentNode = new Node(-2); - volatile private String operation; - volatile private String detail; - volatile private int depth; - volatile private int id; - volatile private boolean conflictFound = false; - volatile private boolean isSet = false; - Transition transition; - Object annotation; - String label; + private Node parentNode = new Node(-2); + private String operation; + private String detail; + private int depth; + private int id; + private boolean conflictFound = false; + private boolean isSet = false; public ConflictTracker(Config config, JPF jpf) { @@ -79,101 +76,104 @@ public class ConflictTracker extends ListenerAdapter { startTime = System.currentTimeMillis(); } - public void setOutSet(Node currentNode) { - DataList inSetApp1List = currentNode.getInSet().getApp1DataList(); // Store the app1List of inSet of current node to temp data set - DataList inSetApp2List = currentNode.getInSet().getApp2DataList(); // Store the app2List of inSet of current node to temp data set - DataList setSetApp1List = currentNode.getSetSet().getApp1DataList(); // Store the app1List of setSet of current node to temp data set - DataList setSetApp2List = currentNode.getSetSet().getApp2DataList(); // Store the app2List of setSet of current node to temp data set - DataSet outSetTemp = currentNode.getOutSet(); // Store the outSet of current node to temp data set - - if ((setSetApp1List.getAppSet())&&(setSetApp2List.getAppSet())) { - // App1 & App2 are writers - outSetTemp.setApp1DataList(setSetApp1List.getAppSet(), setSetApp1List.getValue()); - outSetTemp.setApp2DataList(setSetApp2List.getAppSet(), setSetApp2List.getValue()); - } else if (setSetApp2List.getAppSet()) { - // App1 is a writer - outSetTemp.setApp1DataList(setSetApp1List.getAppSet(), setSetApp1List.getValue()); - outSetTemp.setApp2DataList(inSetApp2List.getAppSet(), inSetApp2List.getValue()); - } else if (setSetApp2List.getAppSet()) { - // App2 is a writer - outSetTemp.setApp1DataList(inSetApp1List.getAppSet(),inSetApp1List.getValue()); - outSetTemp.setApp2DataList(setSetApp2List.getAppSet(), setSetApp2List.getValue()); - } else { - // No writer for this node => outSet = inSet - outSetTemp.setApp1DataList(inSetApp1List.getAppSet(), inSetApp1List.getValue()); - outSetTemp.setApp2DataList(inSetApp2List.getAppSet(), inSetApp2List.getValue()); + void propagateTheChange(Node currentNode) { + HashSet changed = new HashSet(currentNode.getSuccessors()); + boolean isChanged; + + 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 + isChanged = updateSets(nodeToProcess); + + // Check for a conflict + conflictFound = checkForConflict(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); + } + } } } - public void setInSet(Node currentNode) { - for (Node i : currentNode.getPredecessors()) { - // Check to see if dataList1 of predNode(i) is valid or not: if valid get its value - if (i.getOutSet().getApp1DataList().getAppSet()) { - currentNode.getInSet().setApp1DataList(true, i.getOutSet().getApp1DataList().getValue()); + boolean setOutSet(Node currentNode) { + boolean isChanged = false; + HashMap outSet = new HashMap(); + + // Store the outSet of current node to HashMap to help for the search in O(n) + for (NameValuePair i : currentNode.getOutSet()) { + outSet.put(i, i.getValue()); + } + + // Update based on inSet + for (NameValuePair i : currentNode.getInSet()) { + if (currentNode.getOutSet().contains(i)) { + if (outSet.get(i) != i.getValue()) + isChanged = true; + currentNode.getOutSet().remove(i); + } else { + isChanged = true; } + currentNode.getOutSet().add(i); + } - // Check to see if dataList2 of predNode(i) is valid or not: if valid get its value - if (i.getOutSet().getApp2DataList().getAppSet()) { - currentNode.getInSet().setApp2DataList(true, i.getOutSet().getApp2DataList().getValue()); + // Overwrite the outSet based on setSet if we have a writer + for (NameValuePair i : currentNode.getSetSet()) { + if (currentNode.getOutSet().contains(i)) { + if (outSet.get(i) != i.getValue()) + isChanged = true; + currentNode.getOutSet().remove(i); + } else { + isChanged = true; } - } + currentNode.getOutSet().add(i); + } + + return isChanged; } - boolean checkOutSetChange(Node currentNode, DataSet tempOutSet) { - DataList outSetApp1List = currentNode.getOutSet().getApp1DataList(); // Store the app1List of inSet of current node to temp data set - DataList outSetApp2List = currentNode.getOutSet().getApp2DataList(); // Store the app2List of inSet of current node to temp data set - DataList tempSetApp1List = tempOutSet.getApp1DataList(); // Store the app1List of tempOutSet of current node to temp data set - DataList tempSetApp2List = tempOutSet.getApp2DataList(); // Store the app1List of tempOutSet of current node to temp data set - - // Return 1 if the outSet has changed! - return ((outSetApp1List.getAppSet() != tempSetApp1List.getAppSet())|| - !(outSetApp1List.getValue().equals(tempSetApp1List.getValue()))|| - (outSetApp2List.getAppSet() != tempSetApp2List.getAppSet())|| - !(outSetApp2List.getValue().equals(tempSetApp2List.getValue()))); + void setInSet(Node currentNode) { + for (Node i : currentNode.getPredecessors()) { + currentNode.getInSet().addAll(i.getOutSet()); + } } - public void checkForConflict(Node currentNode) { - DataList outSetApp1List = currentNode.getOutSet().getApp1DataList(); // Store the app1List of inSet of current node to temp data set - DataList outSetApp2List = currentNode.getOutSet().getApp2DataList(); // Store the app2List of inSet of current node to temp data set + boolean checkForConflict(Node currentNode) { + HashMap varNameMap = new HashMap(); - if ((outSetApp1List.getAppSet() == true)&&(outSetApp2List.getAppSet() == true)) { - // Both apps have set the device - if (!(outSetApp1List.getValue().equals(outSetApp2List.getValue()))) { - // Values set by the apps are not the same, and we have a conflict! - conflictFound = true; + for (NameValuePair i : currentNode.getOutSet()) { + if (varNameMap.containsKey(i.getVarName())) { + if (varNameMap.get(i) != i.getValue()) { + return true; + } + } else { + varNameMap.put(i.getVarName(), i.getValue()); } } - } - - public DataSet updateSets(Node currentNode) { - // Empty the in set of the node - currentNode.emptyInSet(); - DataList outSetApp1List = currentNode.getOutSet().getApp1DataList(); - DataList outSetApp2List = currentNode.getOutSet().getApp2DataList(); - - // Store the out set of this state to the temporary data set - DataSet tempOutSet = new DataSet(outSetApp1List.getAppSet(), - outSetApp1List.getValue(), - outSetApp2List.getAppSet(), - outSetApp2List.getValue()); + return false; + } + boolean updateSets(Node currentNode) { // Set input set according to output set of pred states of current state setInSet(currentNode); - // Set dataLists of outSet to dataLists of setSet if it is valid, otherwise to dataLists of inSet - setOutSet(currentNode); - - return tempOutSet; + // Set outSet according to inSet, and setSet of current node, check if there is a change + return setOutSet(currentNode); } - class Node { + static class Node { Integer id; - ArrayList predecessors = new ArrayList(); - ArrayList successors = new ArrayList(); - DataSet inSet = new DataSet(false, "NA", false, "NA"); - DataSet setSet = new DataSet(false, "NA", false, "NA"); - DataSet outSet = new DataSet(false, "NA", false, "NA"); + HashSet predecessors = new HashSet(); + HashSet successors = new HashSet(); + HashSet inSet = new HashSet(); + HashSet setSet = new HashSet(); + HashSet outSet = new HashSet(); Node(Integer id) { this.id = id; @@ -187,109 +187,83 @@ public class ConflictTracker extends ListenerAdapter { successors.add(node); } - void emptyInSet() { - this.inSet = new DataSet(false, "NA", false, "NA"); - } - - void setInSet(DataSet inSet) { - DataList inSetApp1List = inSet.getApp1DataList(); - DataList inSetApp2List = inSet.getApp2DataList(); - this.inSet.setApp1DataList(inSetApp1List.getAppSet(), inSetApp1List.getValue()); - this.inSet.setApp2DataList(inSetApp2List.getAppSet(), inSetApp2List.getValue()); - } - - void setSetSet(DataSet setSet) { - DataList setSetApp1List = setSet.getApp1DataList(); - DataList setSetApp2List = setSet.getApp2DataList(); - this.setSet.setApp1DataList(setSetApp1List.getAppSet(), setSetApp1List.getValue()); - this.setSet.setApp2DataList(setSetApp2List.getAppSet(), setSetApp2List.getValue()); - } - - void setOutSet(DataSet outSet) { - DataList outSetApp1List = outSet.getApp1DataList(); - DataList outSetApp2List = outSet.getApp2DataList(); - this.outSet.setApp1DataList(outSetApp1List.getAppSet(), outSetApp1List.getValue()); - this.outSet.setApp2DataList(outSetApp2List.getAppSet(), outSetApp2List.getValue()); + void setSetSet(HashSet setSet) { + this.setSet.addAll(setSet); } Integer getId() { return id; } - ArrayList getPredecessors() { + HashSet getPredecessors() { return predecessors; } - ArrayList getSuccessors() { + HashSet getSuccessors() { return successors; } - DataSet getInSet() { + HashSet getInSet() { return inSet; } - DataSet getOutSet() { - return outSet; + HashSet getSetSet() { + return setSet; } - DataSet getSetSet() { - return setSet; + HashSet getOutSet() { + return outSet; } } - class DataList { - boolean appSet; + static class NameValuePair { + Integer appNum; String value; + String varName; - DataList(boolean appSet, String value) { - this.appSet = appSet; + NameValuePair(Integer appNum, String value, String varName) { + this.appNum = appNum; this.value = value; + this.varName = varName; } - void setAppSet(boolean appSet) { - this.appSet = appSet; + void setAppNum(Integer appNum) { + this.appNum = appNum; } void setValue(String value) { this.value = value; } - boolean getAppSet() { - return appSet; + void setVarName(String varName) { + this.varName = varName; } - String getValue() { - return value; - } - } - - class DataSet { - DataList app1DataList = new DataList(false, "NA"); - DataList app2DataList = new DataList(false, "NA"); - - DataSet(boolean app1Set, String app1Value, boolean app2Set, String app2Value) { - app1DataList.setAppSet(app1Set); - app1DataList.setValue(app1Value); - app2DataList.setAppSet(app2Set); - app2DataList.setValue(app2Value); + Integer getAppNum() { + return appNum; } - void setApp1DataList(boolean appSet, String value) { - app1DataList.setAppSet(appSet); - app1DataList.setValue(value); + String getValue() { + return value; } - void setApp2DataList(boolean appSet, String value) { - app2DataList.setAppSet(appSet); - app2DataList.setValue(value); + String getVarName() { + return varName; } - DataList getApp1DataList() { - return app1DataList; + @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; } - DataList getApp2DataList() { - return app2DataList; + @Override + public int hashCode() { + return appNum.hashCode() * 31 + varName.hashCode(); } } @@ -323,14 +297,14 @@ public class ConflictTracker extends ListenerAdapter { nodes.put(id, new Node(id)); Node currentNode = nodes.get(id); + // Update the setSet for this new node + if (isSet) { + currentNode.setSetSet(tempSetSet); + isSet = false; + } + if (search.isNewState()) { - // Add this new node detail = "new"; - // Update the setSet for this new node - if (isSet) { - currentNode.setSetSet(tempSetSet); - isSet = false; - } } else { detail = "visited"; } @@ -352,37 +326,16 @@ public class ConflictTracker extends ListenerAdapter { if (!(parentNode.getSuccessors().contains(currentNode))) parentNode.addSuccessor(currentNode); - // Update the sets, store the outSet to temp before its changes - DataSet tempOutSet = updateSets(currentNode); + // Update the sets, check if the outSet is changed or not + boolean isChanged = updateSets(currentNode); // Check for a conflict - checkForConflict(currentNode); + conflictFound = checkForConflict(currentNode); // Check if the outSet of this state has changed, update all of its successors' sets if any - if (checkOutSetChange(currentNode, tempOutSet)) { - ArrayList changed = new ArrayList(currentNode.getSuccessors()); - while(!changed.isEmpty()) { - // Get a random node inside the changed list and remove it from the list - Integer rnd = new Random().nextInt(changed.size()); - Node nodeToProcess = changed.get(rnd); - changed.remove(nodeToProcess); - - // Update the sets, store the outSet to temp before its changes - tempOutSet = updateSets(nodeToProcess); - - // Check for a conflict - checkForConflict(nodeToProcess); - - // Checking if the out set has changed or not(Add its successors to the change list!) - if (checkOutSetChange(nodeToProcess, tempOutSet)) { - for (Node i : nodeToProcess.getSuccessors()) { - if (!changed.contains(i)) - changed.add(i); - } - } - } - } - + if (isChanged) + propagateTheChange(currentNode); + // Update the parent node parentNode = new Node(id); } @@ -573,10 +526,10 @@ public class ConflictTracker extends ListenerAdapter { // Update the temporary Set set. if (writer.equals("App1")) - tempSetSet.setApp1DataList(true, value); + tempSetSet.add(new NameValuePair(1, value, var)); else if (writer.equals("App2")) - tempSetSet.setApp2DataList(true, value); - // Set isSet to 1 + tempSetSet.add(new NameValuePair(2, value, var)); + // Set isSet to 1 isSet = true; }