Skip to content

GitLab

Commit 3127b86c authored by Lulu Luong's avatar Lulu Luong
Browse files

works for most examples, except for Java examples -> scripttree does not... 

works for most examples, except for Java examples -> scripttree does not recognize loaded java ex and displays old scripttree
parent 0e92d4c7
Pipeline #25059 passed with stages
in 2 minutes and 59 seconds
Hide whitespace changes
Inline Side-by-side
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/AbstractTreeNode.java
View file @ 3127b86c
package edu.kit.iti.formal.psdbg.gui.controls.ScriptTree;
import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.gui.controls.TreeNode;
import lombok.Getter;
import lombok.Setter;
......@@ -14,12 +15,19 @@ public class AbstractTreeNode {
@Getter @Setter
private List<AbstractTreeNode> children;
@Getter @Setter
private final Node node;
@Getter @Setter
private boolean isMatchEx = false; //is a match expression
@Getter @Setter
private boolean isSucc = true; //applied successfully
public AbstractTreeNode(Node node) {
this.node = node;
}
public TreeNode toTreeNode() {
return new TreeNode("no to string method yet", null);
}
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/BranchLabelNode.java
View file @ 3127b86c
......@@ -5,18 +5,21 @@ import edu.kit.iti.formal.psdbg.gui.controls.TreeNode;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
@RequiredArgsConstructor
public class BranchLabelNode extends AbstractTreeNode {
@Getter
private final Node keyBranchNode;
@Getter
private final String labelName;
public BranchLabelNode(Node node, String labelName) {
super(node);
this.labelName = labelName;
}
@Override
public TreeNode toTreeNode() {
return new TreeNode(labelName, keyBranchNode);
return new TreeNode(labelName, getNode());
}
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/DummyGoalNode.java
View file @ 3127b86c
......@@ -5,17 +5,19 @@ import edu.kit.iti.formal.psdbg.gui.controls.TreeNode;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
@RequiredArgsConstructor
public class DummyGoalNode extends AbstractTreeNode {
@Getter
private final boolean closedGoal;
@Getter
private final Node node;
public DummyGoalNode(Node node, boolean closedGoal) {
super(node);
this.closedGoal = closedGoal;
}
@Override
public TreeNode toTreeNode() {
return new TreeNode((closedGoal? "CLOSED":"OPEN"), node); //TODO:
return new TreeNode((closedGoal? "CLOSED":"OPEN"), getNode()); //TODO:
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/ScriptTreeNode.java
View file @ 3127b86c
......@@ -13,15 +13,20 @@ import lombok.Setter;
* This calss represents a node in the script tree, whcih can be of different kinds.
* The scriptTreeNodes is the model calls for TreeNodes
*/
@RequiredArgsConstructor
public class ScriptTreeNode extends AbstractTreeNode {
@Getter
private final PTreeNode<KeyData> scriptState;
@Getter
private final Node keyNode;
@Getter @Setter
private final int linenr;
public ScriptTreeNode(Node node, PTreeNode<KeyData> scriptState, int linenr) {
super(node);
this.scriptState = scriptState;
this.linenr = linenr;
}
@Override
public String toString(){
return scriptState.getStatement().toString()+" with ID "+scriptState.getId();
......@@ -39,6 +44,6 @@ public class ScriptTreeNode extends AbstractTreeNode {
if (!isSucc()) {
label += " (failed)";
}
return new TreeNode(label, keyNode);
return new TreeNode(label, getNode());
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTreeGraph.java
View file @ 3127b86c
......@@ -14,13 +14,9 @@ import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.CaseStatement;
import edu.kit.iti.formal.psdbg.parser.ast.GuardedCaseStatement;
import javafx.scene.control.TreeItem;
import javafx.scene.control.TreeView;
import sun.reflect.generics.tree.Tree;
import java.security.Key;
import java.util.*;
......@@ -43,7 +39,7 @@ public class ScriptTreeGraph {
public void createGraph(PTreeNode<KeyData> rootPTreeNode, Node root) {
this.currentNode = rootPTreeNode;
ScriptTreeNode rootNode = new ScriptTreeNode(rootPTreeNode, root, rootPTreeNode.getStatement().getStartPosition().getLineNumber());
ScriptTreeNode rootNode = new ScriptTreeNode(root, rootPTreeNode, rootPTreeNode.getStatement().getStartPosition().getLineNumber());
mapping = new HashMap<Node, AbstractTreeNode>();
front = new ArrayList<>();
sortedList = new ArrayList<>();
......@@ -68,273 +64,281 @@ public class ScriptTreeGraph {
}
private void addParentsAndChildren() {
Node current;
AbstractTreeNode currentParent;
Node currentNode;
AbstractTreeNode currentTreenode;
Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0);
while(iter.hasNext()){
while (iter.hasNext()) {
PTreeNode<KeyData> next = iter.next();
if (next.getStateAfterStmt() != null) {
Map.Entry<Node, AbstractTreeNode> entry = getMap(next);
if(entry == null) {
Map.Entry<Node, AbstractTreeNode> entry = getMap(next); //get entry in mapping
if (entry == null) {
continue;
}
currentParent = entry.getValue();
current = entry.getKey();
//no children -> last mutator
currentTreenode = entry.getValue();
currentNode = entry.getKey();
if(next.getStateAfterStmt().getGoals().size() == 0 && currentParent instanceof ScriptTreeNode) {
/* PTreeNode<KeyData> previous = (next.getStepInvInto() != null)? next.getStepInvInto(): next.getStepInvOver();
if(previous == null) {
continue;
}
Map.Entry<Node, AbstractTreeNode> preventry = getMap(previous);
Node prevNode = previous.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
AbstractTreeNode prevParent =(preventry == null)? mapping.get(prevNode) :preventry.getValue();
Node prev =(preventry == null)? prevNode: preventry.getKey(); //TODO: sinnnlos?
//no children -> last mutator
mapping.get(current).setParent(prevParent);
// if(next.getStateAfterStmt().getGoals().size() == 0 && currentTreenode instanceof ScriptTreeNode) {
//add children TODO: remove redundancy
if(mapping.get(prev).getChildren() == null) {
List<AbstractTreeNode> childlist = new ArrayList<>();
childlist.add(mapping.get(current));
mapping.get(prev).setChildren(childlist);
} else {
mapping.get(prev).getChildren().add(mapping.get(current));
Node parent = currentNode.parent();
if(parent != null && currentTreenode != null) {
addToSubChildren(parent, mapping.get(currentNode));
/*
List<AbstractTreeNode> children = currentTreenode.getChildren();
if(children == null) {
continue;
}
for(int i = 0; i < children.size(); i++) {
AbstractTreeNode tn = children.get(i);
mapping.get(tn.getNode()).setParent(currentTreenode);
addToSubChildren(currentNode, tn);
}
continue;
*/
}
//has children
for (GoalNode<KeyData> gn: next.getStateAfterStmt().getGoals()) {
mapping.get(gn.getData().getNode()).setParent(currentParent);
if(mapping.get(gn.getData().getNode()).getParent() != null)
mapping.get(gn.getData().getNode()).setParent(currentTreenode);
addToChildren(currentNode, mapping.get(gn.getData().getNode()));
}
//add children
if(mapping.get(current).getChildren() == null) {
List<AbstractTreeNode> childlist = new ArrayList<>();
childlist.add(mapping.get(gn.getData().getNode()));
mapping.get(current).setChildren(childlist);
} else {
mapping.get(current).getChildren().add(mapping.get(gn.getData().getNode()));
}
/*
for (AbstractTreeNode tn : currentTreenode.getChildren()) {
/*
//set children
List<AbstractTreeNode> children = mapping.get(gn.getData().getNode()).getParent().getChildren();
if( children == null) {
mapping.get(tn.getNode()).setParent(currentTreenode);
//add children
if (mapping.get(currentNode).getChildren() == null) {
List<AbstractTreeNode> childlist = new ArrayList<>();
childlist.add(mapping.get(gn.getData().getNode()));
mapping.get(gn.getData().getNode()).getParent().setChildren(childlist);
childlist.add(mapping.get(tn.getNode()));
mapping.get(currentNode).setChildren(childlist);
} else {
if(!children.contains(mapping.get(gn.getData().getNode()))) {
children.add(mapping.get(gn.getData().getNode()));
}
mapping.get(currentNode).getChildren().add(mapping.get(tn.getNode()));
}
*/
} */
}
}
/*
if(next.getStateBeforeStmt().getSelectedGoalNode() != null) {
current = next.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
currentParent = mapping.get(current);
}
private void addToChildren(Node node, AbstractTreeNode atn) {
if(mapping.get(node) == atn) return;
if (mapping.get(node).getChildren() == null) {
List<AbstractTreeNode> childlist = new ArrayList<>();
childlist.add(atn);
mapping.get(node).setChildren(childlist);
} else {
if (mapping.get(node).getChildren().contains(atn)) return;
mapping.get(node).getChildren().add(atn);
}
*/
}
//mapping.size();
}
private void addToSubChildren(Node node, AbstractTreeNode atn) {
if(mapping.get(node) == atn) return;
if (mapping.get(node).getChildren() == null) {
List<AbstractTreeNode> childlist = new ArrayList<>();
childlist.add(atn);
mapping.get(node).setChildren(childlist);
} else {
/*
private void insertBranchLabels(Node parent, Node child) {
//TODO: add in mappimng and don't forget to double link
String[] branchlabels;
List<AbstractTreeNode> childlist = mapping.get(node).getChildren();
if(childlist.contains(atn)) return;
String currentBranchlabel = child.getNodeInfo().getBranchLabel();
while(currentBranchlabel != parent.getNodeInfo().getBranchLabel()) {
while (childlist.get(0).getChildren() != null) {
if(childlist.contains(atn)) return;
childlist = childlist.get(0).getChildren();
}
List<AbstractTreeNode> subchild = new ArrayList<>();
subchild.add(atn);
childlist.get(0).setChildren(subchild);
}
}
}
*/
private Map.Entry<Node, AbstractTreeNode> getMap(PTreeNode<KeyData> treeNode) {
Iterator it = mapping.entrySet().iterator();
while(it.hasNext()) {
Map.Entry<Node, AbstractTreeNode> pair = (Map.Entry)it.next();
if (pair.getValue() instanceof ScriptTreeNode) {
if(((ScriptTreeNode)pair.getValue()).getScriptState() == treeNode) {
return pair;
private Map.Entry<Node, AbstractTreeNode> getMap (PTreeNode < KeyData > treeNode) {
Iterator it = mapping.entrySet().iterator();
while (it.hasNext()) {
Map.Entry<Node, AbstractTreeNode> pair = (Map.Entry) it.next();
if (pair.getValue() instanceof ScriptTreeNode) {
if (((ScriptTreeNode) pair.getValue()).getScriptState() == treeNode) {
return pair;
}
}
}
return null;
}
return null;
}
private void computeList() {
while (currentNode != null) {
sortedList.add(currentNode);
currentNode = currentNode.getNextPtreeNode(currentNode);
private void computeList () {
while (currentNode != null) {
sortedList.add(currentNode);
currentNode = currentNode.getNextPtreeNode(currentNode);
}
}
}
public void compute() {
Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0);
ScriptVisitor visitor = new ScriptVisitor();
ASTNode statement;
//Node current = rootNode.getKeyNode();
while (iter.hasNext()) {
nextPtreeNode = iter.next();
statement = nextPtreeNode.getStatement();
//check for selected node and find the node in map
if (nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode() != null) {
statement.accept(visitor);
public void compute () {
Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0);
ScriptVisitor visitor = new ScriptVisitor();
ASTNode statement;
//Node current = rootNode.getKeyNode();
while (iter.hasNext()) {
nextPtreeNode = iter.next();
statement = nextPtreeNode.getStatement();
//check for selected node and find the node in map
if (nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode() != null) {
statement.accept(visitor);
}
}
mapping.size();
mapping.forEach((node, abstractTreeNode) -> System.out.println("node.serialNr() = " + node.serialNr() + " " + abstractTreeNode.toTreeNode().label));
}
mapping.size();
mapping.forEach((node, abstractTreeNode) -> System.out.println("node.serialNr() = " + node.serialNr() + " " + abstractTreeNode.toTreeNode().label));
}
public TreeItem<TreeNode> toView () {
TreeItem<TreeNode> treeItem = new TreeItem<>(new TreeNode("Proof", rootNode.getNode()));
public TreeItem<TreeNode> toView() {
TreeItem<TreeNode> treeItem = new TreeItem<>(new TreeNode("Proof", rootNode.getKeyNode()));
List<AbstractTreeNode> children = mapping.get(rootNode.getNode()).getChildren();
if (children == null) return treeItem;
treeItem.getChildren().add(new TreeItem<>(mapping.get(rootNode.getNode()).toTreeNode()));
List<AbstractTreeNode> children = mapping.get(rootNode.getKeyNode()).getChildren();
treeItem.getChildren().add(new TreeItem<TreeNode>(mapping.get(rootNode.getKeyNode()).toTreeNode()));
while (children.size() == 1) {
treeItem.getChildren().add(new TreeItem<>(children.get(0).toTreeNode()));
children = children.get(0).getChildren();
}
while (children.size() == 1) {
treeItem.getChildren().add(new TreeItem<>(children.get(0).toTreeNode()));
children = children.get(0).getChildren();
if(children == null) return treeItem;
}
if(children.size() != 0) {
children.forEach(k -> treeItem.getChildren().add(rekursiveToView(k)));
if (children.size() != 0) {
children.forEach(k -> treeItem.getChildren().add(rekursiveToView(k)));
}
return treeItem;
}
return treeItem;
}
private TreeItem<TreeNode> rekursiveToView(AbstractTreeNode current) {
TreeItem<TreeNode> treeItem = new TreeItem<>(current.toTreeNode()); //TODO: sollte eig immer ein Branchlabel sein
private TreeItem<TreeNode> rekursiveToView (AbstractTreeNode current){
TreeItem<TreeNode> treeItem = new TreeItem<>(current.toTreeNode()); //TODO: sollte eig immer ein Branchlabel sein
List<AbstractTreeNode> children = current.getChildren();
List<AbstractTreeNode> children = current.getChildren();
while (children != null && children.size() == 1) {
treeItem.getChildren().add(new TreeItem<>(children.get(0).toTreeNode()));
children = children.get(0).getChildren();
}
if (children == null) {
return treeItem;
}
if(children.size() != 0) {
children.forEach(k -> treeItem.getChildren().add(rekursiveToView(k)));
}
return treeItem;
}
while (children != null && children.size() == 1) {
if(children.get(0) == null) return treeItem;
treeItem.getChildren().add(new TreeItem<>(children.get(0).toTreeNode()));
children = children.get(0).getChildren();
}
if (children == null) {
return treeItem;
}
private class ScriptVisitor extends DefaultASTVisitor<Void> {
@Override
public Void visit(CallStatement call) {
Node n = nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
ScriptTreeNode sn = new ScriptTreeNode(nextPtreeNode, n, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
// sn.setParent(mapping.get(current));
if(nextPtreeNode.getStateBeforeStmt() == nextPtreeNode.getStateAfterStmt()) {
sn.setSucc(false);
}
putIntoMapping(n, sn);
//mapping.replace(n,sn);
front.remove(n);
// current = n;
List<GoalNode<KeyData>> children = nextPtreeNode.getStateAfterStmt().getGoals();
switch (children.size()) {
case 0:
DummyGoalNode goalnode = new DummyGoalNode(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().isClosed(), nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode());
goalnode.setParent(sn);
List<AbstractTreeNode> childlist = new ArrayList<>();
childlist.add(goalnode);
sn.setChildren(childlist);
putIntoMapping(sn.getKeyNode(), goalnode);
break;
case 1:
putIntoMapping(children.get(0).getData().getNode(), null);
front.add(children.get(0).getData().getNode());
break;
default: //multiple open goals/children -> branch labels
int branchcounter = 1;
for (GoalNode<KeyData> gn : children) {
Node node = gn.getData().getNode();
BranchLabelNode branchNode = (node.getNodeInfo().getBranchLabel() != null)? new BranchLabelNode(node, node.getNodeInfo().getBranchLabel()):
new BranchLabelNode(node, "Case " + branchcounter);
putIntoMapping(node, branchNode);
front.add(node);
branchcounter++;
}
if (children.size() != 0) {
children.forEach(k -> treeItem.getChildren().add(rekursiveToView(k)));
}
return null;
return treeItem;
}
private class ScriptVisitor extends DefaultASTVisitor<Void> {
@Override
public Void visit(CallStatement call) {
Node n = nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
ScriptTreeNode sn = new ScriptTreeNode(n, nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
// sn.setParent(mapping.get(current));
if (nextPtreeNode.getStateBeforeStmt() == nextPtreeNode.getStateAfterStmt()) {
sn.setSucc(false);
}
putIntoMapping(n, sn);
//mapping.replace(n,sn);
front.remove(n);
// current = n;
List<GoalNode<KeyData>> children = nextPtreeNode.getStateAfterStmt().getGoals();
@Override
public Void visit(GuardedCaseStatement caseStatement) {
PTreeNode<KeyData> nextintoptn = nextPtreeNode.getStepInto();
ScriptTreeNode match = new ScriptTreeNode(nextPtreeNode, nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(), nextPtreeNode.getStatement().getStartPosition().getLineNumber());
match.setMatchEx(true);
switch (children.size()) {
case 0:
DummyGoalNode goalnode = new DummyGoalNode(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(), nextPtreeNode.getStateAfterStmt().getGoals().size() == 0);
goalnode.setParent(sn);
if (nextintoptn == null) {
match.setSucc(false);
//TODO: add stuff
return null;
List<AbstractTreeNode> childlist = new ArrayList<>();
childlist.add(goalnode);
sn.setChildren(childlist);
putIntoMapping(sn.getNode(), goalnode);
break;
case 1:
putIntoMapping(children.get(0).getData().getNode(), null);
front.add(children.get(0).getData().getNode());
break;
default: //multiple open goals/children -> branch labels
int branchcounter = 1;
for (GoalNode<KeyData> gn : children) {
Node node = gn.getData().getNode();
BranchLabelNode branchNode = (node.getNodeInfo().getBranchLabel() != null) ? new BranchLabelNode(node, node.getNodeInfo().getBranchLabel()) :
new BranchLabelNode(node, "Case " + branchcounter);
mapping.put(node, branchNode);
front.add(node);
branchcounter++;
}
}
return null;
}
Node n = nextintoptn.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
putIntoMapping(n,match);
return null;
}
}
private void putIntoMapping(Node node, AbstractTreeNode treeNode) { //TODO: more usage?
@Override
public Void visit(GuardedCaseStatement caseStatement) {
PTreeNode<KeyData> nextintoptn = nextPtreeNode.getStepInto();
ScriptTreeNode match = new ScriptTreeNode(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(),nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
match.setMatchEx(true);
if(mapping.get(node) == null) {
mapping.put(node, treeNode);
} else {
if(mapping.get(node).getChildren() == null) {
mapping.get(node).setChildren(new ArrayList<AbstractTreeNode>());
if (nextintoptn == null) {
match.setSucc(false);
//TODO: add stuff
return null;