Script Tree:

TODO: working view
branch labels
matches
colouring

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java

@@ -145,6 +145,8 @@ public class DebuggerMain implements Initializable {
     @FXML
     private CheckMenuItem miProofTree;
     @FXML
+    private CheckMenuItem miScriptTree;
+    @FXML
     private ToggleButton btnInteractiveMode;
 
     @FXML
@@ -158,6 +160,12 @@ public class DebuggerMain implements Initializable {
     //-----------------------------------------------------------------------------------------------------------------
     private ProofTree proofTree = new ProofTree(this);
     private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree");
+
+    //TODO: anpassen
+    private ScriptTreeGraph scriptTreeGraph = new ScriptTreeGraph();
+    private ScriptTreeView scriptTreeView = new ScriptTreeView();
+    private DockNode scriptTreeDock = new DockNode(scriptTreeView,"Script Tree");
+
     private WelcomePane welcomePane = new WelcomePane(this);
     private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT));
     private DockNode activeInspectorDock;
@@ -165,6 +173,7 @@ public class DebuggerMain implements Initializable {
     private DockNode commandHelpDock = new DockNode(commandHelp, "DebuggerCommand Help");
     private InteractiveModeController interactiveModeController;
     private ScriptExecutionController scriptExecutionController;
+
     @FXML
     private Menu examplesMenu;
     private Timer interpreterThreadTimer;
@@ -1302,6 +1311,22 @@ public class DebuggerMain implements Initializable {
         }
     }
 
+    @FXML
+    public void showScriptTree(ActionEvent actionEvent) {
+       // FXML
+        //TODO: anpassen
+        if (!scriptTreeDock.isDocked() && !scriptTreeDock.isFloating()) {
+            scriptTreeDock.dock(dockStation, DockPos.CENTER);
+        }
+        ScriptTreeGraph stg = new ScriptTreeGraph();
+        stg.createGraph(model.getDebuggerFramework().getPtreeManager().getStartNode(), FACADE.getProof().root());
+        scriptTreeView.setTree(stg.toView());
+
+
+
+    }
+
+
     public DockNode getJavaAreaDock() {
         return javaAreaDock;
     }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/AbstractTreeNode.java

 package edu.kit.iti.formal.psdbg.gui.controls.ScriptTree;
 
+import edu.kit.iti.formal.psdbg.gui.controls.TreeNode;
 import lombok.Getter;
 import lombok.Setter;
 
 import java.util.List;
 
 public class AbstractTreeNode {
+
     @Getter @Setter
     private AbstractTreeNode parent;
 
     @Getter @Setter
     private List<AbstractTreeNode> children;
 
+    @Getter @Setter
+    private boolean isMatchEx = false; //is a match expression
+
+    @Getter @Setter
+    private boolean isSucc = true; //applied successfully
+
+    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

 package edu.kit.iti.formal.psdbg.gui.controls.ScriptTree;
 
 import de.uka.ilkd.key.proof.Node;
-import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.AbstractTreeNode;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/DummyGoalNode.java

 package edu.kit.iti.formal.psdbg.gui.controls.ScriptTree;
 
-import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.AbstractTreeNode;
+import de.uka.ilkd.key.proof.Node;
+import edu.kit.iti.formal.psdbg.gui.controls.TreeNode;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 
@@ -10,4 +11,11 @@ public class DummyGoalNode extends AbstractTreeNode {
     @Getter
     private final boolean closedGoal;
 
+    @Getter
+    private final Node node;
+
+    @Override
+    public TreeNode toTreeNode() {
+        return  new TreeNode((closedGoal? "CLOSED":"OPEN"), node); //TODO:
+    }
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/ScriptTreeNode.java

 package edu.kit.iti.formal.psdbg.gui.controls.ScriptTree;
 
 import de.uka.ilkd.key.proof.Node;
-import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.AbstractTreeNode;
+import edu.kit.iti.formal.psdbg.gui.controls.TreeNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
 import lombok.Getter;
@@ -18,10 +18,26 @@ public class ScriptTreeNode extends AbstractTreeNode {
     private final PTreeNode<KeyData> scriptState;
     @Getter
     private final Node keyNode;
+    @Getter @Setter
+    private final int linenr;
 
     @Override
     public String toString(){
         return scriptState.getStatement().toString()+" with ID "+scriptState.getId();
     }
 
+    @Override
+    public TreeNode toTreeNode() {
+        String label;
+        if (isMatchEx()) {
+            label = "match in line " + linenr;
+        } else {
+            label = scriptState.getStatement().getNodeName() + " (line " + linenr + ")";
+        }
+
+        if (!isSucc()) {
+            label += " (failed)";
+        }
+        return  new TreeNode(label, keyNode);
+    }
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTreeGraph.java

@@ -4,16 +4,22 @@ import com.google.common.graph.GraphBuilder;
 import com.google.common.graph.MutableGraph;
 import de.uka.ilkd.key.proof.Node;
 import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.AbstractTreeNode;
+import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.DummyGoalNode;
 import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.ScriptTreeNode;
-import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.data.State;
 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.*;
 
 
@@ -27,6 +33,8 @@ public class ScriptTreeGraph {
 
     private PTreeNode<KeyData> currentNode;
 
+    private PTreeNode<KeyData> nextPtreeNode;
+
     private List<PTreeNode<KeyData>> sortedList;
     private final MutableGraph<AbstractTreeNode> graph =
             GraphBuilder.directed().allowsSelfLoops(false).build();
@@ -34,7 +42,7 @@ public class ScriptTreeGraph {
     public void createGraph(PTreeNode<KeyData> rootPTreeNode, Node root) {
 
         this.currentNode = rootPTreeNode;
-        ScriptTreeNode rootNode = new ScriptTreeNode(rootPTreeNode, root);
+        ScriptTreeNode rootNode = new ScriptTreeNode(rootPTreeNode, root, rootPTreeNode.getStatement().getStartPosition().getLineNumber());
         mapping = new HashMap<Node, AbstractTreeNode>();
         front = new ArrayList<>();
         sortedList = new ArrayList<>();
@@ -55,27 +63,74 @@ public class ScriptTreeGraph {
 
     }
 
-    private void addParents() {
+    private void addParents() { //TODO and childrens
         Node current = rootNode.getKeyNode();
         AbstractTreeNode currentParent = mapping.get(current);
 
+
+
         Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0);
         while(iter.hasNext()){
             PTreeNode<KeyData> next = iter.next();
             if (next.getStateAfterStmt() != null) {
+                Map.Entry<Node, AbstractTreeNode> entry = getMap(next);
+                if(entry == null) {
+                    continue;
+                }
+                currentParent = entry.getValue();
+                current = entry.getKey();
+
                 for (GoalNode<KeyData> gn: next.getStateAfterStmt().getGoals()) {
                     mapping.get(gn.getData().getNode()).setParent(currentParent);
+
+
+                    //add children
+                    if(mapping.get(current).getChildren() == null) {
+                        List<AbstractTreeNode> children = new ArrayList<>();
+                        children.add(mapping.get(gn.getData().getNode()));
+                        mapping.get(current).setChildren(children);
+                    } else {
+                        mapping.get(current).getChildren().add(mapping.get(gn.getData().getNode()));
+                    }
+
+
+                    /*
+                    //set children
+                    List<AbstractTreeNode> children = mapping.get(gn.getData().getNode()).getParent().getChildren();
+                    if( children == null) {
+                        List<AbstractTreeNode> childlist = new ArrayList<>();
+                        childlist.add(mapping.get(gn.getData().getNode()));
+                        mapping.get(gn.getData().getNode()).getParent().setChildren(childlist);
+                    } else {
+                        if(!children.contains(mapping.get(gn.getData().getNode()))) {
+                            children.add(mapping.get(gn.getData().getNode()));
+                        }
+                    }
+                    */
                 }
             }
+            /*
             if(next.getStateBeforeStmt().getSelectedGoalNode() != null) {
                 current = next.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
                 currentParent = mapping.get(current);
             }
+            */
         }
 
         mapping.size();
     }
 
+    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(((ScriptTreeNode)pair.getValue()).getScriptState() == treeNode) {
+                return pair;
+            }
+        }
+        return null;
+    }
+
     private void computeList() {
         while (currentNode != null) {
             sortedList.add(currentNode);
@@ -85,31 +140,111 @@ public class ScriptTreeGraph {
 
     public void compute() {
         Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0);
+        ScriptVisitor visitor = new ScriptVisitor();
+
+        ASTNode statement;
         //Node current = rootNode.getKeyNode();
         while (iter.hasNext()) {
-            PTreeNode<KeyData> nextPtreeNode = iter.next();
-            ASTNode statement = nextPtreeNode.getStatement();
+            nextPtreeNode = iter.next();
+            statement = nextPtreeNode.getStatement();
             //check for selected node and find the node in map
             if (nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode() != null) {
-                if (statement instanceof CallStatement) {
-                    Node n = nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
-                    ScriptTreeNode sn = new ScriptTreeNode(nextPtreeNode, n);
-                   // sn.setParent(mapping.get(current));
-                    mapping.replace(n, sn);
-                    front.remove(n);
-                   // current = n;
-                    for (GoalNode<KeyData> gn : nextPtreeNode.getStateAfterStmt().getGoals()) {
-                        mapping.put(gn.getData().getNode(), null);
-                        front.add(gn.getData().getNode());
-                    }
-
-                }
-                if(statement instanceof CaseStatement){
-
-                }
+                statement.accept(visitor);
             }
         }
+        //TODO create DummyGoalNodes
         mapping.size();
         mapping.forEach((node, abstractTreeNode) -> System.out.println("node.serialNr() = " + node.serialNr() + " " + abstractTreeNode.toString()));
     }
+
+    public TreeItem<TreeNode> toView() {
+        TreeItem<TreeNode> treeItem = new TreeItem<TreeNode>(new TreeNode("Proof", rootNode.getKeyNode()));
+
+
+        List<AbstractTreeNode> children = mapping.get(rootNode.getKeyNode()).getChildren();
+
+        while (children.size() == 1) {
+            treeItem.getChildren().add(new TreeItem<>(children.get(0).toTreeNode()));
+            children = children.get(0).getChildren();
+        }
+
+        if(children.size() != 0) {
+            children.forEach(k -> treeItem.getChildren().add(rekursiveToView(k)));
+        }
+        return treeItem;
+    }
+
+    private TreeItem<TreeNode> rekursiveToView(AbstractTreeNode current) {
+        TreeItem<TreeNode> treeItem = new TreeItem<>(current.toTreeNode()); //TODO: sollte eig immer ein Branchlabel sein
+
+        AbstractTreeNode parent = current;
+        List<AbstractTreeNode> children = current.getChildren();
+
+
+        while (children != null && children.size() == 1) {
+            treeItem.getChildren().add(new TreeItem<>(children.get(0).toTreeNode()));
+            parent = children.get(0);
+            children = children.get(0).getChildren();
+        }
+        if (children == null) {
+            try {
+                Node node = ((ScriptTreeNode)parent).getKeyNode();
+                DummyGoalNode dummy = new DummyGoalNode(node.isClosed(), node);
+                treeItem.getChildren().add(new TreeItem<>(dummy.toTreeNode())); //TODO : dummy in mapping ?? check if getchildren can be null
+            } catch (Exception e) {
+                //TODO;
+                return treeItem;
+
+            }
+           return treeItem;
+        }
+
+        if(children.size() != 0) {
+            children.forEach(k -> treeItem.getChildren().add(rekursiveToView(k)));
+        }
+        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);
+           }
+            mapping.replace(n, sn);
+            front.remove(n);
+            // current = n;
+            for (GoalNode<KeyData> gn : nextPtreeNode.getStateAfterStmt().getGoals()) {
+                mapping.put(gn.getData().getNode(), null);
+                front.add(gn.getData().getNode());
+            }
+            return null;
+        }
+
+        @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);
+
+           if (nextintoptn == null) {
+                match.setSucc(false);
+                //TODO: add stuff
+               return null;
+            }
+            Node n = nextintoptn.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
+            if(mapping.get(n) != null) {
+                mapping.get(n).getChildren().add(match);
+            } else {
+                mapping.put(n,match);
+            }
+            return null;
+        }
+
+
+    }
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTreeView.java

+package edu.kit.iti.formal.psdbg.gui.controls;
+
+import javafx.fxml.FXML;
+import javafx.scene.control.TreeCell;
+import javafx.scene.control.TreeItem;
+import javafx.scene.control.TreeView;
+import javafx.scene.control.cell.TextFieldTreeCell;
+import javafx.scene.layout.BorderPane;
+import javafx.util.StringConverter;
+
+public class ScriptTreeView extends BorderPane {
+    @FXML
+    TreeView<TreeNode> treeView;
+
+    public ScriptTreeView() {
+        Utils.createWithFXML(this);
+
+        treeView = new TreeView<>();
+        treeView.setCellFactory(this::cellFactory);
+
+    }
+
+    public void setTree(TreeItem<TreeNode> tree) {
+        treeView.setRoot(tree);
+        treeView.refresh();
+    }
+
+    private TreeCell<TreeNode> cellFactory(TreeView<TreeNode> nodeTreeView) {
+        TextFieldTreeCell<TreeNode> tftc = new TextFieldTreeCell<>();
+        StringConverter<TreeNode> stringConverter = new StringConverter<TreeNode>() {
+            @Override
+            public String toString(TreeNode object) {
+                return object.label;
+            }
+
+            @Override
+            public TreeNode fromString(String string) {
+                return null;
+            }
+        };
+        tftc.setConverter(stringConverter);
+        /*
+        tftc.itemProperty().addListener((p, o, n) -> {
+            if (n != null)
+                repaint(tftc);
+        }); */
+
+        //colorOfNodes.addListener((InvalidationListener) o -> repaint(tftc));
+        return tftc;
+    }
+}

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml

@@ -181,6 +181,11 @@
                                         <MaterialDesignIconView glyphName="TREE" size="24.0"/>
                                     </graphic>
                                 </CheckMenuItem>
+                                <CheckMenuItem fx:id="miScriptTree" onAction="#showScriptTree" text="Show Script Tree">
+                                    <graphic>
+                                        <MaterialDesignIconView glyphName="TREE" size="24.0"/>
+                                    </graphic>
+                                </CheckMenuItem>
                                 <CheckMenuItem fx:id="miCommandHelp" onAction="#showCommandHelp"
                                                accelerator="F1"
                                                text="Show Command Help">

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/ScriptTreeView.fxml

+<?xml version="1.0" encoding="UTF-8"?>
+
+<?import java.lang.*?>
+<?import java.util.*?>
+<?import javafx.scene.*?>
+<?import javafx.scene.control.*?>
+<?import javafx.scene.layout.*?>
+
+<fx:root type="javafx.scene.layout.BorderPane" xmlns:fx="http://javafx.com/fxml/1" fx:id="rootPane" xmlns="http://javafx.com/javafx/8.0.112">
+<center>
+    <TreeView fx:id="treeView" editable="false">
+
+    </TreeView>
+</center>
+
+
+</fx:root>
\ No newline at end of file