private final PrintWriter out;
private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
- private final HashMap<Integer, ArrayList<Integer>> predSet = new HashMap<Integer, ArrayList<Integer>>();
- private final HashMap<Integer, ArrayList<Integer>> succSet = new HashMap<Integer, ArrayList<Integer>>();
- private final HashMap<Integer, DataSet> setSet = new HashMap<Integer, DataSet>();
- private final HashMap<Integer, DataSet> inSet = new HashMap<Integer, DataSet>();
- private final HashMap<Integer, DataSet> outSet = new HashMap<Integer, DataSet>();
+ private final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // 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;
}
}
+ 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<Node> predecessors = new ArrayList<Node>();
+ ArrayList<Node> successors = new ArrayList<Node>();
+ 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<Node> getPredecessors() {
+ return predecessors;
+ }
+
+ ArrayList<Node> 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<Integer, DataList> dataSet = new HashMap<Integer, DataList>();
+ 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<Integer, DataList> 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
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) {
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";
}
}
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<Integer, DataList> inDataSet = new HashMap<Integer, DataList>();
- 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<Integer, DataList> outDataSet = new HashMap<Integer, DataList>();
- 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<Integer, DataList> tempOutDataSet = new HashMap<Integer, DataList>();
- 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<Integer> changed = new ArrayList<Integer>(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<Node> changed = new ArrayList<Node>(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<Integer, DataList> nodeDataSet = new HashMap<Integer, DataList>();
- 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<Integer, DataList> currentOutDataSet = new HashMap<Integer, DataList>();
- 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<Integer> ids = succSet.get(id);
- if (!ids.contains(parentId)) {
- ids.add(parentId);
- succSet.put(id, ids);
- }
- } else if (parentId != -2) {
- ArrayList<Integer> ids = new ArrayList<Integer>();
- ids.add(parentId);
- succSet.put(id, ids);
- }
-
- //Update the suc
- if (succSet.containsKey(parentId)) {
- ArrayList<Integer> ids = succSet.get(parentId);
- if (!ids.contains(id)) {
- ids.add(id);
- succSet.put(parentId, ids);
- }
- } else if (parentId != -2) {
- ArrayList<Integer> ids = new ArrayList<Integer>();
- ids.add(id);
- succSet.put(parentId, ids);
- }
- parentId = id;
+ //Update the parent node
+ parentNode = new Node(id);
}
out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
- parentId = id;
+ //Update the parent node
+ parentNode = new Node(id);
}
@Override
@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());
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<Integer, DataList> dataSet = new HashMap<Integer, DataList>();
- 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;
+
}
}
projects / jpf-core.git / commitdiff