Commit c5fd7c63 authored by Lulu Luong's avatar Lulu Luong
Browse files

bug fix: visible DummyGoalsNodes via front

parent 29682c3e
Pipeline #25496 passed with stages
in 99 minutes and 23 seconds
...@@ -49,13 +49,16 @@ public class ScriptTreeGraph { ...@@ -49,13 +49,16 @@ public class ScriptTreeGraph {
if (stateAfterStmt != null) { if (stateAfterStmt != null) {
for (GoalNode<KeyData> g : stateAfterStmt.getGoals()) { for (GoalNode<KeyData> g : stateAfterStmt.getGoals()) {
putIntoMapping(g.getData().getNode(), null); putIntoMapping(g.getData().getNode(), null);
front.add(g.getData().getNode()); putIntoFront(g.getData().getNode());
} }
} else {
} }
this.rootNode = rootNode; this.rootNode = rootNode;
computeList(); computeList();
compute(); compute();
addParentsAndChildren(); addParentsAndChildren();
addGoals();
mapping.size(); mapping.size();
//TODO: remove following //TODO: remove following
...@@ -261,6 +264,7 @@ public class ScriptTreeGraph { ...@@ -261,6 +264,7 @@ public class ScriptTreeGraph {
switch (children.size()) { switch (children.size()) {
case 0: case 0:
/*
DummyGoalNode goalnode = new DummyGoalNode(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(), nextPtreeNode.getStateAfterStmt().getGoals().size() == 0); DummyGoalNode goalnode = new DummyGoalNode(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(), nextPtreeNode.getStateAfterStmt().getGoals().size() == 0);
goalnode.setParent(sn); goalnode.setParent(sn);
...@@ -270,11 +274,12 @@ public class ScriptTreeGraph { ...@@ -270,11 +274,12 @@ public class ScriptTreeGraph {
sn.setChildren(childlist); sn.setChildren(childlist);
putIntoMapping(sn.getNode(), goalnode); putIntoMapping(sn.getNode(), goalnode);*/
putIntoFront(n);
break; break;
case 1: case 1:
putIntoMapping(children.get(0).getData().getNode(), null); putIntoMapping(children.get(0).getData().getNode(), null);
front.add(children.get(0).getData().getNode()); putIntoFront(children.get(0).getData().getNode());
break; break;
default: //multiple open goals/children -> branch labels default: //multiple open goals/children -> branch labels
int branchcounter = 1; int branchcounter = 1;
...@@ -283,7 +288,7 @@ public class ScriptTreeGraph { ...@@ -283,7 +288,7 @@ public class ScriptTreeGraph {
BranchLabelNode branchNode = (node.getNodeInfo().getBranchLabel() != null) ? new BranchLabelNode(node, node.getNodeInfo().getBranchLabel()) : BranchLabelNode branchNode = (node.getNodeInfo().getBranchLabel() != null) ? new BranchLabelNode(node, node.getNodeInfo().getBranchLabel()) :
new BranchLabelNode(node, "Case " + branchcounter); new BranchLabelNode(node, "Case " + branchcounter);
mapping.put(node, branchNode); mapping.put(node, branchNode);
front.add(node); putIntoFront(node);
branchcounter++; branchcounter++;
} }
} }
...@@ -304,6 +309,7 @@ public class ScriptTreeGraph { ...@@ -304,6 +309,7 @@ public class ScriptTreeGraph {
} }
Node n = nextintoptn.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(); Node n = nextintoptn.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
putIntoMapping(n, match); putIntoMapping(n, match);
//front.remove(n);
return null; return null;
} }
...@@ -315,15 +321,24 @@ public class ScriptTreeGraph { ...@@ -315,15 +321,24 @@ public class ScriptTreeGraph {
* @param node * @param node
* @param treeNode * @param treeNode
*/ */
private void putIntoMapping (Node node, AbstractTreeNode treeNode){ //TODO: more usage? private void putIntoMapping (Node node, AbstractTreeNode treeNode){
if (mapping.get(node) == null) { if (mapping.get(node) == null) {
mapping.put(node, treeNode); mapping.put(node, treeNode);
} else { } else {
addToSubChildren(node, treeNode); addToSubChildren(node, treeNode);
} }
}
private void putIntoFront (Node node) {
if(!front.contains(node)) {
front.add(node);
} }
}
private void addGoals() {
front.forEach(k -> putIntoMapping(k, new DummyGoalNode(k, k.isClosed())));
}
private String getMappingString (AbstractTreeNode node){ private String getMappingString (AbstractTreeNode node){
String s = ""; String s = "";
if (node != null) { if (node != null) {
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment