From a4f363e1d695c48dbe42a750a81ea140cec6199a Mon Sep 17 00:00:00 2001 From: Lulu Luong Date: Thu, 27 Sep 2018 19:53:05 +0200 Subject: [PATCH] #54 --- .../controller/InteractiveModeController.java | 71 ++++++++++++++----- .../psdbg/examples/contraposition/script.kps | 4 ++ 2 files changed, 57 insertions(+), 18 deletions(-) diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java index 24af3477..4e6f7211 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java @@ -7,7 +7,6 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.SequentFormula; -import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.scripts.*; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; @@ -27,7 +26,6 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework; import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode; import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException; -import edu.kit.iti.formal.psdbg.interpreter.funchdl.MacroCommandHandler; import edu.kit.iti.formal.psdbg.interpreter.funchdl.ProofScriptCommandBuilder; import edu.kit.iti.formal.psdbg.parser.PrettyPrinter; import edu.kit.iti.formal.psdbg.parser.ast.*; @@ -69,8 +67,8 @@ public class InteractiveModeController { private PTreeNode nodeAtInteractionStart; //needed for Undo-Operation - private ArrayList savepointsstatement; - private ArrayList savepointslist; + private ArrayList laststatementlist; + private ArrayList lastnodeslist; private Proof currentProof; private Services keYServices; @@ -102,8 +100,8 @@ public class InteractiveModeController { gcs.setBody(v); casesStatement.getCases().add(gcs); }); - savepointslist = new ArrayList<>(); - savepointsstatement = new ArrayList<>(); + lastnodeslist = new ArrayList<>(); + laststatementlist = new ArrayList<>(); nodeAtInteractionStart = debuggerFramework.getStatePointer(); } @@ -113,13 +111,14 @@ public class InteractiveModeController { * Undo the application of the last rule */ public void undo(javafx.event.ActionEvent actionEvent) { - if (savepointslist.isEmpty()) { + if (lastnodeslist.isEmpty()) { Debug.log("Kein vorheriger Zustand."); return; } - val pruneNode = savepointslist.get(savepointslist.size() - 1); - savepointslist.remove(pruneNode); + val pruneNode = lastnodeslist.get(lastnodeslist.size() - 1); + lastnodeslist.remove(pruneNode); + ImmutableList goalsbeforePrune = currentProof.getSubtreeGoals(pruneNode); currentProof.pruneProof(pruneNode); @@ -130,19 +129,55 @@ public class InteractiveModeController { .filter(keyDataGoalNode -> goalsbeforePrune.contains(keyDataGoalNode.getData().getGoal())) .collect(Collectors.toList()); + if(prunedChildren.size() == 0) { + //TODO: add Utils.showInfoD + return; + } KeyData kd = prunedChildren.get(0).getData(); goals.removeAll(prunedChildren); + + + //Set selected goal after prune + GoalNode lastGoalNode = null; - for (Goal newGoalNode : goalsafterPrune) { - KeyData kdn = new KeyData(kd, newGoalNode.node()); + KeyData kdn; + if (lastnodeslist.size() == 0) { + kdn = new KeyData(kd, goalsafterPrune.get(0).node()); goals.add( - lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent().getParent(), kdn, kdn.getNode().isClosed())); + lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent(), kdn, kdn.getNode().isClosed())); + } else { + for (Goal newGoalNode : goalsafterPrune) { + kdn = new KeyData(kd, newGoalNode.node()); + goals.add( + lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent().getParent(), kdn, kdn.getNode().isClosed())); + } } model.setSelectedGoalNodeToShow(lastGoalNode); - val pruneStatement = savepointsstatement.get(savepointsstatement.size() - 1); - cases.forEach((k, v) -> v.remove(pruneStatement)); + + val pruneStatement = laststatementlist.get(laststatementlist.size() - 1); + laststatementlist.remove(laststatementlist.size() - 1); + + //TODO: buggy cuz allstatements of same node removed + + //remove statement from cases / script + Statements statements = (cases.get(pruneNode.parent()) == null)? cases.get(pruneNode) : cases.get(pruneNode.parent()); + int i = statements.size()-1; + + while(statements.get(i) != pruneStatement && i >= 0) { + statements.remove(i); + i--; + } + statements.remove(i); + + + /* + cases.forEach((k, v) -> { + v.remove(pruneStatement); + + }); + */ String c = getCasesAsString(); scriptArea.setText("" + @@ -294,8 +329,8 @@ public class InteractiveModeController { private void applyRuleHelper(CallStatement call, Goal g, Type t) throws ScriptCommandNotApplicableException { - savepointslist.add(g.node()); - savepointsstatement.add(call); + lastnodeslist.add(g.node()); + laststatementlist.add(call); ObservableList> goals = model.getGoals(); GoalNode expandedNode; @@ -429,8 +464,8 @@ public class InteractiveModeController { } /* private void applyRule(CallStatement call, Goal g) throws ScriptCommandNotApplicableException { - savepointslist.add(g.node()); - savepointsstatement.add(call); + lastnodeslist.add(g.node()); + laststatementlist.add(call); ObservableList> goals = model.getGoals(); GoalNode expandedNode; 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 475b4549..236855d1 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,3 +1,7 @@ +script empty(){ + +} + script full(){ impRight; impRight; -- GitLab