graph for easier debugging

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java

@@ -161,10 +161,10 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
     }
 
     private Value evaluate(GoalNode<T> g, Expression expr) {
-        enterScope(expr);
+        //enterScope(expr);
         Evaluator<T> evaluator = new Evaluator<>(g.getAssignments(), g);
         evaluator.setMatcher(matcherApi);
-        exitScope(expr);
+        //exitScope(expr);
         return evaluator.eval(expr);
     }
 

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

@@ -114,7 +114,7 @@ public class ContractChooser extends Dialog<Contract> {
                 text.getChildren().add(contract);
                 text.getChildren().add(name);
                 text.getChildren().add(new Text("\n"));
-                //text.getChildren().add(tcontent);
+                //text.getChildren().addCell(tcontent);
 
                 for (String line : content.split("\n")) {
                     if (line.contains(":")) {

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

@@ -20,6 +20,8 @@ import edu.kit.iti.formal.psdbg.examples.Examples;
 import edu.kit.iti.formal.psdbg.fmt.DefaultFormatter;
 import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger;
 import edu.kit.iti.formal.psdbg.gui.controls.*;
+import edu.kit.iti.formal.psdbg.gui.graph.Graph;
+import edu.kit.iti.formal.psdbg.gui.graph.GraphView;
 import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel;
 import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
 import edu.kit.iti.formal.psdbg.gui.model.InterpreterThreadState;
@@ -69,8 +71,6 @@ import java.util.*;
 import java.util.concurrent.*;
 import java.util.stream.Collectors;
 
-import org.reactfx.util.Timer;
-
 /**
  * Controller for the Debugger MainWindow
  *
@@ -88,76 +88,53 @@ public class DebuggerMain implements Initializable {
 
     @Getter
     private final DebuggerMainModel model = new DebuggerMainModel();
+    private final GraphView graphView = new GraphView();
+    private final Graph.PTreeGraph graph = graphView.getGraph();
 
+    private final DockNode graphViewNode = new DockNode(graphView, "Debug graph");
     private InspectionViewsController inspectionViewsController;
-
     private ScriptController scriptController;
-
     @FXML
     private DebuggerStatusBar statusBar;
-
     @FXML
     private DockPane dockStation;
-
     @FXML
     private ToggleButton togBtnCommandHelp;
-
     @FXML
     private ToggleButton togBtnProofTree;
-
     @FXML
     private ToggleButton togBtnActiveInspector;
-
     @FXML
     private ToggleButton togBtnWelcome;
-
     @FXML
     private ToggleButton togBtnCodeDock;
-
     @FXML
     private CheckMenuItem miCommandHelp;
-
     @FXML
     private CheckMenuItem miCodeDock;
-
     @FXML
     private CheckMenuItem miWelcomeDock;
-
     @FXML
     private CheckMenuItem miActiveInspector;
-
     @FXML
     private CheckMenuItem miProofTree;
-
     @FXML
     private ToggleButton btnInteractiveMode;
-
     private JavaArea javaArea = new JavaArea();
-
     private DockNode javaAreaDock = new DockNode(javaArea, "Java Source",
             new MaterialDesignIconView(MaterialDesignIcon.CODEPEN)
     );
-
     //-----------------------------------------------------------------------------------------------------------------
     private ProofTree proofTree = new ProofTree();
-
     private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree");
-
     private WelcomePane welcomePane = new WelcomePane(this);
-
     private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT));
-
     private DockNode activeInspectorDock;
-
     private CommandHelp commandHelp = new CommandHelp();
-
     private DockNode commandHelpDock = new DockNode(commandHelp, "DebuggerCommand Help");
-
     private InteractiveModeController interactiveModeController;
-
     @FXML
     private Menu examplesMenu;
-
     private Timer interpreterThreadTimer;
 
     @Subscribe
@@ -303,6 +280,8 @@ public class DebuggerMain implements Initializable {
      * @see {@link #handleStatePointer(PTreeNode)}
      */
     private void handleStatePointerUI(PTreeNode<KeyData> node) {
+        graph.addPartiallyAndMark(node);
+
         if (node != null) {
             getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt());
             scriptController.getDebugPositionHighlighter().highlight(node.getStatement());
@@ -326,7 +305,7 @@ public class DebuggerMain implements Initializable {
             showCodeDock(null);
         });
 
-        //add listener for linehighlighting when changing selection in inspectionview
+        //addCell listener for linehighlighting when changing selection in inspectionview
         getInspectionViewsController().getActiveInspectionViewTab().getModel().highlightedJavaLinesProperty().
                 addListener((observable, oldValue, newValue) -> {
                     if (newValue != null) {
@@ -346,6 +325,19 @@ public class DebuggerMain implements Initializable {
 
     }
 
+    //region Actions: Menu
+
+    /*@FXML
+    public void saveAsScript() throws IOException {
+        File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps");
+        if (f != null) {
+           /* if(!f.exists()){
+                f.createNewFile();
+            }
+            saveScript(f);
+        }
+    }*/
+
     public KeYProofFacade getFacade() {
         return FACADE;
     }
@@ -365,19 +357,6 @@ public class DebuggerMain implements Initializable {
         });
     }
 
-    //region Actions: Menu
-
-    /*@FXML
-    public void saveAsScript() throws IOException {
-        File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps");
-        if (f != null) {
-           /* if(!f.exists()){
-                f.createNewFile();
-            }
-            saveScript(f);
-        }
-    }*/
-
     public void showCodeDock(ActionEvent actionEvent) {
         if (!javaAreaDock.isDocked()) {
             javaAreaDock.dock(dockStation, DockPos.RIGHT);
@@ -474,7 +453,6 @@ public class DebuggerMain implements Initializable {
         }
     }
 
-
     /**
      * Execute the script that with using the interpreter that is build using the interpreterbuilder
      *
@@ -535,12 +513,46 @@ public class DebuggerMain implements Initializable {
         });
     }
 
+    @FXML
+    public void debugGraph(ActionEvent event) {
+        if (!graphViewNode.isDocked() && !graphViewNode.isFloating()) {
+            graphViewNode.dock(dockStation, DockPos.CENTER);
+        }
+
+        graph.clear(true);
+
+        for (PTreeNode<KeyData> n : model.getDebuggerFramework().getStates()) {
+            graph.addCell(n);
+        }
+
+        for (PTreeNode<KeyData> n : model.getDebuggerFramework().getStates()) {
+            if (n.getStepOver() != null) {
+                graph.addEdge(n, n.getStepOver(), "over");
+            }
+            if (n.getStepInto() != null) {
+                graph.addEdge(n, n.getStepInto(), "into");
+            }
+            if (n.getStepInvOver() != null) {
+                graph.addEdge(n, n.getStepInvOver(), "revo");
+            }
+            if (n.getStepInvInto() != null) {
+                graph.addEdge(n, n.getStepInvInto(), "otni");
+            }
+            if (n.getStepReturn() != null) {
+                graph.addEdge(n, n.getStepReturn(), "rtrn");
+            }
+        }
+    }
+
     @FXML
     public void debugPrintDot(@Nullable ActionEvent ae) {
         if (model.getDebuggerFramework() == null) {
             statusBar.publishErrorMessage("can print debug info, no debugger started!");
             return;
         }
+
+        debugGraph(ae);
+
         try (PrintWriter out = new PrintWriter(new FileWriter("debug.dot"))) {
             out.println("digraph G {");
             for (PTreeNode<KeyData> n : model.getDebuggerFramework().getStates()) {
@@ -729,6 +741,7 @@ public class DebuggerMain implements Initializable {
 
     /**
      * Reload a problem from the beginning
+     *
      * @param event
      */
     @FXML
@@ -765,6 +778,7 @@ public class DebuggerMain implements Initializable {
 
 
     }
+
     @FXML
     public void closeProgram() {
         System.exit(0);
@@ -914,6 +928,7 @@ public class DebuggerMain implements Initializable {
     /**
      * Perform a step back
      * Does stepinto back
+     *
      * @param actionEvent
      */
     public void stepBack(ActionEvent actionEvent) {
@@ -1048,7 +1063,7 @@ public class DebuggerMain implements Initializable {
         webEngine.load(url);
         DockNode dn = new DockNode(browser);
         dn.setTitle("ScriptLanguage Description");
-        //this.dockStation.getChildren().add(dn);
+        //this.dockStation.getChildren().addCell(dn);
         dn.dock(dockStation, DockPos.LEFT);
     }
 

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

@@ -77,7 +77,7 @@ public class Events {
     @RequiredArgsConstructor
     /**
      * Event that should be fired when a new goal node was created to inform view
-     * components s.t. they can update their view
+     * components s.t. they can updateTarget their view
      */
     public static class EventForNewGoalView {
         private final ASTNode correspodingASTNode;

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

@@ -41,7 +41,7 @@ public class ASTNodeHiglightListener<T> {
         if (currentInterpreter != null) deinstall(interpreter);
         int i = interpreter.getEntryListeners().size();
         interpreter.getEntryListeners().add(0, list);
-        //    interpreter.getExitListeners().add(0, exitListener);
+        //    interpreter.getExitListeners().addCell(0, exitListener);
         currentInterpreter = interpreter;
     }
 

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

@@ -143,7 +143,7 @@ public class InspectionView extends BorderPane {
                     Mode.LIVING.name(),
                     Mode.POSTMORTEM.name()
             );
-            getStyleClass().add(mode.get().name());
+            getStyleClass().addCell(mode.get().name());
         });
          */
     }

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

@@ -344,9 +344,9 @@ public class ProofTree extends BorderPane {
 
            /* if(!label.equals("Proof")) {
                 TreeItem<TreeNode> self = new TreeItem<>(new TreeNode(n.serialNr() + ": " + toString(n), n));
-                ti.getChildren().add(self);
+                ti.getChildren().addCell(self);
             }*/
-            // ti.getChildren().add(e);
+            // ti.getChildren().addCell(e);
 
 
             return ti;
@@ -373,7 +373,7 @@ public class ProofTree extends BorderPane {
 
                     TreeItem<TreeNode> populate = populate(childNode.getNodeInfo().getBranchLabel(), childNode);
                     // TreeItem<TreeNode> self = new TreeItem<>(new TreeNode(childNode.serialNr() + ": " + toString(childNode), childNode));
-                    // populate.getChildren().add(0, self);
+                    // populate.getChildren().addCell(0, self);
                     ti.getChildren().add(populate);
 
                 } else {
@@ -385,11 +385,11 @@ public class ProofTree extends BorderPane {
                 }
             }
 
-/*            node.childrenIterator().forEachRemaining(child -> ti.getChildren().add(
+/*            node.childrenIterator().forEachRemaining(child -> ti.getChildren().addCell(
                     populate(child.getNodeInfo().getBranchLabel(), child)));
 */
             //node.children().forEach(child ->
-            //        ti.getChildren().add(populate(child.getNodeInfo().getBranchLabel(), child)));
+            //        ti.getChildren().addCell(populate(child.getNodeInfo().getBranchLabel(), child)));
         }
 
         return ti;

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

@@ -337,13 +337,13 @@ public class ScriptArea extends BorderPane {
             codeArea.setStyleSpans(0, codeArea.getStyleSpans(0, getExecutionMarkerPosition()).mapStyles(styleMapper));
 
 
-            //this results in a NotSupportedOperation Exception because the add to an immutable list is not allowed
+            //this results in a NotSupportedOperation Exception because the addCell to an immutable list is not allowed
            /* getStyleSpans(0, getExecutionMarkerPosition()).forEach(span -> {
                 Collection<String> style = span.getStyle();
                 if (style.isEmpty()) {
                     setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA"));
                 } else {
-                    style.add("NON_EXE_AREA");
+                    style.addCell("NON_EXE_AREA");
                 }
             });
 */

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

@@ -117,7 +117,7 @@ public class SequentMatcher extends BorderPane {
                 services);
         ObservableList<Map<String, MatchPath>> resultlist = FXCollections.observableArrayList(matchings);
 
-        //If no matchings found, add "No matchings found"
+        //If no matchings found, addCell "No matchings found"
         if (resultlist.isEmpty()) {
             matchingsView.setVisible(false);
             nomatchings.setVisible(true);

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

@@ -257,7 +257,7 @@ public class TacletContextMenu extends ContextMenu {
 
             // Items for insertion of hidden terms appear in a submenu.
             /*if (insertHiddenController.isResponsible(item)) {
-                insertHiddenController.add(item);
+                insertHiddenController.addCell(item);
             } else */
             {
                 // If one of the sets contains the rule it is considered rare
@@ -415,10 +415,10 @@ public class TacletContextMenu extends ContextMenu {
                                     String inputText) {
         TextInputDialog dialog = new TextInputDialog(inputText);
 
-        // Get the Stage and add KeY Icon.
+        // Get the Stage and addCell KeY Icon.
        /* Stage stage = (Stage) dialog.getDialogPane().getScene().getWindow();
         stage.getIcons()
-                .add(new Image(NUIConstants.KEY_APPLICATION_WINDOW_ICON_PATH));
+                .addCell(new Image(NUIConstants.KEY_APPLICATION_WINDOW_ICON_PATH));
         dialog.setTitle("Abbreviation Dialog");
         dialog.setHeaderText(header);
         dialog.setContentText(message);

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

@@ -261,8 +261,8 @@ public class Utils {
 
         GridPane expContent = new GridPane();
         expContent.setMaxWidth(Double.MAX_VALUE);
-        expContent.add(label, 0, 0);
-        expContent.add(textArea, 0, 1);
+        expContent.addCell(label, 0, 0);
+        expContent.addCell(textArea, 0, 1);
 
         alert.getDialogPane().setExpandableContent(expContent);
         */

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Cell.java

+package edu.kit.iti.formal.psdbg.gui.graph;
+
+import javafx.scene.Node;
+import javafx.scene.control.Label;
+import javafx.scene.input.DragEvent;
+import javafx.scene.layout.Pane;
+import javafx.scene.layout.VBox;
+import lombok.Getter;
+import lombok.RequiredArgsConstructor;
+import lombok.Setter;
+
+import java.util.Arrays;
+
+@RequiredArgsConstructor
+public class Cell<T> extends Pane {
+    @Getter
+    private final T cellId;
+
+    /**
+     * if true, this cell is handled by the layouter.
+     */
+    @Getter
+    @Setter
+    private boolean invalid = true;
+
+    private Dragger dragger = new Dragger(this);
+
+    public Cell(T cellId, Node... children) {
+        super(children);
+        getStyleClass().add("graph-cell");
+        this.cellId = cellId;
+    }
+
+    public Cell(T cellId, String... children) {
+        getStyleClass().add("graph-cell");
+        this.cellId = cellId;
+        VBox hbox = new VBox();
+        hbox.getStyleClass().add("vbox");
+        getChildren().addAll(hbox);
+        Arrays.stream(children).forEachOrdered(s -> hbox.getChildren().add(new Label(s)));
+    }
+}
+
+class Dragger {
+    private double mouseX;
+    private double mouseY;
+
+    public Dragger(Node node) {
+        assert node != null;
+        node.setOnMousePressed(event -> {
+            mouseX = event.getSceneX();
+            mouseY = event.getSceneY();
+        });
+
+        node.setOnMouseDragged(event -> {
+            double deltaX = event.getSceneX() - mouseX;
+            double deltaY = event.getSceneY() - mouseY;
+            node.relocate(node.getLayoutX() + deltaX, node.getLayoutY() + deltaY);
+            mouseX = event.getSceneX();
+            mouseY = event.getSceneY();
+        });
+    }
+}
+
+

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/CellLayer.java

+package edu.kit.iti.formal.psdbg.gui.graph;
+
+import javafx.scene.layout.Pane;
+
+public class CellLayer extends Pane {
+
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Edge.java

+package edu.kit.iti.formal.psdbg.gui.graph;
+
+import javafx.beans.Observable;
+import javafx.beans.property.SimpleObjectProperty;
+import javafx.beans.value.ObservableValue;
+import javafx.geometry.Point2D;
+import javafx.scene.Group;
+import javafx.scene.control.Label;
+import javafx.scene.paint.Paint;
+import javafx.scene.shape.*;
+
+import java.util.Random;
+
+public class Edge<T> extends Group {
+    private static Random r = new Random();
+    protected SimpleObjectProperty<Cell<T>> source = new SimpleObjectProperty<>(), target = new SimpleObjectProperty<>();
+    private Line line = new Line();
+    private Label label = new Label();
+    private Circle circle = new Circle();
+    private double shiftX, shiftY;
+
+    public Edge(Cell<T> source, Cell<T> target, String label) {
+        setSource(source);
+        setTarget(target);
+
+        shiftX = r.nextInt(50) - 25;
+        shiftY = r.nextInt(50) - 25;
+
+        line = new Line();
+        line.getStyleClass().addAll("edge", label);
+        circle.getStyleClass().addAll("edge", label);
+        this.label.getStyleClass().addAll("edge-label", label);
+        this.label.setText(label);
+        this.source.addListener(this::renewNode);
+        this.target.addListener(this::renewNode);
+
+
+        renewNode(this.source, null, source);
+        renewNode(this.target, null, target);
+
+        getChildren().addAll(line, this.label, circle);
+        redraw();
+    }
+
+    private void renewNode(ObservableValue<? extends Cell> observableValue, Cell<T> old, Cell<T> nValue) {
+        if (old != null) {
+            old.layoutBoundsProperty().removeListener(this::redraw);
+            old.layoutXProperty().removeListener(this::redraw);
+            old.layoutYProperty().removeListener(this::redraw);
+        }
+        if (nValue != null) {
+            nValue.layoutBoundsProperty().addListener(this::redraw);
+            nValue.layoutXProperty().addListener(this::redraw);
+            nValue.layoutYProperty().addListener(this::redraw);
+        }
+        redraw();
+    }
+
+    void redraw() {
+        redraw(null);
+    }
+
+    void redraw(Observable observable) {
+        double x1, y1, x2, y2;
+        if (getSource() == null || getTarget() == null) {
+            x1 = y1 = x2 = y2 = 0;
+        } else {
+
+            x1 = getSource().getLayoutX() + getSource().getBoundsInParent().getWidth() / 2.0;
+            x2 = getTarget().getLayoutX() + getTarget().getBoundsInParent().getWidth() / 2.0;
+
+            y1 = getSource().getLayoutY() + getSource().getBoundsInParent().getHeight() / 2.0;
+            y2 = getTarget().getLayoutY() + getTarget().getBoundsInParent().getHeight() / 2.0;
+
+        }
+
+        Point2D start = new Point2D(x1, y1);
+        Point2D end = new Point2D(x2, y2);
+
+        Point2D midpoint = start.midpoint(end);
+
+        label.relocate(midpoint.getX() + shiftX, shiftY + midpoint.getY());
+
+        line.setStartX(x1);
+        line.setStartY(y1);
+        line.setEndX(x2);
+        line.setEndY(y2);
+
+        circle.setCenterX(x2);
+        circle.setCenterY(y2);
+        circle.setRadius(15);
+
+        if (getTarget() != null) {
+            end = correctToRectangle(getTarget().getLayoutX(),
+                    getTarget().getLayoutY(), getTarget().getWidth(), getTarget().getHeight());
+            if (end != null) {
+                circle.setCenterX(end.getX());
+                circle.setCenterY(end.getY());
+
+                line.setEndX(end.getX());
+                line.setEndY(end.getY());
+            }
+        }
+    }
+
+    private Point2D correctToRectangle(double x, double y, double width, double height) {
+        Rectangle r = new Rectangle(x, y, width, height);
+        r.setStroke(Paint.valueOf("black"));
+        r.setStrokeWidth(1);
+        r.setFill(null);
+        try {
+            Path inter = (Path) Shape.intersect(line, r);
+            MoveTo mt = (MoveTo) inter.getElements().get(0);
+            return new Point2D(mt.getX(), mt.getY());
+        } catch (ClassCastException | IndexOutOfBoundsException cce) {
+            //cce.printStackTrace();
+        }
+        return null;
+    }
+
+    public Cell getSource() {
+        return source.get();
+    }
+
+    public void setSource(Cell source) {
+        this.source.set(source);
+    }
+
+    public SimpleObjectProperty<Cell<T>> sourceProperty() {
+        return source;
+    }
+
+    public Cell getTarget() {
+        return target.get();
+    }
+
+    public void setTarget(Cell target) {
+        this.target.set(target);
+    }
+
+    public SimpleObjectProperty<Cell<T>> targetProperty() {
+        return target;
+    }
+}
\ No newline at end of file