Bugfix that removed/expanded nodes were still in state due to selectedGoalNode field

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java

@@ -2,7 +2,6 @@ package edu.kit.iti.formal.psdbg.interpreter;
 
 import com.google.common.collect.BiMap;
 import com.google.common.collect.ImmutableBiMap;
-import de.uka.ilkd.key.api.ScriptApi;
 import de.uka.ilkd.key.api.VariableAssignments;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
@@ -66,7 +65,7 @@ public class KeyInterpreter extends Interpreter<KeyData> {
             }
         }
         //prune proof
-        logger.debug("The closes script " + (allClosed ? "closed the proof.\n" : "did not close the proof.\n") + "Rolling Back proof now.");
+        LOGGER.debug("The closes script " + (allClosed ? "closed the proof.\n" : "did not close the proof.\n") + "Rolling Back proof now.");
         Proof currentKeYproof = selectedGoalNode.getData().getProof();
         ImmutableList<Goal> subtreeGoals = currentKeYproof.getSubtreeGoals(((KeyData) selectedGoalNode.getData()).getNode());
         currentKeYproof.pruneProof(selectedGoalCopy.getData().getNode());

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/MacroCommandHandler.java

@@ -15,6 +15,8 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
 import org.key_project.util.collection.ImmutableList;
 
 import java.util.Collection;
@@ -28,6 +30,8 @@ import java.util.Map;
  */
 @RequiredArgsConstructor
 public class MacroCommandHandler implements CommandHandler<KeyData> {
+    protected static Logger LOGGER = LogManager.getLogger(MacroCommandHandler.class);
+
     @Getter
     private final Map<String, ProofMacro> macros;
 
@@ -57,6 +61,7 @@ public class MacroCommandHandler implements CommandHandler<KeyData> {
 
         State<KeyData> state = interpreter.getCurrentState();
         GoalNode<KeyData> expandedNode = state.getSelectedGoalNode();
+        assert state.getGoals().contains(expandedNode);
 
 
         try {
@@ -67,6 +72,8 @@ public class MacroCommandHandler implements CommandHandler<KeyData> {
                 ImmutableList<Goal> ngoals = expandedNode.getData().getProof().getSubtreeGoals(expandedNode.getData().getNode());
 
                 state.getGoals().remove(expandedNode);
+                state.setSelectedGoalNode(null);
+
                 if (ngoals.isEmpty()) {
                     Node start = expandedNode.getData().getNode();
                     //start.leavesIterator()
@@ -74,7 +81,7 @@ public class MacroCommandHandler implements CommandHandler<KeyData> {
                     Iterator<Node> nodeIterator = start.leavesIterator();
                     while (nodeIterator.hasNext()) {
                         Node n = nodeIterator.next();
-                        System.out.println(n.isClosed());
+                        LOGGER.error(n.isClosed());
                     }
 
                 } else {
@@ -83,6 +90,9 @@ public class MacroCommandHandler implements CommandHandler<KeyData> {
                         KeyData kdn = new KeyData(expandedNode.getData(), g.node());
                         state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.isClosedNode()));
                     }
+                    assert !state.getGoals().contains(expandedNode);
+
+
                 }
             }
         } catch (InterruptedException e) {

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java

@@ -15,6 +15,8 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
 import org.key_project.util.collection.ImmutableList;
 
 import java.util.Collection;
@@ -30,6 +32,8 @@ import java.util.Map;
  */
 @RequiredArgsConstructor
 public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
+    protected static Logger LOGGER = LogManager.getLogger(ProofScriptCommandBuilder.class);
+
     @Getter
     private final Map<String, ProofScriptCommand> commands;
 
@@ -65,7 +69,10 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
             AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
             c.execute(uiControl, cc, estate);
             //what happens if this is empty -> meaning proof is closed
-
+            state.getGoals().remove(expandedNode);
+            if (state.getSelectedGoalNode().equals(expandedNode)) {
+                state.setSelectedGoalNode(null);
+            }
             ImmutableList<Goal> ngoals = kd.getProof().getSubtreeGoals(kd.getNode());
             if (ngoals.isEmpty()) {
                 Node start = expandedNode.getData().getNode();
@@ -74,7 +81,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
                 Iterator<Node> nodeIterator = start.leavesIterator();
                 while (nodeIterator.hasNext()) {
                     Node n = nodeIterator.next();
-                    System.out.println(n.isClosed());
+                    LOGGER.error(n.isClosed());
                 }
 
             } else {
@@ -83,7 +90,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
                     state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.isClosedNode()));
                 }
             }
-            state.getGoals().remove(expandedNode);
+
 
         } catch (Exception e) {
             throw new RuntimeException(e);

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java

@@ -68,6 +68,9 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
 
             ImmutableList<Goal> ngoals = kd.getProof().getSubtreeGoals(kd.getNode());
             state.getGoals().remove(expandedNode);
+            if (state.getSelectedGoalNode().equals(expandedNode)) {
+                state.setSelectedGoalNode(null);
+            }
             for (Goal g : ngoals) {
                 KeyData kdn = new KeyData(kd, g.node());
                 state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java

@@ -221,6 +221,9 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
             }
 
             State<T> stateAfterCase = popState(); //remove state from stack
+            if (stateAfterCase.getSelectedGoalNode() != null) {
+                assert stateAfterCase.getGoals().contains(stateAfterCase.getSelectedGoalNode());
+            }
 
             if (result && stateAfterCase.getGoals() != null) {
                 resultingGoals.addAll(stateAfterCase.getGoals());
@@ -273,6 +276,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         Expression matchExpression = guardedCaseStatement.getGuard();
         State<T> currentStateToMatch = peekState();
         GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
+        assert currentStateToMatch.getGoals().contains(selectedGoal);
         VariableAssignment va = evaluateMatchInGoal(matchExpression, selectedGoal);
 
         try {
@@ -510,6 +514,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         enterScope(caseStmts);
         goalNode.enterScope(va);
         State<T> s = newState(goalNode);
+        assert s.getGoals().contains(s.getSelectedGoalNode());
         caseStmts.accept(this);
         //popState(s); //This may be incorrect-> Bug? -> Cases Statement needs to pop, as goals need to be collected
         exitScope(caseStmts);
@@ -644,7 +649,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
     //region State Handling
     public GoalNode<T> getSelectedNode() {
         try {
-            return stateStack.peek().getSelectedGoalNode();
+            GoalNode<T> selectedGoalNode = stateStack.peek().getSelectedGoalNode();
+            if (selectedGoalNode != null) {
+                assert stateStack.peek().getGoals().contains(selectedGoalNode);
+            }
+            return selectedGoalNode;
         } catch (IllegalStateException e) {
             if (scrictSelectedGoalMode)
                 throw e;

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/State.java

@@ -79,10 +79,6 @@ public class State<T> {
         return new State<T>(copiedGoals, refToSelGoal);
     }
 
-    public void setSelectedGoalNode(GoalNode<T> gn) {
-        this.selectedGoalNode = gn;
-    }
-
     public GoalNode<T> getSelectedGoalNode() {
      /*   if (selectedGoalNode == null) {
             throw new IllegalStateException("no selected node");
@@ -96,9 +92,17 @@ public class State<T> {
         if (getGoals().size() == 1) {
             selectedGoalNode = getGoals().get(0);
         }
+
         return selectedGoalNode;
     }
 
+    public void setSelectedGoalNode(GoalNode<T> gn) {
+        if (gn != null) {
+            assert goals.contains(gn);
+        }
+        this.selectedGoalNode = gn;
+    }
+
     public String toString() {
         if (selectedGoalNode == null) {
             return "No Goal selected";

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java

@@ -103,7 +103,7 @@ public class ProofScriptDebugger extends Application {
             logger.info("KeY: " + KeYConstants.COPYRIGHT);
             logger.info("KeY Version: " + KeYConstants.VERSION);
             logger.info("KeY Internal: " + KeYConstants.INTERNAL_VERSION);
-            //logger.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
+            //LOGGER.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
 
 
         } catch (Exception e) {