From 05c451a2f98c7f40812d9ffcf1d63b80342b0381 Mon Sep 17 00:00:00 2001 From: amiraj Date: Mon, 7 Oct 2019 12:06:59 -0700 Subject: [PATCH] Make more changes to the ConflictTracker listener. --- .../nasa/jpf/listener/ConflictTracker.java | 134 ++++++++++-------- 1 file changed, 78 insertions(+), 56 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index 8d5d1c4..d58ed39 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -75,46 +75,68 @@ 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()); + 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()); } } 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()); + 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 - if (i.getOutSet().getDataList2().getAppSet()) { - currentNode.getInSet().setDataList2(true, i.getOutSet().getDataList2().getValue()); + if (i.getOutSet().getApp2DataList().getAppSet()) { + currentNode.getInSet().setApp2DataList(true, i.getOutSet().getApp2DataList().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()))); + 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()))); } 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! + 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 + if (!(outSetApp1List.getValue().equals(outSetApp2List.getValue()))) { + //Values set by the apps are not the same, and we have a conflict! conflictFound = true; + } } } @@ -143,18 +165,18 @@ public class ConflictTracker extends ListenerAdapter { } void setInSet(DataSet inSet) { - this.inSet.setDataList1(inSet.getDataList1().getAppSet(), inSet.getDataList1().getValue()); - this.inSet.setDataList2(inSet.getDataList2().getAppSet(), inSet.getDataList2().getValue()); + this.inSet.setApp1DataList(inSet.getApp1DataList().getAppSet(), inSet.getApp1DataList().getValue()); + this.inSet.setApp2DataList(inSet.getApp2DataList().getAppSet(), inSet.getApp2DataList().getValue()); } void setSetSet(DataSet setSet) { - this.setSet.setDataList1(setSet.getDataList1().getAppSet(), setSet.getDataList1().getValue()); - this.setSet.setDataList2(setSet.getDataList2().getAppSet(), setSet.getDataList2().getValue()); + this.setSet.setApp1DataList(setSet.getApp1DataList().getAppSet(), setSet.getApp1DataList().getValue()); + this.setSet.setApp2DataList(setSet.getApp2DataList().getAppSet(), setSet.getApp2DataList().getValue()); } void setOutSet(DataSet outSet) { - this.outSet.setDataList1(outSet.getDataList1().getAppSet(), outSet.getDataList1().getValue()); - this.outSet.setDataList2(outSet.getDataList2().getAppSet(), outSet.getDataList2().getValue()); + this.outSet.setApp1DataList(outSet.getApp1DataList().getAppSet(), outSet.getApp1DataList().getValue()); + this.outSet.setApp2DataList(outSet.getApp2DataList().getAppSet(), outSet.getApp2DataList().getValue()); } Integer getId() { @@ -209,32 +231,32 @@ public class ConflictTracker extends ListenerAdapter { } class DataSet { - 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); + 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); } - void setDataList1(boolean appSet, String value) { - dataList1.setAppSet(appSet); - dataList1.setValue(value); + void setApp1DataList(boolean appSet, String value) { + app1DataList.setAppSet(appSet); + app1DataList.setValue(value); } - void setDataList2(boolean appSet, String value) { - dataList2.setAppSet(appSet); - dataList2.setValue(value); + void setApp2DataList(boolean appSet, String value) { + app2DataList.setAppSet(appSet); + app2DataList.setValue(value); } - DataList getDataList1() { - return dataList1; + DataList getApp1DataList() { + return app1DataList; } - DataList getDataList2() { - return dataList2; + DataList getApp2DataList() { + return app2DataList; } } @@ -303,10 +325,10 @@ public class ConflictTracker extends ListenerAdapter { //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()); + DataSet tempOutSet = new DataSet(currentNode.getOutSet().getApp1DataList().getAppSet(), + currentNode.getOutSet().getApp1DataList().getValue(), + currentNode.getOutSet().getApp2DataList().getAppSet(), + currentNode.getOutSet().getApp2DataList().getValue()); //Set input set according to output set of pred states of current state @@ -336,10 +358,10 @@ public class ConflictTracker extends ListenerAdapter { nodeToProcess.emptyInSet(); //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()); + tempOutSet = new DataSet(nodeToProcess.getOutSet().getApp1DataList().getAppSet(), + nodeToProcess.getOutSet().getApp1DataList().getValue(), + nodeToProcess.getOutSet().getApp2DataList().getAppSet(), + nodeToProcess.getOutSet().getApp2DataList().getValue()); //Set input set according to output set of pred states of current state @@ -541,9 +563,9 @@ public class ConflictTracker extends ListenerAdapter { //Update the temporary Set set. if (writer.equals("App1")) - tempSetSet.setDataList1(true, value); + tempSetSet.setApp1DataList(true, value); else if (writer.equals("App2")) - tempSetSet.setDataList2(true, value); + tempSetSet.setApp2DataList(true, value); //Set isSet to 1 isSet = true; -- 2.34.1