From a8d6499c8f18ac6f9b445795f83b806419554782 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Wed, 16 Aug 2017 22:37:11 +0200 Subject: [PATCH] Proof Tree --- .../kit/formal/gui/ProofScriptDebugger.java | 3 +- .../DebuggerMainWindowController.java | 27 ++- .../kit/formal/gui/controls/ProofTree.java | 187 ++++++++++++++++++ .../formal/interpreter/KeYProofFacade.java | 39 +++- src/main/resources/DebuggerMain.fxml | 1 + .../kit/formal/gui/controls/ProofTree.fxml | 11 ++ .../interpreter/KeYInterpreterTest.java | 2 +- 7 files changed, 256 insertions(+), 14 deletions(-) create mode 100644 src/main/java/edu/kit/formal/gui/controls/ProofTree.java create mode 100644 src/main/resources/edu/kit/formal/gui/controls/ProofTree.fxml diff --git a/src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java b/src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java index ca8f618d..e2611f34 100644 --- a/src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java +++ b/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); } } diff --git a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java index 821f26e7..615e928a 100644 --- a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java +++ b/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 task = FACADE.loadKeyFileTask(keyFile); + Task 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> { @Override protected Task> createTask() { diff --git a/src/main/java/edu/kit/formal/gui/controls/ProofTree.java b/src/main/java/edu/kit/formal/gui/controls/ProofTree.java new file mode 100644 index 00000000..be3a4db5 --- /dev/null +++ b/src/main/java/edu/kit/formal/gui/controls/ProofTree.java @@ -0,0 +1,187 @@ +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 = new SimpleObjectProperty<>(); + private ObjectProperty root = new SimpleObjectProperty<>(); + private MapProperty colorOfNodes = new SimpleMapProperty<>(FXCollections.observableHashMap()); + + @FXML + private TreeView 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 cellFactory(TreeView nodeTreeView) { + TextFieldTreeCell tftc = new TextFieldTreeCell<>(); + tftc.setConverter(new StringConverter() { + @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 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 rootProperty() { + return root; + } + + public Proof getProof() { + return proof.get(); + } + + public void setProof(Proof proof) { + this.proof.set(proof); + } + + public ObjectProperty proofProperty() { + return proof; + } +} + +class TreeItemNode extends TreeItem { + public TreeItemNode(Node value) { + super(value); + } + + @Override + public ObservableList> 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 diff --git a/src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java b/src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java index 8fe4021a..3aa03768 100644 --- a/src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java +++ b/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 loadKeyFileTask(File keYFile) { - Task task = new Task() { + public Task loadKeyFileTask(File keYFile) { + Task task = new Task() { @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> 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); diff --git a/src/main/resources/DebuggerMain.fxml b/src/main/resources/DebuggerMain.fxml index 2dc88a6e..beea2e4f 100644 --- a/src/main/resources/DebuggerMain.fxml +++ b/src/main/resources/DebuggerMain.fxml @@ -61,6 +61,7 @@ + diff --git a/src/main/resources/edu/kit/formal/gui/controls/ProofTree.fxml b/src/main/resources/edu/kit/formal/gui/controls/ProofTree.fxml new file mode 100644 index 00000000..44998c80 --- /dev/null +++ b/src/main/resources/edu/kit/formal/gui/controls/ProofTree.fxml @@ -0,0 +1,11 @@ + + + + + +
+ + + +
+ \ No newline at end of file diff --git a/src/test/java/edu/kit/formal/interpreter/KeYInterpreterTest.java b/src/test/java/edu/kit/formal/interpreter/KeYInterpreterTest.java index a41e7861..74d6c455 100644 --- a/src/test/java/edu/kit/formal/interpreter/KeYInterpreterTest.java +++ b/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 i = execute(getClass().getResourceAsStream("contraposition/testIsClosable.kps")); List> goals = i.getCurrentState().getGoals(); Assert.assertEquals(2, goals.size()); -- 2.26.2