Commit 2978eada authored by Sarah Grebing's avatar Sarah Grebing

StepInverseInto should work now

parent 5f18506f
Pipeline #16979 passed with stages
in 9 minutes and 1 second
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import lombok.val;
public class StepIntoReverseCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) throws DebuggerException {
val statePointer = dbg.getCurrentStatePointer();
PTreeNode<T> stepBack = statePointer.getStepInvInto() != null ?
statePointer.getStepInvInto() :
statePointer.getStepInvOver();
PTreeNode<T> statePointer = dbg.getStatePointer();
assert statePointer != null;
if (statePointer.getStepInvInto() != null) {
dbg.setStatePointer(statePointer.getStepInvInto());
} else {
if (statePointer.getStepInvOver() != null) {
PTreeNode<T> statementBefore = statePointer.getStepInvOver();
dbg.setStatePointer(statementBefore);
}
}
if (stepBack == null) {
info("There is no previous state to the current one.");
}
dbg.setStatePointer(stepBack);
}
}
......@@ -15,7 +15,6 @@ import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.speclang.Contract;
import edu.kit.iti.formal.psdbg.ShortCommandPrinter;
import edu.kit.iti.formal.psdbg.StepIntoCommand;
import edu.kit.iti.formal.psdbg.examples.Examples;
import edu.kit.iti.formal.psdbg.fmt.DefaultFormatter;
import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger;
......@@ -71,6 +70,8 @@ import java.util.*;
import java.util.concurrent.*;
import java.util.stream.Collectors;
import org.reactfx.util.Timer;
/**
* Controller for the Debugger MainWindow
*
......@@ -907,7 +908,7 @@ public class DebuggerMain implements Initializable {
* @param actionEvent
*/
public void stepInto(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMain.stepOver");
LOGGER.debug("DebuggerMain.stepInto");
try {
if (model.getDebuggerFramework().getStatePointer().isAtomic()) {
model.getDebuggerFramework().getStatePointerListener()
......@@ -931,6 +932,7 @@ public class DebuggerMain implements Initializable {
*
* @param actionEvent
*/
@Deprecated
public void stepBack(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMain.stepBack");
try {
......@@ -953,13 +955,26 @@ public class DebuggerMain implements Initializable {
public void stepIntoReverse(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMain.stepOverReverse");
LOGGER.debug("DebuggerMain.stepIntoReverser");
try {
if (model.getDebuggerFramework().getStatePointer().isAtomic()) {
model.getDebuggerFramework().getStatePointerListener()
.add(new StepIntoReverseHandler(model.getStatePointer()));
}
model.getDebuggerFramework().execute(new StepIntoReverseCommand<>());
} catch (DebuggerException e) {
Utils.showExceptionDialog("", "", "", e);
LOGGER.error(e);
}
/* LOGGER.debug("DebuggerMain.stepOverReverse");
try {
model.getDebuggerFramework().execute(new StepIntoReverseCommand<>());
} catch (DebuggerException e) {
Utils.showExceptionDialog("", "", "", e);
LOGGER.error(e);
}*/
}
public void stopDebugMode(ActionEvent actionEvent) {
......@@ -1197,6 +1212,64 @@ public class DebuggerMain implements Initializable {
node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea()));
}
}
@RequiredArgsConstructor
private class StepIntoReverseHandler implements java.util.function.Consumer<PTreeNode<KeyData>> {
private final PTreeNode<KeyData> original;
@Override
public void accept(PTreeNode<KeyData> keyDataPTreeNode) {
Platform.runLater(this::acceptUI);
}
public void acceptUI() {
model.getDebuggerFramework().getStatePointerListener().remove(this);
PTreeNode<KeyData> stepInvOver = model.getDebuggerFramework().getStatePointer();
GoalNode<KeyData> beforeNode = stepInvOver.getStateBeforeStmt().getSelectedGoalNode();
List<GoalNode<KeyData>> stateAfterStmt = stepInvOver.getStateAfterStmt().getGoals();
ProofTree ptree = new ProofTree();
Proof proof = beforeNode.getData().getProof();
Node pnode = beforeNode.getData().getNode();
// stateAfterStmt.forEach(keyDataGoalNode -> System.out.println("keyDataGoalNode.getData().getNode().serialNr() = " + keyDataGoalNode.getData().getNode().serialNr()));
ptree.setProof(proof);
ptree.setRoot(pnode);
ptree.addNodeColor(pnode, "blueviolet");
ptree.setDeactivateRefresh(true);
if (stateAfterStmt.size() > 0) {
Set<Node> sentinels = proof.getSubtreeGoals(pnode)
.stream()
.map(Goal::node)
.collect(Collectors.toSet());
ptree.getSentinels().addAll(sentinels);
sentinels.forEach(node -> ptree.addNodeColor(node, "blueviolet"));
} else {
Set<Node> sentinels = new HashSet<>();
Iterator<Node> nodeIterator = beforeNode.getData().getNode().leavesIterator();
while (nodeIterator.hasNext()) {
Node next = nodeIterator.next();
sentinels.add(next);
}
ptree.getSentinels().addAll(sentinels);
sentinels.forEach(node -> ptree.addNodeColor(node, "blueviolet"));
//traverseProofTreeAndAddSentinelsToLeaves();
}
ptree.expandRootToSentinels();
DockNode node = new DockNode(ptree, "Proof Tree for Step Inverse Into: " +
original.getStatement().accept(new ShortCommandPrinter())
);
node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea()));
}
}
//endregion
}
//deprecated
......
......@@ -154,7 +154,7 @@ public class SequentView extends CodeArea {
insertText(0, backend.getString());
if (node.get().isClosed()) {
this.setBorder(new Border(new BorderStroke(Color.GREEN, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT)));
this.getStyleClass().add("closed-sequent-view");
// this.getStyleClass().add("closed-sequent-view");
} else {
this.setBorder(new Border(new BorderStroke(Color.BLACK, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT)));
this.getStyleClass().remove("closed-sequent-view");
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment