From 1d88791c7bd60ed5557623eab7f4c0963b44f826 Mon Sep 17 00:00:00 2001 From: amiraj Date: Sat, 5 Oct 2019 10:11:40 -0700 Subject: [PATCH] Make the program cleaner, easy to understand --- .../nasa/jpf/listener/ConflictTracker.java | 433 ++++++++++-------- 1 file changed, 238 insertions(+), 195 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index d1efe46..8d5d1c4 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -41,17 +41,15 @@ public class ConflictTracker extends ListenerAdapter { private final PrintWriter out; 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> predSet = new HashMap>(); - private final HashMap> succSet = new HashMap>(); - private final HashMap setSet = new HashMap(); - private final HashMap inSet = new HashMap(); - private final HashMap outSet = new HashMap(); + private final HashMap nodes = new HashMap(); // Nodes of a graph + private final DataSet tempSetSet = new DataSet(false, "NA", false, "NA"); + 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 int parentId = -2; - volatile private int conflictFound = 0; + volatile private boolean conflictFound = false; + volatile private boolean isSet = false; Transition transition; Object annotation; String label; @@ -76,22 +74,168 @@ public class ConflictTracker extends ListenerAdapter { } } + public void setOutSet(Node currentNode) { + if ((currentNode.getSetSet().getDataList1().getAppSet())&&(currentNode.getSetSet().getDataList2().getAppSet())) { //App1 & App2 are writers + currentNode.getOutSet().setDataList1(currentNode.getSetSet().getDataList1().getAppSet(), currentNode.getSetSet().getDataList1().getValue()); + currentNode.getOutSet().setDataList2(currentNode.getSetSet().getDataList2().getAppSet(), currentNode.getSetSet().getDataList2().getValue()); + } else if (currentNode.getSetSet().getDataList1().getAppSet()) { //App1 is a writer + currentNode.getOutSet().setDataList1(currentNode.getSetSet().getDataList1().getAppSet(), currentNode.getSetSet().getDataList1().getValue()); + currentNode.getOutSet().setDataList2(currentNode.getInSet().getDataList2().getAppSet(), currentNode.getInSet().getDataList2().getValue()); + } else if (currentNode.getSetSet().getDataList2().getAppSet()) { //App2 is a writer + currentNode.getOutSet().setDataList1(currentNode.getInSet().getDataList1().getAppSet(), currentNode.getInSet().getDataList1().getValue()); + currentNode.getOutSet().setDataList2(currentNode.getSetSet().getDataList2().getAppSet(), currentNode.getSetSet().getDataList2().getValue()); + } else { //No writer for this node => outSet = inSet + currentNode.getOutSet().setDataList1(currentNode.getInSet().getDataList1().getAppSet(), currentNode.getInSet().getDataList1().getValue()); + currentNode.getOutSet().setDataList2(currentNode.getInSet().getDataList2().getAppSet(), currentNode.getInSet().getDataList2().getValue()); + } + } + + 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().getDataList1().getAppSet()) { + currentNode.getInSet().setDataList1(true, i.getOutSet().getDataList1().getValue()); + } + + //Check to see if dataList2 of predNode(i) is valid or not: if valid get its value + if (i.getOutSet().getDataList2().getAppSet()) { + currentNode.getInSet().setDataList2(true, i.getOutSet().getDataList2().getValue()); + } + } + } + + boolean checkOutSetChange(Node currentNode, DataSet tempOutSet) { + return ((currentNode.getOutSet().getDataList1().getAppSet() != tempOutSet.getDataList1().getAppSet())|| + !(currentNode.getOutSet().getDataList1().getValue().equals(tempOutSet.getDataList1().getValue()))|| + (currentNode.getOutSet().getDataList2().getAppSet() != tempOutSet.getDataList2().getAppSet())|| + !(currentNode.getOutSet().getDataList2().getValue().equals(tempOutSet.getDataList2().getValue()))); + } + + public void checkForConflict(Node currentNode) { + if ((currentNode.getOutSet().getDataList1().getAppSet() == true)&&(currentNode.getOutSet().getDataList2().getAppSet() == true)) { //Both apps have set the device + if (!(currentNode.getOutSet().getDataList1().getValue().equals(currentNode.getOutSet().getDataList2().getValue()))) //Values set by the apps are not the same, and we have a conflict! + conflictFound = true; + } + } + + 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"); + + Node(Integer id) { + this.id = id; + } + + void addPredecessor(Node node) { + predecessors.add(node); + } + + void addSuccessor(Node node) { + successors.add(node); + } + + void emptyInSet() { + this.inSet = new DataSet(false, "NA", false, "NA"); + } + + void setInSet(DataSet inSet) { + this.inSet.setDataList1(inSet.getDataList1().getAppSet(), inSet.getDataList1().getValue()); + this.inSet.setDataList2(inSet.getDataList2().getAppSet(), inSet.getDataList2().getValue()); + } + + void setSetSet(DataSet setSet) { + this.setSet.setDataList1(setSet.getDataList1().getAppSet(), setSet.getDataList1().getValue()); + this.setSet.setDataList2(setSet.getDataList2().getAppSet(), setSet.getDataList2().getValue()); + } + + void setOutSet(DataSet outSet) { + this.outSet.setDataList1(outSet.getDataList1().getAppSet(), outSet.getDataList1().getValue()); + this.outSet.setDataList2(outSet.getDataList2().getAppSet(), outSet.getDataList2().getValue()); + } + + Integer getId() { + return id; + } + + ArrayList getPredecessors() { + return predecessors; + } + + ArrayList getSuccessors() { + return successors; + } + + DataSet getInSet() { + return inSet; + } + + DataSet getOutSet() { + return outSet; + } + + DataSet getSetSet() { + return setSet; + } + } + class DataList { boolean appSet; String value; - DataList(boolean appSet, String value) { + DataList(boolean appSet, String value) { this.appSet = appSet; this.value = value; - } + } + + void setAppSet(boolean appSet) { + this.appSet = appSet; + } + + void setValue(String value) { + this.value = value; + } + + boolean getAppSet() { + return appSet; + } + + String getValue() { + return value; + } } class DataSet { - HashMap dataSet = new HashMap(); + DataList dataList1 = new DataList(false, "NA"); + DataList dataList2 = new DataList(false, "NA"); + + DataSet(boolean appSet1, String value1, boolean appSet2, String value2) { + dataList1.setAppSet(appSet1); + dataList1.setValue(value1); + dataList2.setAppSet(appSet2); + dataList2.setValue(value2); + } - DataSet(HashMap dataSet) { - this.dataSet = dataSet; - } + void setDataList1(boolean appSet, String value) { + dataList1.setAppSet(appSet); + dataList1.setValue(value); + } + + void setDataList2(boolean appSet, String value) { + dataList2.setAppSet(appSet); + dataList2.setValue(value); + } + + DataList getDataList1() { + return dataList1; + } + + DataList getDataList2() { + return dataList2; + } } @Override @@ -102,14 +246,16 @@ public class ConflictTracker extends ListenerAdapter { detail = null; out.println("The state is restored to state with id: "+id+", depth: "+depth); - - parentId = id; + + //Update the parent node + parentNode = new Node(id); } @Override public void searchStarted(Search search) { out.println("----------------------------------- search started"); } + @Override public void stateAdvanced(Search search) { @@ -117,9 +263,19 @@ public class ConflictTracker extends ListenerAdapter { id = search.getStateId(); depth = search.getDepth(); operation = "forward"; - + + //Add the node to the list of nodes + nodes.put(id, new Node(id)); + Node currentNode = nodes.get(id); + 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"; } @@ -130,178 +286,82 @@ 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.addPredecessor(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); + + + //Set the input set of this state to empty + currentNode.emptyInSet(); - //Set input set of this state to empty! - HashMap inDataSet = new HashMap(); - inDataSet.put(0, new DataList(false, "NA")); - inDataSet.put(1, new DataList(false, "NA")); - DataSet inTempDataSet = new DataSet(inDataSet); - inSet.put(id, inTempDataSet); - - //Set output set of this state to empty if it is not initialized! - if (!outSet.containsKey(id)) { - HashMap outDataSet = new HashMap(); - outDataSet.put(0, new DataList(false, "NA")); - outDataSet.put(1, new DataList(false, "NA")); - DataSet outTempDataSet = new DataSet(outDataSet); - outSet.put(id, outTempDataSet); - } + //Store the out set of this state to the temporary data set + DataSet tempOutSet = new DataSet(currentNode.getOutSet().getDataList1().getAppSet(), + currentNode.getOutSet().getDataList1().getValue(), + currentNode.getOutSet().getDataList2().getAppSet(), + currentNode.getOutSet().getDataList2().getValue()); - //Create a temp data set of out set of this node - DataList tempDataList1 = new DataList(outSet.get(id).dataSet.get(0).appSet, outSet.get(id).dataSet.get(0).value); - DataList tempDataList2 = new DataList(outSet.get(id).dataSet.get(1).appSet, outSet.get(id).dataSet.get(1).value); - HashMap tempOutDataSet = new HashMap(); - tempOutDataSet.put(0, tempDataList1); - tempOutDataSet.put(1, tempDataList2); - DataSet tempDataSet = new DataSet(tempOutDataSet); //Set input set according to output set of pred states of current state - if (predSet.containsKey(id)) { - for (Integer i : predSet.get(id)) { - if ((outSet.get(i).dataSet.get(0).appSet == true)||(inSet.get(id).dataSet.get(0).appSet == true)) { - inSet.get(id).dataSet.get(0).appSet = true; - inSet.get(id).dataSet.get(0).value = outSet.get(i).dataSet.get(0).value; - } - if ((outSet.get(i).dataSet.get(1).appSet == true)||(inSet.get(id).dataSet.get(1).appSet == true)) { - inSet.get(id).dataSet.get(1).appSet = true; - inSet.get(id).dataSet.get(1).value = outSet.get(i).dataSet.get(1).value; - } - } - } + setInSet(currentNode); + + + + //Set dataLists of outSet to dataLists of setSet if it is valid, otherwise to dataLists of inSet + setOutSet(currentNode); - //Set output set to inset or setSet - if (setSet.containsKey(id)) { - if ((setSet.get(id).dataSet.get(0).appSet == true)&&(setSet.get(id).dataSet.get(1).appSet == true)) { //App1 & App2 are writers - outSet.get(id).dataSet.get(0).appSet = true; - outSet.get(id).dataSet.get(0).value = setSet.get(id).dataSet.get(0).value; - outSet.get(id).dataSet.get(1).appSet = true; - outSet.get(id).dataSet.get(1).value = setSet.get(id).dataSet.get(1).value; - } else if (setSet.get(id).dataSet.get(0).appSet == true) { //App1 is a writer - outSet.get(id).dataSet.get(0).appSet = true; - outSet.get(id).dataSet.get(0).value = setSet.get(id).dataSet.get(0).value; - outSet.get(id).dataSet.get(1).appSet = inSet.get(id).dataSet.get(1).appSet; - outSet.get(id).dataSet.get(1).value = inSet.get(id).dataSet.get(1).value; - } else if (setSet.get(id).dataSet.get(1).appSet == true) { //App2 is a writer - outSet.get(id).dataSet.get(0).appSet = inSet.get(id).dataSet.get(0).appSet; - outSet.get(id).dataSet.get(0).value = inSet.get(id).dataSet.get(0).value; - outSet.get(id).dataSet.get(1).appSet = true; - outSet.get(id).dataSet.get(1).value = setSet.get(id).dataSet.get(1).value; - } - } else { - outSet.get(id).dataSet.get(0).appSet = inSet.get(id).dataSet.get(0).appSet; - outSet.get(id).dataSet.get(0).value = inSet.get(id).dataSet.get(0).value; - outSet.get(id).dataSet.get(1).appSet = inSet.get(id).dataSet.get(1).appSet; - outSet.get(id).dataSet.get(1).value = inSet.get(id).dataSet.get(1).value; - } - if ((outSet.get(id).dataSet.get(0).appSet == true)&&(outSet.get(id).dataSet.get(1).appSet == true)) { //Both apps have set the device - if (!(outSet.get(id).dataSet.get(0).value.equals(outSet.get(id).dataSet.get(1).value))) //Values set by the apps are not the same, and we have a conflict! - conflictFound = 1; - } + //Check for a conflict + checkForConflict(currentNode); + + - if ((outSet.get(id).dataSet.get(0).appSet != tempDataSet.dataSet.get(0).appSet)|| - ((!outSet.get(id).dataSet.get(0).value.equals(tempDataSet.dataSet.get(0).value)))|| - (outSet.get(id).dataSet.get(1).appSet != tempDataSet.dataSet.get(1).appSet)|| - ((!outSet.get(id).dataSet.get(1).value.equals(tempDataSet.dataSet.get(1).value)))) { - ArrayList changed = new ArrayList(predSet.get(id)); + //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! + //Get a random node inside the changed list and remove it from the list Integer rnd = new Random().nextInt(changed.size()); - Integer nodeToProcess = changed.get(rnd); + Node nodeToProcess = changed.get(rnd); changed.remove(nodeToProcess); - //Initialize the empty input set for the current node - HashMap nodeDataSet = new HashMap(); - nodeDataSet.put(0, new DataList(false, "NA")); - nodeDataSet.put(1, new DataList(false, "NA")); - DataSet nodeTempDataSet = new DataSet(nodeDataSet); - inSet.put(nodeToProcess, nodeTempDataSet); - - //Store current output to temp dataset - HashMap currentOutDataSet = new HashMap(); - currentOutDataSet.put(0, new DataList(outSet.get(nodeToProcess).dataSet.get(0).appSet, outSet.get(nodeToProcess).dataSet.get(0).value)); - currentOutDataSet.put(1, new DataList(outSet.get(nodeToProcess).dataSet.get(1).appSet, outSet.get(nodeToProcess).dataSet.get(1).value)); - DataSet currentDataSet = new DataSet(currentOutDataSet); - - //Update the in set based on predecessors - for (Integer i : predSet.get(nodeToProcess)) { - if ((outSet.get(i).dataSet.get(0).appSet == true)||(inSet.get(nodeToProcess).dataSet.get(0).appSet == true)) { - inSet.get(nodeToProcess).dataSet.get(0).appSet = true; - inSet.get(nodeToProcess).dataSet.get(0).value = outSet.get(i).dataSet.get(0).value; - } + //Initialize the empty input set for current node + nodeToProcess.emptyInSet(); - if ((outSet.get(i).dataSet.get(1).appSet == true)||(inSet.get(nodeToProcess).dataSet.get(1).appSet == true)) { - inSet.get(nodeToProcess).dataSet.get(1).appSet = true; - inSet.get(nodeToProcess).dataSet.get(1).value = outSet.get(i).dataSet.get(1).value; - } - } + //Store the out set of this state to the temporary data set + tempOutSet = new DataSet(nodeToProcess.getOutSet().getDataList1().getAppSet(), + nodeToProcess.getOutSet().getDataList1().getValue(), + nodeToProcess.getOutSet().getDataList2().getAppSet(), + nodeToProcess.getOutSet().getDataList2().getValue()); + + + //Set input set according to output set of pred states of current state + setInSet(nodeToProcess); + + + //Set outSet to setSet if it is valid, otherwise to inSet + setOutSet(nodeToProcess); - //Set output set to inset or setSet - if (setSet.containsKey(nodeToProcess)) { - if ((setSet.get(nodeToProcess).dataSet.get(0).appSet == true)&&(setSet.get(nodeToProcess).dataSet.get(1).appSet == true)) { //App1 & App2 are writers - outSet.get(nodeToProcess).dataSet.get(0).appSet = true; - outSet.get(nodeToProcess).dataSet.get(0).value = setSet.get(nodeToProcess).dataSet.get(0).value; - outSet.get(nodeToProcess).dataSet.get(1).appSet = true; - outSet.get(nodeToProcess).dataSet.get(1).value = setSet.get(nodeToProcess).dataSet.get(1).value; - } else if (setSet.get(nodeToProcess).dataSet.get(0).appSet == true) { //App1 is a writer - outSet.get(nodeToProcess).dataSet.get(0).appSet = true; - outSet.get(nodeToProcess).dataSet.get(0).value = setSet.get(nodeToProcess).dataSet.get(0).value; - outSet.get(nodeToProcess).dataSet.get(1).appSet = inSet.get(nodeToProcess).dataSet.get(1).appSet; - outSet.get(nodeToProcess).dataSet.get(1).value = inSet.get(nodeToProcess).dataSet.get(1).value; - } else if (setSet.get(nodeToProcess).dataSet.get(1).appSet == true) { //App2 is a writer - outSet.get(nodeToProcess).dataSet.get(0).appSet = inSet.get(nodeToProcess).dataSet.get(0).appSet; - outSet.get(nodeToProcess).dataSet.get(0).value = inSet.get(nodeToProcess).dataSet.get(0).value; - outSet.get(nodeToProcess).dataSet.get(1).appSet = true; - outSet.get(nodeToProcess).dataSet.get(1).value = setSet.get(nodeToProcess).dataSet.get(1).value; - } - } else { - outSet.get(nodeToProcess).dataSet.get(0).appSet = inSet.get(nodeToProcess).dataSet.get(0).appSet; - outSet.get(nodeToProcess).dataSet.get(0).value = inSet.get(nodeToProcess).dataSet.get(0).value; - outSet.get(nodeToProcess).dataSet.get(1).appSet = inSet.get(nodeToProcess).dataSet.get(1).appSet; - outSet.get(nodeToProcess).dataSet.get(1).value = inSet.get(nodeToProcess).dataSet.get(1).value; - } - //Checking if the output set has changed or not(Add its successors to the change list!) - if ((outSet.get(nodeToProcess).dataSet.get(0).appSet != currentDataSet.dataSet.get(0).appSet)|| - !(outSet.get(nodeToProcess).dataSet.get(0).value.equals(currentDataSet.dataSet.get(0).value))|| - (outSet.get(nodeToProcess).dataSet.get(1).appSet != currentDataSet.dataSet.get(1).appSet)|| - !(outSet.get(nodeToProcess).dataSet.get(1).value.equals(currentDataSet.dataSet.get(1).value))) { - for (Integer i : succSet.get(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); + } } - } } - - //Update the pred - if (succSet.containsKey(id)) { - ArrayList ids = succSet.get(id); - if (!ids.contains(parentId)) { - ids.add(parentId); - succSet.put(id, ids); - } - } else if (parentId != -2) { - ArrayList ids = new ArrayList(); - ids.add(parentId); - succSet.put(id, ids); - } - - //Update the suc - if (succSet.containsKey(parentId)) { - ArrayList ids = succSet.get(parentId); - if (!ids.contains(id)) { - ids.add(id); - succSet.put(parentId, ids); - } - } else if (parentId != -2) { - ArrayList ids = new ArrayList(); - ids.add(id); - succSet.put(parentId, ids); - } - parentId = id; + //Update the parent node + parentNode = new Node(id); } @@ -314,7 +374,8 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is backtracked to state with id: "+id+", depth: "+depth); - parentId = id; + //Update the parent node + parentNode = new Node(id); } @Override @@ -460,7 +521,7 @@ public class ConflictTracker extends ListenerAdapter { @Override public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { - if (conflictFound == 1) { + if (conflictFound) { StringBuilder sb = new StringBuilder(); sb.append("Conflict found between two apps!"); Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString()); @@ -478,32 +539,14 @@ public class ConflictTracker extends ListenerAdapter { if (writer == null) return; - //Update the HashMap for Set set. - if (setSet.containsKey(id)) { - if (writer.equals("App1")) { - setSet.get(id).dataSet.get(0).appSet = true; - setSet.get(id).dataSet.get(0).value = value; - } else if (writer.equals("App2")) { - setSet.get(id).dataSet.get(1).appSet = true; - setSet.get(id).dataSet.get(1).value = value; - } - } else { - HashMap dataSet = new HashMap(); - DataList dataList1 = new DataList(false, "NA"); - DataList dataList2 = new DataList(false, "NA"); - if (writer.equals("App1")) { - dataList1.appSet = true; - dataList1.value = value; - } else if (writer.equals("App2")) { - dataList2.appSet = true; - dataList2.value = value; - } - dataSet.put(0, dataList1); - dataSet.put(1, dataList2); - DataSet tempDataSet = new DataSet(dataSet); - setSet.put(id, tempDataSet); - } - + //Update the temporary Set set. + if (writer.equals("App1")) + tempSetSet.setDataList1(true, value); + else if (writer.equals("App2")) + tempSetSet.setDataList2(true, value); + //Set isSet to 1 + isSet = true; + } } -- 2.34.1