From e4da0904b11090c95f5bfb284673301c53402cc7 Mon Sep 17 00:00:00 2001 From: amiraj Date: Tue, 8 Oct 2019 10:29:06 -0700 Subject: [PATCH] Changing small things in the listener! --- .../nasa/jpf/listener/ConflictTracker.java | 104 +++++++++--------- 1 file changed, 55 insertions(+), 49 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index e9ca30c..307463e 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -80,26 +80,26 @@ public class ConflictTracker extends ListenerAdapter { } 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 + 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 + // App1 & App2 are writers outSetTemp.setApp1DataList(setSetApp1List.getAppSet(), setSetApp1List.getValue()); outSetTemp.setApp2DataList(setSetApp2List.getAppSet(), setSetApp2List.getValue()); } else if (setSetApp2List.getAppSet()) { - //App1 is a writer + // App1 is a writer outSetTemp.setApp1DataList(setSetApp1List.getAppSet(), setSetApp1List.getValue()); outSetTemp.setApp2DataList(inSetApp2List.getAppSet(), inSetApp2List.getValue()); } else if (setSetApp2List.getAppSet()) { - //App2 is a writer + // App2 is a writer outSetTemp.setApp1DataList(inSetApp1List.getAppSet(),inSetApp1List.getValue()); outSetTemp.setApp2DataList(setSetApp2List.getAppSet(), setSetApp2List.getValue()); } else { - //No writer for this node => outSet = inSet + // No writer for this node => outSet = inSet outSetTemp.setApp1DataList(inSetApp1List.getAppSet(), inSetApp1List.getValue()); outSetTemp.setApp2DataList(inSetApp2List.getAppSet(), inSetApp2List.getValue()); } @@ -107,12 +107,12 @@ public class ConflictTracker extends ListenerAdapter { 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 + // 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()); } - //Check to see if dataList2 of predNode(i) is valid or not: if valid get its value + // 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()); } @@ -120,12 +120,12 @@ public class ConflictTracker extends ListenerAdapter { } 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 + 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 1 if the outSet has changed! return ((outSetApp1List.getAppSet() != tempSetApp1List.getAppSet())|| !(outSetApp1List.getValue().equals(tempSetApp1List.getValue()))|| (outSetApp2List.getAppSet() != tempSetApp2List.getAppSet())|| @@ -133,35 +133,35 @@ public class ConflictTracker extends ListenerAdapter { } 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 + 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 if ((outSetApp1List.getAppSet() == true)&&(outSetApp2List.getAppSet() == true)) { - //Both apps have set the device + // 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! + // Values set by the apps are not the same, and we have a conflict! conflictFound = true; } } } public DataSet updateSets(Node currentNode) { - //Empty the in set of the node + // 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 + // Store the out set of this state to the temporary data set DataSet tempOutSet = new DataSet(outSetApp1List.getAppSet(), outSetApp1List.getValue(), outSetApp2List.getAppSet(), outSetApp2List.getValue()); - //Set input set according to output set of pred states of current state + // 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 + // Set dataLists of outSet to dataLists of setSet if it is valid, otherwise to dataLists of inSet setOutSet(currentNode); return tempOutSet; @@ -192,18 +192,24 @@ public class ConflictTracker extends ListenerAdapter { } void setInSet(DataSet inSet) { - this.inSet.setApp1DataList(inSet.getApp1DataList().getAppSet(), inSet.getApp1DataList().getValue()); - this.inSet.setApp2DataList(inSet.getApp2DataList().getAppSet(), inSet.getApp2DataList().getValue()); + 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) { - this.setSet.setApp1DataList(setSet.getApp1DataList().getAppSet(), setSet.getApp1DataList().getValue()); - this.setSet.setApp2DataList(setSet.getApp2DataList().getAppSet(), setSet.getApp2DataList().getValue()); + 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) { - this.outSet.setApp1DataList(outSet.getApp1DataList().getAppSet(), outSet.getApp1DataList().getValue()); - this.outSet.setApp2DataList(outSet.getApp2DataList().getAppSet(), outSet.getApp2DataList().getValue()); + DataList outSetApp1List = outSet.getApp1DataList(); + DataList outSetApp2List = outSet.getApp2DataList(); + this.outSet.setApp1DataList(outSetApp1List.getAppSet(), outSetApp1List.getValue()); + this.outSet.setApp2DataList(outSetApp2List.getAppSet(), outSetApp2List.getValue()); } Integer getId() { @@ -296,7 +302,7 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is restored to state with id: "+id+", depth: "+depth); - //Update the parent node + // Update the parent node parentNode = new Node(id); } @@ -313,14 +319,14 @@ public class ConflictTracker extends ListenerAdapter { depth = search.getDepth(); operation = "forward"; - //Add the node to the list of nodes + // 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 + // Add this new node detail = "new"; - //Update the setSet for this new node + // Update the setSet for this new node if (isSet) { currentNode.setSetSet(tempSetSet); isSet = false; @@ -336,38 +342,38 @@ 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 + // 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 + // 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); - //update the sets, store the outSet to temp before changes + // Update the sets, store the outSet to temp before its changes DataSet tempOutSet = updateSets(currentNode); - //Check for a conflict + // Check for a conflict checkForConflict(currentNode); - //Check if the outSet of this state has changed, update all of its successors' sets if any + // 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 + // 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 changes + // Update the sets, store the outSet to temp before its changes tempOutSet = updateSets(nodeToProcess); - //Check for a conflict + // Check for a conflict checkForConflict(nodeToProcess); - //Checking if the out set has changed or not(Add its successors to the change list!) + // 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)) @@ -377,7 +383,7 @@ public class ConflictTracker extends ListenerAdapter { } } - //Update the parent node + // Update the parent node parentNode = new Node(id); } @@ -390,7 +396,7 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is backtracked to state with id: "+id+", depth: "+depth); - //Update the parent node + // Update the parent node parentNode = new Node(id); } @@ -565,12 +571,12 @@ public class ConflictTracker extends ListenerAdapter { if (writer == null) return; - //Update the temporary Set set. + // Update the temporary Set set. if (writer.equals("App1")) tempSetSet.setApp1DataList(true, value); else if (writer.equals("App2")) tempSetSet.setApp2DataList(true, value); - //Set isSet to 1 + // Set isSet to 1 isSet = true; } -- 2.34.1