Commit 73513b9a authored by Sarah Grebing's avatar Sarah Grebing

interim

parent 2566cd6e
......@@ -97,7 +97,7 @@ public class KeyProofTreeTransformation {
TreeItem<TreeNode> populate = populate(childNode.getNodeInfo().getBranchLabel(), childNode);
currentItem.getChildren().add(populate);
} else {
TreeItem<TreeNode> populate = populate("BRANCH " + branchCounter, childNode);
TreeItem<TreeNode> populate = populate("Case " + branchCounter, childNode);
TreeItem<TreeNode> self = itemFactory(childNode);
populate.getChildren().add(0, self);
currentItem.getChildren().add(populate);
......
package edu.kit.iti.formal.psdbg.gui.controls;
import com.google.common.graph.Graph;
import com.google.common.graph.GraphBuilder;
import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
public class ScriptTreeGraph {
private ScriptTreeNode rootNode;
private final Graph<ScriptTreeNode> graph =
GraphBuilder.directed().allowsSelfLoops(false).build();
public void createGraph(PTreeNode<KeyData> rootPTreeNode, Node root) {
ScriptTreeNode rootNode = new ScriptTreeNode(rootPTreeNode);
rootNode.setKeyNode(root);
graph.nodes().add(rootNode);
this.rootNode = rootNode;
}
}
package edu.kit.iti.formal.psdbg.gui.controls;
import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
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 {
@Getter
private final PTreeNode<KeyData> scriptState;
@Getter @Setter
private Node keyNode;
}
......@@ -2,6 +2,8 @@ package edu.kit.iti.formal.psdbg.gui.controls;
import com.google.common.collect.HashMultimap;
import com.google.common.collect.Multimap;
import com.google.common.graph.Graph;
import com.google.common.graph.GraphBuilder;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.ShortCommandPrinter;
......@@ -15,6 +17,7 @@ import javafx.util.Pair;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import lombok.val;
import sun.reflect.generics.tree.Tree;
import java.util.*;
......@@ -65,8 +68,8 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
}
return getNextPtreeNode(current);
}
}
@Override
public TreeItem<TreeNode> create(Proof proof) {
Set<PTreeNode<KeyData>> nodes = manager.getNodes();
......@@ -115,44 +118,13 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
}
/*//TODO: Reverse ArrayList in the end or nah?
@Deprecated
public ArrayList<String> getBranchLabels(TreeNode node) {
TreeItem<TreeNode> proofTree = create(proof);
ArrayList<String> branchlabels = new ArrayList<>();
int i = 0;
branchlabels.set(0, node.label);
while (node != null) {
if (!branchlabels.get(i).equals(node.label)) {
i++;
branchlabels.set(i, node.label);
}
//TODO: node = node.parent
}
public TreeItem<TreeNode> buildTree(PTreeNode<KeyData> rootNode, Proof proof){
return branchlabels;
}
public ArrayList<String> getBranchLabels(Node node) {
ArrayList<String> branchlabels = new ArrayList<>();
int i = 0;
//TODO: branchlabel = all branchlabels or only next one
branchlabels.set(0, node.getNodeInfo().getBranchLabel());
Node n = node.parent();
while (n != null) {
if (!branchlabels.get(i).equals(n.getNodeInfo().getBranchLabel())) {
i++;
branchlabels.set(i, n.getNodeInfo().getBranchLabel());
}
n = n.parent();
}
setPointer(rootNode);
return branchlabels;
TreeItem<TreeNode> rootTree = new TreeItem<>(new TreeNode("Proof", proof.root()));
return rootTree;
}
*/
public TreeItem<TreeNode> buildScriptTree(PTreeNode<KeyData> node, Proof proof) {
......@@ -169,7 +141,7 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
TreeItem<TreeNode> currentItem = new TreeItem<>(new TreeNode("Proof", nextNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode()));
//build the first node after the root
TreeNode t = createTreeNode(nextNode);
if (t != null) currentItem.getChildren().add(new TreeItem<>());
if (t != null) currentItem.getChildren().add(new TreeItem<>(t));
return buildScriptSubTree(currentItem, nextNode, nextNode.getStateAfterStmt().getSelectedGoalNode());
......@@ -179,7 +151,6 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
* Build the subtrees for the script tree structure
* @param currentItem
* @param nextNode
* @param root
* @return
*/
public TreeItem<TreeNode> buildScriptSubTree(TreeItem<TreeNode> currentItem, PTreeNode<KeyData> nextNode, GoalNode<KeyData> currentNode) {
......@@ -220,7 +191,7 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
int size = goals.size();
for (int i = 0; i < size; i++) {
currentNode = goals.get(i);
TreeItem<TreeNode> child = new TreeItem<>(new TreeNode("Branch " + i, goals.get(i).getData().getNode())); //todo right branches
TreeItem<TreeNode> child = new TreeItem<>(new TreeNode("Case " + i+1, goals.get(i).getData().getNode())); //todo right branches
Pair<TreeItem<TreeNode>, PTreeNode<KeyData>> treeItemPTreeNodePair = buildScriptTreeHelper(nextNode, goals.get(i));
child.getChildren().add(treeItemPTreeNodePair.getKey());
......
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