branchlabels extracted

TODO: add to mapping in right order

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

@@ -163,7 +163,7 @@ public class DebuggerMain implements Initializable {
 
     //TODO: anpassen
     private ScriptTreeGraph scriptTreeGraph = new ScriptTreeGraph();
-    private ScriptTreeView scriptTreeView = new ScriptTreeView();
+    private ScriptTreeView scriptTreeView = new ScriptTreeView(this);
     private DockNode scriptTreeDock = new DockNode(scriptTreeView,"Script Tree");
 
     private WelcomePane welcomePane = new WelcomePane(this);
@@ -1317,21 +1317,18 @@ public class DebuggerMain implements Initializable {
         if (!scriptTreeDock.isDocked() && !scriptTreeDock.isFloating()) {
             scriptTreeDock.dock(dockStation, DockPos.LEFT);
         }
+
+        // old version of scripttree
+
         ScriptTreeGraph stg = new ScriptTreeGraph();
         PTreeNode startnode = (model.getDebuggerFramework() != null)?model.getDebuggerFramework().getPtreeManager().getStartNode():null;
         stg.createGraph(startnode, FACADE.getProof().root());
 
-
-
         TreeItem<TreeNode> item = (stg.toView());
 
-       /* TreeView<TreeNode> content = new TreeView<>(item);
-        DockNode dn = new DockNode(content, "TEst");
+        scriptTreeView.setTree(item);
 
-        dn.dock(dockStation, DockPos.LEFT);
-        */
 
-        scriptTreeView.setTree(item);
 
     }
 

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

@@ -59,6 +59,7 @@ public class ProofTree extends BorderPane {
         @Override
         public void proofIsBeingPruned(ProofTreeEvent proofTreeEvent) {
 
+
         }
 
         @Override

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

@@ -18,6 +18,7 @@ import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
 import edu.kit.iti.formal.psdbg.parser.ast.ForeachStatement;
 import edu.kit.iti.formal.psdbg.parser.ast.GuardedCaseStatement;
 import javafx.scene.control.TreeItem;
+import lombok.Getter;
 import sun.reflect.generics.tree.Tree;
 
 import java.util.*;
@@ -25,8 +26,10 @@ import java.util.*;
 
 public class ScriptTreeGraph {
 
+    @Getter
     private ScriptTreeNode rootNode;
 
+    @Getter
     private Map<Node, AbstractTreeNode> mapping;
 
     private List<Node> front;
@@ -288,11 +291,23 @@ public class ScriptTreeGraph {
                         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);
+
+                            List<BranchLabelNode> branchlabel = getBranchLabels(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode(), gn);
+
+                            BranchLabelNode branchNode;
+                            if(branchlabel != null) {
+                                //TODO: insertBranchLabels(branchlabel);
+
+                                branchNode = new BranchLabelNode(node, branchlabel.toString());
+                                mapping.put(node, branchNode);
+
+                            }else{
+                                branchNode = new BranchLabelNode(node, "Case " + branchcounter);
+                                mapping.put(node, branchNode);
+                                branchcounter++;
+                            }
+
                             putIntoFront(node);
-                            branchcounter++;
                         }
                 }
                 return null;
@@ -344,6 +359,30 @@ public class ScriptTreeGraph {
         }
     }
 
+
+    private List<BranchLabelNode> getBranchLabels(GoalNode<KeyData> parent, GoalNode<KeyData> child) {
+        List<BranchLabelNode> branchlabels = new ArrayList<>();
+        Node parentnode = parent.getData().getNode();
+        Node childnode = child.getData().getNode();
+        if(childnode.getNodeInfo().getBranchLabel() != null && isBranchLabel(childnode.getNodeInfo().getBranchLabel())) branchlabels.add( new BranchLabelNode(childnode, childnode.getNodeInfo().getBranchLabel()));
+        while(childnode.parent() != parentnode)  {
+            if(childnode.getNodeInfo().getBranchLabel() != null && isBranchLabel(childnode.getNodeInfo().getBranchLabel())) branchlabels.add( new BranchLabelNode(childnode, childnode.getNodeInfo().getBranchLabel()));
+            childnode = childnode.parent();
+        }
+        return branchlabels;
+    }
+
+    private boolean isBranchLabel(String label) {
+        if (label.contains("rule") || label.contains("rules")) return false;
+        return true;
+    }
+
+    private void insertBranchLabels(List<BranchLabelNode> branchlabels) {
+        if(branchlabels == null) return;
+
+
+    }
+
     private void addGoals() {
         front.forEach(k -> putIntoMapping(k, new DummyGoalNode(k, k.isClosed())));
     }

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

 package edu.kit.iti.formal.psdbg.gui.controls;
 
+import de.uka.ilkd.key.proof.Node;
+import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
+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 javafx.beans.property.MapProperty;
+import javafx.beans.property.SimpleMapProperty;
+import javafx.collections.FXCollections;
 import javafx.fxml.FXML;
 import javafx.scene.control.TreeCell;
 import javafx.scene.control.TreeItem;
@@ -7,12 +15,21 @@ import javafx.scene.control.TreeView;
 import javafx.scene.control.cell.TextFieldTreeCell;
 import javafx.scene.layout.BorderPane;
 import javafx.util.StringConverter;
+import lombok.Setter;
+
+import java.util.List;
+import java.util.Map;
 
 public class ScriptTreeView extends BorderPane {
+
+    @Setter
+    private ScriptTreeGraph stg;
+
+    private MapProperty<Node, String> colorOfNodes = new SimpleMapProperty<Node, String>(FXCollections.observableHashMap());
     @FXML
     TreeView<TreeNode> treeView;
 
-    public ScriptTreeView() {
+    public ScriptTreeView(DebuggerMain main) {
         Utils.createWithFXML(this);
         treeView.setCellFactory(this::cellFactory);
 
@@ -45,4 +62,80 @@ public class ScriptTreeView extends BorderPane {
         //colorOfNodes.addListener((InvalidationListener) o -> repaint(tftc));
         return tftc;
     }
+
+
+    /**
+     * returns treeItem that represents current Script tree
+     * @return
+     */
+
+    /*
+    public TreeItem<TreeNode> toView () {
+        TreeItem<TreeNode> treeItem;
+        ScriptTreeNode rootNode = stg.getRootNode();
+        Map<Node, AbstractTreeNode> mapping = stg.getMapping();
+        if(rootNode == null) {
+            treeItem = new TreeItem<>(new TreeNode("Proof", null));
+            DummyGoalNode dummy = new DummyGoalNode(null, false);
+            treeItem.getChildren().add(new TreeItem<>(dummy.toTreeNode()));
+            return treeItem;
+        }
+        treeItem = new TreeItem<>(new TreeNode("Proof", rootNode.getNode()));
+
+
+        List<AbstractTreeNode> children = mapping.get(rootNode.getNode()).getChildren();
+        if (children == null) return treeItem;
+        treeItem.getChildren().add(new TreeItem<>(mapping.get(rootNode.getNode()).toTreeNode()));
+
+        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)));
+        }
+        return treeItem;
+    }
+
+    private TreeItem<TreeNode> rekursiveToView (AbstractTreeNode current){
+        TreeItem<TreeNode> treeItem = new TreeItem<>(current.toTreeNode()); //
+
+        List<AbstractTreeNode> children = current.getChildren();
+
+
+        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;
+        }
+
+        if (children.size() != 0) {
+            children.forEach(k -> treeItem.getChildren().add(rekursiveToView(k)));
+        }
+        return treeItem;
+    }
+*/
+    private void repaint(TextFieldTreeCell<TreeNode> tftc) {
+        TreeNode item = tftc.getItem();
+        Node n = item.node;
+        tftc.setStyle("");
+        if (n != null) {
+            if (n.leaf() && !item.label.contains("BRANCH")) {
+                if (n.isClosed()) {
+                    colorOfNodes.putIfAbsent(n, "lightseagreen");
+                    //tftc.setStyle("-fx-background-color: greenyellow");
+                } else {
+                    colorOfNodes.putIfAbsent(n, "indianred");
+                }
+                if (colorOfNodes.containsKey(n)) {
+                    tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";");
+                }
+            }
+        }
+    }
 }

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

@@ -18,6 +18,7 @@
 
           </DockStation>-->
 
+
         <DockPane fx:id="dockStation"/>
 
         <!--