Proof Tree

src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java

@@ -58,8 +58,9 @@ public class ProofScriptDebugger extends Application {
             //logger.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
 
 
-        } catch (IOException e) {
+        } catch (Exception e) {
             e.printStackTrace();
+            System.exit(1);
         }
     }
 

src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java

@@ -2,6 +2,7 @@ package edu.kit.formal.gui.controller;
 
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
+import de.uka.ilkd.key.api.ProofApi;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.speclang.Contract;
 import edu.kit.formal.gui.ProofScriptDebugger;
@@ -84,6 +85,8 @@ public class DebuggerMainWindowController implements Initializable {
 
 
     //-----------------------------------------------------------------------------------------------------------------
+    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 = inspectionViewsController.getActiveInterpreterTabDock();
@@ -122,6 +125,17 @@ public class DebuggerMainWindowController implements Initializable {
         //statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
         marriageJavaCode();
 
+        //marriage key proof facade to proof tree
+        getFacade().proofProperty().addListener(
+                (prop, o, n) -> {
+                    proofTree.setRoot(n.root());
+                    proofTree.setProof(n);
+                    getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals());
+                }
+        );
+
+
+
         //Debugging
         Utils.addDebugListener(javaCode);
         Utils.addDebugListener(executeNotPossible, "executeNotPossible");
@@ -133,6 +147,7 @@ public class DebuggerMainWindowController implements Initializable {
     /**
      * Connects the proof tree controller with the model of the active inspection view model.
      */
+
     private void marriageProofTreeControllerWithActiveInspectionView() {
         InspectionModel imodel = getInspectionViewsController().getActiveInspectionViewTab().getModel();
 
@@ -386,11 +401,10 @@ public class DebuggerMainWindowController implements Initializable {
         if (keyFile != null) {
             setKeyFile(keyFile);
             setInitialDirectory(keyFile.getParentFile());
-            Task<Void> task = FACADE.loadKeyFileTask(keyFile);
+            Task<ProofApi> task = FACADE.loadKeyFileTask(keyFile);
             task.setOnSucceeded(event -> {
                 statusBar.publishMessage("Loaded key sourceName: %s", keyFile);
                 statusBar.stopProgress();
-                getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals());
             });
 
             task.setOnFailed(event -> {
@@ -418,7 +432,6 @@ public class DebuggerMainWindowController implements Initializable {
     }
 
 
-
     //endregion
 
     //region Santa's Little Helper
@@ -548,6 +561,13 @@ public class DebuggerMainWindowController implements Initializable {
         }
     }
 
+    @FXML
+    public void showProofTree(ActionEvent actionEvent) {
+        if (!proofTreeDock.isDocked() && !proofTreeDock.isFloating()) {
+            proofTreeDock.dock(dockStation, DockPos.CENTER);
+        }
+    }
+
     public DockNode getJavaAreaDock() {
         return javaAreaDock;
     }
@@ -656,6 +676,7 @@ public class DebuggerMainWindowController implements Initializable {
         return initialDirectory;
     }
 
+
     public class ContractLoaderService extends Service<List<Contract>> {
         @Override
         protected Task<List<Contract>> createTask() {

src/main/java/edu/kit/formal/gui/controls/ProofTree.java

+package edu.kit.formal.gui.controls;
+
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.ProofTreeEvent;
+import de.uka.ilkd.key.proof.ProofTreeListener;
+import javafx.beans.InvalidationListener;
+import javafx.beans.property.MapProperty;
+import javafx.beans.property.ObjectProperty;
+import javafx.beans.property.SimpleMapProperty;
+import javafx.beans.property.SimpleObjectProperty;
+import javafx.collections.FXCollections;
+import javafx.collections.ObservableList;
+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;
+
+import java.util.stream.Collectors;
+
+public class ProofTree extends BorderPane {
+    private ObjectProperty<Proof> proof = new SimpleObjectProperty<>();
+    private ObjectProperty<Node> root = new SimpleObjectProperty<>();
+    private MapProperty colorOfNodes = new SimpleMapProperty<>(FXCollections.observableHashMap());
+
+    @FXML
+    private TreeView<Node> treeProof;
+    private ProofTreeListener proofTreeListener = new ProofTreeListener() {
+        @Override
+        public void proofExpanded(ProofTreeEvent proofTreeEvent) {
+            treeProof.refresh();
+        }
+
+        @Override
+        public void proofIsBeingPruned(ProofTreeEvent proofTreeEvent) {
+
+        }
+
+        @Override
+        public void proofPruned(ProofTreeEvent proofTreeEvent) {
+            treeProof.refresh();
+        }
+
+        @Override
+        public void proofStructureChanged(ProofTreeEvent proofTreeEvent) {
+            treeProof.refresh();
+        }
+
+        @Override
+        public void proofClosed(ProofTreeEvent proofTreeEvent) {
+            treeProof.refresh();
+        }
+
+        @Override
+        public void proofGoalRemoved(ProofTreeEvent proofTreeEvent) {
+            treeProof.refresh();
+        }
+
+        @Override
+        public void proofGoalsAdded(ProofTreeEvent proofTreeEvent) {
+            treeProof.refresh();
+        }
+
+        @Override
+        public void proofGoalsChanged(ProofTreeEvent proofTreeEvent) {
+            treeProof.refresh();
+        }
+
+        @Override
+        public void smtDataUpdate(ProofTreeEvent proofTreeEvent) {
+
+        }
+
+        @Override
+        public void notesChanged(ProofTreeEvent proofTreeEvent) {
+
+        }
+    };
+
+    public ProofTree() {
+        Utils.createWithFXML(this);
+        treeProof.setCellFactory(this::cellFactory);
+        root.addListener(o -> init());
+        proof.addListener((prop, old, n) -> {
+            if (old != null) {
+                old.removeProofTreeListener(proofTreeListener);
+            }
+            n.addProofTreeListener(proofTreeListener);
+        });
+        init();
+    }
+
+    private TreeCell<Node> cellFactory(TreeView<Node> nodeTreeView) {
+        TextFieldTreeCell<Node> tftc = new TextFieldTreeCell<>();
+        tftc.setConverter(new StringConverter<Node>() {
+            @Override
+            public String toString(Node object) {
+                return object.sequent().toString();
+            }
+
+            @Override
+            public Node fromString(String string) {
+                return null;
+            }
+        });
+        tftc.itemProperty().addListener((p, o, n) -> repaint(tftc));
+        colorOfNodes.addListener((InvalidationListener) o -> repaint(tftc));
+        return tftc;
+    }
+
+    private void repaint(TextFieldTreeCell<Node> tftc) {
+        Node n = tftc.getItem();
+        tftc.setStyle("");
+        if (n != null) {
+            if (n.isClosed()) {
+                tftc.setStyle("-fx-background-color: greenyellow");
+            }
+            if (colorOfNodes.containsKey(n)) {
+                tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";");
+            }
+        }
+    }
+
+    private void init() {
+        if (root.get() != null)
+            treeProof.setRoot(new TreeItemNode(root.get()));
+        treeProof.refresh();
+    }
+
+    public Object getColorOfNodes() {
+        return colorOfNodes.get();
+    }
+
+    public void setColorOfNodes(Object colorOfNodes) {
+        this.colorOfNodes.set(colorOfNodes);
+    }
+
+    public MapProperty colorOfNodesProperty() {
+        return colorOfNodes;
+    }
+
+    public Node getRoot() {
+        return root.get();
+    }
+
+    public void setRoot(Node root) {
+        this.root.set(root);
+    }
+
+    public ObjectProperty<Node> rootProperty() {
+        return root;
+    }
+
+    public Proof getProof() {
+        return proof.get();
+    }
+
+    public void setProof(Proof proof) {
+        this.proof.set(proof);
+    }
+
+    public ObjectProperty<Proof> proofProperty() {
+        return proof;
+    }
+}
+
+class TreeItemNode extends TreeItem<Node> {
+    public TreeItemNode(Node value) {
+        super(value);
+    }
+
+    @Override
+    public ObservableList<TreeItem<Node>> getChildren() {
+        if (super.getChildren().size() != getValue().children().size())
+            super.getChildren().setAll(
+                    getValue().children().stream().map(TreeItemNode::new).collect(Collectors.toList()));
+        return super.getChildren();
+    }
+
+    @Override
+    public boolean isLeaf() {
+        return getValue().leaf();
+    }
+}
\ No newline at end of file

src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java

@@ -11,6 +11,7 @@ import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.speclang.Contract;
 import edu.kit.formal.interpreter.data.GoalNode;
 import edu.kit.formal.interpreter.data.KeyData;
+import javafx.application.Platform;
 import javafx.beans.binding.BooleanBinding;
 import javafx.beans.property.SimpleObjectProperty;
 import javafx.concurrent.Task;
@@ -24,6 +25,7 @@ import java.util.List;
 
 /**
  * Facade to KeY. Build part of the interpreter
+ *
  * @author S. Grebing
  * @author A. Weigl
  */
@@ -53,23 +55,45 @@ public class KeYProofFacade {
     private ProofManagementApi pma;
 
     //region loading
-    public Task<Void> loadKeyFileTask(File keYFile) {
-        Task<Void> task = new Task<Void>() {
+    public Task<ProofApi> loadKeyFileTask(File keYFile) {
+        Task<ProofApi> task = new Task<ProofApi>() {
             @Override
-            protected Void call() throws Exception {
-                loadKeyFile(keYFile);
-                return null;
+            protected ProofApi call() throws Exception {
+                ProofApi pa = loadKeyFile(keYFile);
+                return pa;
+            }
+
+            @Override
+            protected void succeeded() {
+                System.out.println("KeYProofFacade.succeeded");
+                environment.set(getValue().getEnv());
+                proof.set(getValue().getProof());
+                contract.set(null);
             }
         };
+
         return task;
     }
 
-    public void loadKeyFile(File keYFile) throws ProblemLoaderException {
+    /**
+     * This method does not set the environment or proof property, because of threading reason
+     *
+     * @param keYFile
+     * @return
+     * @throws ProblemLoaderException
+     */
+    ProofApi loadKeyFile(File keYFile) throws ProblemLoaderException {
         ProofManagementApi pma = KeYApi.loadFromKeyFile(keYFile);
         ProofApi pa = pma.getLoadedProof();
+        return pa;
+    }
+
+    public ProofApi loadKeyFileSync(File keyFile) throws ProblemLoaderException {
+        ProofApi pa = loadKeyFile(keyFile);
         environment.set(pa.getEnv());
         proof.set(pa.getProof());
         contract.set(null);
+        return pa;
     }
 
     public Task<List<Contract>> getContractsForJavaFileTask(File javaFile) {
@@ -98,7 +122,6 @@ public class KeYProofFacade {
 
     /**
      * Build the KeYInterpreter that handles the execution of the loaded key problem sourceName
-     *
      */
     public InterpreterBuilder buildInterpreter() {
         assert readyToExecute.getValue();
@@ -118,8 +141,6 @@ public class KeYProofFacade {
 
     /**
      * Reload all KeY structure if proof should be reloaded
-     *
-     * @param fileToLoad
      */
     public void reloadEnvironment() {
         setProof(null);

src/main/resources/DebuggerMain.fxml

@@ -61,6 +61,7 @@
                                 <MenuItem onAction="#showCodeDock" text="Show Java Code window"/>
                                 <MenuItem onAction="#showWelcomeDock" text="Show Welcome window"/>
                                 <MenuItem onAction="#showActiveInspector" text="Show Active Inspector window"/>
+                                <MenuItem onAction="#showProofTree" text="Show Proof Tree"/>
                             </items>
                         </Menu>
                         <Menu text="Help">

src/main/resources/edu/kit/formal/gui/controls/ProofTree.fxml

+<?xml version="1.0" encoding="UTF-8"?>
+
+<?import javafx.scene.control.TreeView?>
+<?import javafx.scene.layout.BorderPane?>
+<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="treeProof" editable="false">
+
+        </TreeView>
+    </center>
+</fx:root>
\ No newline at end of file

src/test/java/edu/kit/formal/interpreter/KeYInterpreterTest.java

@@ -36,7 +36,7 @@ public class KeYInterpreterTest {
 
     @Test
     public void testIsClosable() throws IOException, ProblemLoaderException {
-        facade.loadKeyFile(new File("src/test/resources/edu/kit/formal/interpreter/contraposition/contraposition.key"));
+        facade.loadKeyFileSync(new File("src/test/resources/edu/kit/formal/interpreter/contraposition/contraposition.key"));
         Interpreter<KeyData> i = execute(getClass().getResourceAsStream("contraposition/testIsClosable.kps"));
         List<GoalNode<KeyData>> goals = i.getCurrentState().getGoals();
         Assert.assertEquals(2, goals.size());