bugfix-Idea

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

@@ -6,6 +6,7 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.macros.ProofMacro;
 import de.uka.ilkd.key.macros.ProofMacroFinishedInfo;
 import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
 import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
@@ -18,6 +19,7 @@ import org.key_project.util.collection.ImmutableList;
 
 import java.util.Collection;
 import java.util.HashMap;
+import java.util.Iterator;
 import java.util.Map;
 
 /**
@@ -65,9 +67,22 @@ public class MacroCommandHandler implements CommandHandler<KeyData> {
                 ImmutableList<Goal> ngoals = expandedNode.getData().getProof().getSubtreeGoals(expandedNode.getData().getNode());
 
                 state.getGoals().remove(expandedNode);
-                for (Goal g : ngoals) {
-                    KeyData kdn = new KeyData(expandedNode.getData(), g.node());
-                    state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.isClosedNode()));
+                if (ngoals.isEmpty()) {
+                    Node start = expandedNode.getData().getNode();
+                    //start.leavesIterator()
+//                Goal s = kd.getProof().getGoal(start);
+                    Iterator<Node> nodeIterator = start.leavesIterator();
+                    while (nodeIterator.hasNext()) {
+                        Node n = nodeIterator.next();
+                        System.out.println(n.isClosed());
+                    }
+
+                } else {
+
+                    for (Goal g : ngoals) {
+                        KeyData kdn = new KeyData(expandedNode.getData(), g.node());
+                        state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.isClosedNode()));
+                    }
                 }
             }
         } catch (InterruptedException e) {

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

@@ -6,6 +6,7 @@ import de.uka.ilkd.key.macros.scripts.EngineState;
 import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
 import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument;
 import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
 import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
@@ -18,6 +19,7 @@ import org.key_project.util.collection.ImmutableList;
 
 import java.util.Collection;
 import java.util.HashMap;
+import java.util.Iterator;
 import java.util.Map;
 
 /**
@@ -62,13 +64,27 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
             Object cc = c.evaluateArguments(estate, map); //exception?
             AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
             c.execute(uiControl, cc, estate);
+            //what happens if this is empty -> meaning proof is closed
 
             ImmutableList<Goal> ngoals = kd.getProof().getSubtreeGoals(kd.getNode());
-            state.getGoals().remove(expandedNode);
-            for (Goal g : ngoals) {
-                KeyData kdn = new KeyData(kd, g.node());
-                state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.isClosedNode()));
+            if (ngoals.isEmpty()) {
+                Node start = expandedNode.getData().getNode();
+                //start.leavesIterator()
+//                Goal s = kd.getProof().getGoal(start);
+                Iterator<Node> nodeIterator = start.leavesIterator();
+                while (nodeIterator.hasNext()) {
+                    Node n = nodeIterator.next();
+                    System.out.println(n.isClosed());
+                }
+
+            } else {
+                for (Goal g : ngoals) {
+                    KeyData kdn = new KeyData(kd, g.node());
+                    state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.isClosedNode()));
+                }
             }
+            state.getGoals().remove(expandedNode);
+
         } catch (Exception e) {
             throw new RuntimeException(e);
         }

rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/ExecuteTest.java

@@ -75,5 +75,18 @@ public class ExecuteTest {
         Assert.assertEquals("Antecedent should contain the cut formula", s, goal0_data.getNode().sequent().antecedent().get(0).formula());
 
 
+    }
+
+    @Test
+    public void testLiarsville() throws IOException, ParseException, ParserException {
+        Execute execute = create(
+                getFile(getClass(), "testCasesKeYFiles/liarsville.key"),
+                "-s", getFile(getClass(), "testCasesKeYFiles/liarsvilleAuto.kps"));
+        Interpreter<KeyData> i = execute.run();
+        State<KeyData> currentState = i.getCurrentState();
+        System.out.println(currentState);
+        //This revealed a bug in the interpreter for body of a case
+
+
     }
 }
\ No newline at end of file

rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/testCasesKeYFiles/liarsville.key

+// This file is part of KeY - Integrated Deductive Software Design
+//
+// Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany
+//                         Universitaet Koblenz-Landau, Germany
+//                         Chalmers University of Technology, Sweden
+// Copyright (C) 2011-2013 Karlsruhe Institute of Technology, Germany
+//                         Technical University Darmstadt, Germany
+//                         Chalmers University of Technology, Sweden
+//
+// The KeY system is protected by the GNU General
+// Public License. See LICENSE.TXT for details.
+//
+
+
+
+\predicates {
+        Mr_Applebee_lies;
+        Mrs_Beatle_lies;
+        Ms_Casey_lies;
+        Dr_Doodle_lies;
+        Mr_Eastwood_lies;
+}
+
+\problem {
+(
+        (Mr_Applebee_lies & Mrs_Beatle_lies & Ms_Casey_lies & Dr_Doodle_lies & !Mr_Eastwood_lies)
+|
+        (Mr_Applebee_lies & Mrs_Beatle_lies & Ms_Casey_lies & !Dr_Doodle_lies & Mr_Eastwood_lies)
+|
+        (Mr_Applebee_lies & Mrs_Beatle_lies & !Ms_Casey_lies & Dr_Doodle_lies & Mr_Eastwood_lies)
+|
+        (Mr_Applebee_lies & !Mrs_Beatle_lies & Ms_Casey_lies & Dr_Doodle_lies & Mr_Eastwood_lies)
+|
+        (!Mr_Applebee_lies & Mrs_Beatle_lies & Ms_Casey_lies & Dr_Doodle_lies & Mr_Eastwood_lies)
+)
+->
+        (Mr_Applebee_lies -> Mr_Applebee_lies)
+&
+        (Mrs_Beatle_lies -> Dr_Doodle_lies)
+&
+        (Ms_Casey_lies -> !Ms_Casey_lies)
+&
+        (Dr_Doodle_lies -> Mrs_Beatle_lies)
+&
+        (Mr_Eastwood_lies -> Mr_Eastwood_lies)
+->
+        !Ms_Casey_lies
+}

rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/testCasesKeYFiles/liarsvilleAuto.kps

+script test(){
+auto;
+}
\ No newline at end of file

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

@@ -27,6 +27,7 @@ import javafx.concurrent.Task;
 import javafx.event.ActionEvent;
 import javafx.fxml.FXML;
 import javafx.fxml.Initializable;
+import javafx.scene.control.Button;
 import javafx.scene.control.Menu;
 import javafx.scene.control.MenuItem;
 import javafx.scene.control.ProgressBar;
@@ -734,6 +735,8 @@ public class DebuggerMain implements Initializable {
 
     public void stopDebugMode(ActionEvent actionEvent) {
         scriptController.getDebugPositionHighlighter().remove();
+        Button stop = (Button) actionEvent.getSource();
+        stop.setText("Reload");
         //linenumberMainscript from model?
         //scriptController.getActiveScriptAreaTab().getScriptArea().removeHighlightStmt(lineNumberMainScript);
         //inspectionViewsController.getInspectionViewTab.clear();

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml

@@ -157,14 +157,14 @@
                             </tooltip>
                         </Button>
 
-                        <!--<Button onAction="#stopDebugMode" disable="${! controller.debugMode}">
+                        <Button onAction="#stopDebugMode" disable="${! controller.debugMode}">
                             <graphic>
                                 <MaterialDesignIconView glyphName="STOP" size="24.0"/>
                             </graphic>
                             <tooltip>
                                 <Tooltip text="Stop"/>
                             </tooltip>
-                        </Button>-->
+                        </Button>
                     </items>
                 </ToolBar>
             </children>