diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/CommandHandler.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/CommandHandler.java index a6b95596d9b6df36ee4beed4688c45c6350d22a0..323ab7a0ddc163d7e43657d77470a303bad6e784 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/CommandHandler.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/CommandHandler.java @@ -28,7 +28,7 @@ public interface CommandHandler { VariableAssignment params); default boolean isAtomic() { - return false; + return true; } /** diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptHandler.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptHandler.java index 2f679042a091c7a27179f7c1e032f712a629f724..08fe0ed47a54aa78115e7f80329477b8a3a05621 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptHandler.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptHandler.java @@ -98,7 +98,7 @@ public class ProofScriptHandler implements CommandHandler { @Override public boolean isAtomic() { - return true; + return false; } public void addScripts(List ast) { diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java index cbe735765995254e81c71d60abb75b3281a82313..73985b580191162f1874b258076c053cd2e2a59b 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java @@ -6,6 +6,9 @@ import com.google.common.eventbus.Subscribe; 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.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.speclang.Contract; @@ -40,6 +43,7 @@ import javafx.scene.web.WebEngine; import javafx.scene.web.WebView; import javafx.stage.FileChooser; import lombok.Getter; +import lombok.RequiredArgsConstructor; import org.antlr.v4.runtime.RecognitionException; import org.apache.commons.io.FileUtils; import org.apache.logging.log4j.LogManager; @@ -63,6 +67,7 @@ import java.util.Optional; import java.util.ResourceBundle; import java.util.Set; import java.util.concurrent.*; +import java.util.stream.Collectors; /** * Controller for the Debugger MainWindow @@ -787,6 +792,10 @@ public class DebuggerMain implements Initializable { public void stepInto(ActionEvent actionEvent) { LOGGER.debug("DebuggerMain.stepOver"); try { + if (model.getDebuggerFramework().getStatePointer().isAtomic()) { + model.getDebuggerFramework().getStatePointerListener() + .add(new StepIntoHandler(model.getStatePointer())); + } model.getDebuggerFramework().execute(new StepIntoCommand<>()); } catch (DebuggerException e) { Utils.showExceptionDialog("", "", "", e); @@ -794,6 +803,11 @@ public class DebuggerMain implements Initializable { } } + private void handleStepInto(PTreeNode newState) { + + + } + /** * Perform a step back * @@ -931,6 +945,38 @@ public class DebuggerMain implements Initializable { return FACADE.getContractsForJavaFileTask(model.getJavaFile()); } } + + @RequiredArgsConstructor + private class StepIntoHandler implements java.util.function.Consumer> { + private final PTreeNode original; + + @Override + public void accept(PTreeNode keyDataPTreeNode) { + Platform.runLater(this::acceptUI); + } + + public void acceptUI() { + model.getDebuggerFramework().getStatePointerListener().remove(this); + GoalNode beforeNode = original.getStateBeforeStmt().getSelectedGoalNode(); + ProofTree ptree = new ProofTree(); + Proof proof = beforeNode.getData().getProof(); + Node pnode = beforeNode.getData().getNode(); + + ptree.setProof(proof); + ptree.setRoot(pnode); + ptree.setDeactivateRefresh(true); + + Set sentinels = proof.getSubtreeGoals(pnode) + .stream() + .map(Goal::node) + .collect(Collectors.toSet()); + ptree.getSentinels().addAll(sentinels); + DockNode node = new DockNode(ptree, "Proof Tree for Step Into: " + + original.getStatement().accept(new ShortCommandPrinter()) + ); + node.dock(dockStation, DockPos.CENTER, getActiveInspectorDock()); + } + } //endregion } //deprecated diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java index dfc97462fcc548f3dc917ac7afc170d30df8f3bc..970b1a3a3afbbb06c9e48b0c10b22596341e5e61 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java @@ -11,11 +11,9 @@ import de.uka.ilkd.key.proof.ProofTreeListener; import edu.kit.iti.formal.psdbg.LabelFactory; import edu.kit.iti.formal.psdbg.gui.controller.Events; import javafx.application.Platform; -import javafx.beans.property.MapProperty; -import javafx.beans.property.ObjectProperty; -import javafx.beans.property.SimpleMapProperty; -import javafx.beans.property.SimpleObjectProperty; +import javafx.beans.property.*; import javafx.collections.FXCollections; +import javafx.collections.ObservableSet; import javafx.fxml.FXML; import javafx.scene.control.*; import javafx.scene.control.cell.TextFieldTreeCell; @@ -40,11 +38,21 @@ public class ProofTree extends BorderPane { private ObjectProperty root = new SimpleObjectProperty<>(); + private SetProperty sentinels = new SimpleSetProperty<>(FXCollections.observableSet()); + + private MapProperty colorOfNodes = new SimpleMapProperty<>(FXCollections.observableHashMap()); @FXML private TreeView treeProof; + private ContextMenu contextMenu; + + @Getter @Setter + private Services services;// = DebuggerMain.FACADE.getService(); + + private BooleanProperty deactivateRefresh = new SimpleBooleanProperty(); + private ProofTreeListener proofTreeListener = new ProofTreeListener() { @Override public void proofExpanded(ProofTreeEvent proofTreeEvent) { @@ -97,11 +105,6 @@ public class ProofTree extends BorderPane { } }; - private ContextMenu contextMenu; - - @Getter @Setter - private Services services;// = DebuggerMain.FACADE.getService(); - public ProofTree() { Utils.createWithFXML(this); treeProof.setCellFactory(this::cellFactory); @@ -259,18 +262,26 @@ public class ProofTree extends BorderPane { } private void init() { + if (deactivateRefresh.get()) + return; + if (root.get() != null) { TreeItem item = populate("Proof", root.get()); treeProof.setRoot(item); } + treeProof.refresh(); } private TreeItem populate(String label, Node n) { - val treeNode = new TreeNode(label, n); - TreeItem ti = new TreeItem<>(treeNode); + + // abort the traversing iff we have reached a sentinel! + if (sentinels.contains(n)) { + return ti; + } + if (n.childrenCount() == 0) { ti.getChildren().add(new TreeItem<>(new TreeNode( n.isClosed() ? "CLOSED GOAL" : "OPEN GOAL", null))); @@ -386,6 +397,30 @@ public class ProofTree extends BorderPane { return proof; } + public ObservableSet getSentinels() { + return sentinels.get(); + } + + public void setSentinels(ObservableSet sentinels) { + this.sentinels.set(sentinels); + } + + public SetProperty sentinelsProperty() { + return sentinels; + } + + public boolean isDeactivateRefresh() { + return deactivateRefresh.get(); + } + + public void setDeactivateRefresh(boolean deactivateRefresh) { + this.deactivateRefresh.set(deactivateRefresh); + } + + public BooleanProperty deactivateRefreshProperty() { + return deactivateRefresh; + } + @AllArgsConstructor private static class TreeNode { String label;