From 132b1c978f5cbda81f2fdf5a9427ac7a88f5c9c7 Mon Sep 17 00:00:00 2001 From: amiraj Date: Mon, 7 Oct 2019 12:24:41 -0700 Subject: [PATCH] Make more changes to the ConflictTracker listener. --- .../nasa/jpf/listener/ConflictTracker.java | 67 ++++++++----------- 1 file changed, 28 insertions(+), 39 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index d58ed39..6c9be0e 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -140,6 +140,28 @@ public class ConflictTracker extends ListenerAdapter { } } + 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()); + + //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; + } + class Node { Integer id; ArrayList predecessors = new ArrayList(); @@ -318,32 +340,12 @@ public class ConflictTracker extends ListenerAdapter { //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(); - - - //Store the out set of this state to the temporary data set - 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 - setInSet(currentNode); - + //update the sets, store the outSet to temp before changes + DataSet tempOutSet = updateSets(currentNode); - //Set dataLists of outSet to dataLists of setSet if it is valid, otherwise to dataLists of inSet - setOutSet(currentNode); - - //Check for a conflict checkForConflict(currentNode); - - //Check if the outSet of this state has changed, update all of its successors' sets if any if (checkOutSetChange(currentNode, tempOutSet)) { @@ -354,23 +356,11 @@ public class ConflictTracker extends ListenerAdapter { Node nodeToProcess = changed.get(rnd); changed.remove(nodeToProcess); - //Initialize the empty input set for current node - nodeToProcess.emptyInSet(); - - //Store the out set of this state to the temporary data set - 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 - setInSet(nodeToProcess); - - - //Set outSet to setSet if it is valid, otherwise to inSet - setOutSet(nodeToProcess); + //update the sets, store the outSet to temp before 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)) { @@ -384,7 +374,6 @@ public class ConflictTracker extends ListenerAdapter { //Update the parent node parentNode = new Node(id); - } @Override -- 2.34.1