From 96e41055ef127e62b327bea4430eb579eb326d29 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Tue, 16 Jan 2018 10:01:06 +0100 Subject: [PATCH] Fixed first bug for step into proof tree, still not working properly yet --- .../interpreter/dbg/ContinueCommand.java | 10 ++-- .../interpreter/dbg/StepOverCommand.java | 5 ++ .../psdbg/gui/controller/DebuggerMain.java | 54 ++++++++++++------- .../formal/psdbg/gui/controls/ProofTree.java | 7 +++ .../psdbg/examples/contraposition/script.kps | 6 +++ 5 files changed, 59 insertions(+), 23 deletions(-) diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ContinueCommand.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ContinueCommand.java index 3e00877a..1bf400e9 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ContinueCommand.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ContinueCommand.java @@ -5,6 +5,11 @@ import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; import java.util.Arrays; import java.util.function.Supplier; +/** + * Continue Command if interpreter stopped at a breakpoint + * + * @param + */ public class ContinueCommand extends DebuggerCommand { @Override public void execute(DebuggerFramework dbg) { @@ -24,11 +29,6 @@ public class ContinueCommand extends DebuggerCommand { } Supplier currenDepth = () -> dbg.getStatePointer().getContext().length; - - //Blocker.BlockPredicate predicate = new Blocker.ParentInContext(ctx); - // Blocker.SmallerContext predicate = new Blocker.SmallerContext( - // currenDepth.get(), currenDepth); - //dbg.releaseUntil(predicate); dbg.release(); } else { diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepOverCommand.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepOverCommand.java index 10adba5b..dde68999 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepOverCommand.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepOverCommand.java @@ -5,6 +5,11 @@ import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; import java.util.Arrays; import java.util.function.Supplier; +/** + * Step Over Command, to step Over a proof command + * + * @param + */ public class StepOverCommand extends DebuggerCommand { @Override public void execute(DebuggerFramework dbg) { 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 95182adb..be699e5f 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 @@ -65,13 +65,12 @@ import java.io.PrintWriter; import java.net.URL; import java.nio.charset.Charset; import java.time.Duration; -import java.util.List; -import java.util.Optional; -import java.util.ResourceBundle; -import java.util.Set; +import java.util.*; import java.util.concurrent.*; import java.util.stream.Collectors; +import org.reactfx.util.Timer; + /** * Controller for the Debugger MainWindow * @@ -711,7 +710,11 @@ public class DebuggerMain implements Initializable { } - + /** + * Continue after the interpreter has reached a breakpoint + * + * @param event + */ @FXML public void continueAfterRun(ActionEvent event) { LOGGER.debug("DebuggerMain.continueAfterBreakpoint"); @@ -724,6 +727,10 @@ public class DebuggerMain implements Initializable { } } + /** + * Reload a problem from the beginning + * @param event + */ @FXML public void reloadProblem(ActionEvent event) { //abort current execution(); @@ -745,9 +752,6 @@ public class DebuggerMain implements Initializable { iModel.getGoals().clear(); iModel.setSelectedGoalNodeToShow(null); - // init(); - - //reload File try { FACADE.reload(lastLoaded); if (iModel.getGoals().size() > 0) { @@ -1111,24 +1115,37 @@ public class DebuggerMain implements Initializable { Proof proof = beforeNode.getData().getProof(); Node pnode = beforeNode.getData().getNode(); - System.out.println("pnode.serialNr() = " + pnode.serialNr()); - stateAfterStmt.forEach(keyDataGoalNode -> System.out.println("keyDataGoalNode.getData().getNode().serialNr() = " + keyDataGoalNode.getData().getNode().serialNr())); + // stateAfterStmt.forEach(keyDataGoalNode -> System.out.println("keyDataGoalNode.getData().getNode().serialNr() = " + keyDataGoalNode.getData().getNode().serialNr())); ptree.setProof(proof); ptree.setRoot(pnode); ptree.setDeactivateRefresh(true); + + //TODO Traversierung WICHTIG - //this is always 0 subtreegoals dies not return the subtree - //getSubtreegoals == 0 //traverse tree to closed goals -> set Sentinels //laeves of PNode wenn aftestmt leer //sonst nodes nodes afterstmt - Set sentinels = proof.getSubtreeGoals(pnode) - .stream() - .map(Goal::node) - .collect(Collectors.toSet()); - System.out.println("Sentinels: " + sentinels.isEmpty()); - ptree.getSentinels().addAll(sentinels); + + if (stateAfterStmt.size() > 0) { + Set sentinels = proof.getSubtreeGoals(pnode) + .stream() + .map(Goal::node) + .collect(Collectors.toSet()); + ptree.getSentinels().addAll(sentinels); + } else { + Set sentinels = new HashSet<>(); + Iterator nodeIterator = beforeNode.getData().getNode().leavesIterator(); + while (nodeIterator.hasNext()) { + Node next = nodeIterator.next(); + + sentinels.add(next.parent()); + } + ptree.getSentinels().addAll(sentinels); + //traverseProofTreeAndAddSentinelsToLeaves(); + } + + ptree.expandRootToLeaves(); //TODO set coloring of starting and end node DockNode node = new DockNode(ptree, "Proof Tree for Step Into: " + @@ -1138,6 +1155,7 @@ public class DebuggerMain implements Initializable { node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea())); } } + //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 3a9a33eb..d7d6d9f4 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 @@ -160,6 +160,13 @@ public class ProofTree extends BorderPane { } public void expandRootToLeaves() { + if (getTreeProof().getRoot() == null) { + if (root.get() != null) { + TreeItem item = new TreeItem<>(new TreeNode(root.get().serialNr() + ": " + toString(root.get()), root.get())); + treeProof.setRoot(item); + } + + } expandRootToLeaves(getTreeProof().getRoot()); } diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps index a1001751..b96c558d 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps @@ -1,5 +1,11 @@ // Please select one of the following scripts. // + +script test1234(){ + impRight; + auto; +} + script test23(){ impRight; x:term := find(match `?rt ==>`); -- 2.26.2