Savepoint: prune + keypersistencefacade not yet added (TODO)

minor bug fixes

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java

@@ -14,7 +14,7 @@ public class ASTDiff extends DefaultASTVisitor<ASTNode> {
         newScript.setSignature(proofScript.getSignature());
 
         other = ((ProofScript) other).getBody();
-        newScript.setBody(visit(newScript.getBody()));
+        newScript.setBody(visit(proofScript.getBody()));
         return newScript;
     }
 
@@ -61,12 +61,13 @@ public class ASTDiff extends DefaultASTVisitor<ASTNode> {
 
         int i = 0;
         for (; i < statements.size(); i++) {
-            if (statements.get(i).eq(other.get(i))) {
-                break;
+            if (!statements.get(i).isSame(other.get(i))) {
+                System.out.println("Alter Script wurde verändert");
+                return null;
             }
         }
 
-        for (int j = i; j < other.size(); j++) {
+        for (; i < other.size(); i++) {
             s.add(other.get(i));
         }
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java

@@ -167,6 +167,11 @@ public abstract class ASTNode<T extends ParserRuleContext>
         return Objects.hash(getRuleContext());
     }
 
+    //TODO: param + class
+    public boolean isSame(ASTNode other) {
+        return this.getNodeName().equals(other.getNodeName());
+    }
+
     public int getSyntaxWidth() {
         if (ruleContext != null) {
             return ruleContext.stop.getStopIndex()

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

@@ -225,9 +225,10 @@ public class InterpreterBuilder {
 
     public InterpreterBuilder setProblemPath(File path){
         Map<String, CommandHandler<KeyData>> builtinsnew = this.bich.getBuiltins();
-        SaveCommand sc = new SaveCommand(path);
-        builtinsnew.put(SaveCommand.SAVE_COMMAND_NAME, sc);
+
+        builtinsnew.put(SaveCommand.SAVE_COMMAND_NAME, new SaveCommand(path));
         this.bich.setBuiltins(builtinsnew);
+
         return this;
 
     }

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

@@ -15,8 +15,10 @@ import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
 import javax.annotation.Nullable;
+import javax.xml.bind.JAXBException;
 import java.io.File;
 import java.io.IOException;
+import java.io.StringWriter;
 import java.util.Optional;
 import java.util.concurrent.CyclicBarrier;
 import java.util.concurrent.Semaphore;
@@ -74,8 +76,10 @@ public class SaveCommand implements CommandHandler<KeyData> {
 
             if(execute.get())
                 interpreter.getSelectedNode().getData().getProof().saveToFile(newFile);
-            //KeyPersistentFacade.write();
-            //TODO Call to key persistend facade
+                //TODO: KeyPersistentFacade.write(interpreter.getCurrentState(), new StringWriter());
+
+
+
         } catch (IOException e) {
             e.printStackTrace();
         } catch (InterruptedException e) {

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

@@ -2,6 +2,7 @@ package edu.kit.iti.formal.psdbg.gui.controller;
 
 import alice.tuprolog.InvalidLibraryException;
 import alice.tuprolog.InvalidTheoryException;
+import antlr.collections.AST;
 import com.google.common.eventbus.Subscribe;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
@@ -25,6 +26,7 @@ import edu.kit.iti.formal.psdbg.gui.graph.GraphView;
 import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel;
 import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
 import edu.kit.iti.formal.psdbg.gui.model.InterpreterThreadState;
+import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
 import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
 import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
 import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
@@ -33,7 +35,12 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
 import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
+import edu.kit.iti.formal.psdbg.parser.ASTDiff;
+import edu.kit.iti.formal.psdbg.parser.Facade;
+import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
+import edu.kit.iti.formal.psdbg.parser.ast.CaseStatement;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
+import edu.kit.iti.formal.psdbg.storage.KeyPersistentFacade;
 import javafx.application.Platform;
 import javafx.beans.InvalidationListener;
 import javafx.beans.binding.BooleanBinding;
@@ -54,6 +61,7 @@ import javafx.stage.FileChooser;
 import javafx.stage.Modality;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
+import lombok.val;
 import org.apache.commons.io.FileUtils;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
@@ -66,11 +74,11 @@ import org.reactfx.util.Timer;
 
 import javax.annotation.Nullable;
 import javax.swing.*;
+import java.awt.event.WindowAdapter;
+import java.awt.event.WindowEvent;
+import java.awt.event.WindowListener;
 import java.awt.im.InputContext;
-import java.io.File;
-import java.io.FileWriter;
-import java.io.IOException;
-import java.io.PrintWriter;
+import java.io.*;
 import java.net.URL;
 import java.nio.charset.Charset;
 import java.time.Duration;
@@ -829,6 +837,9 @@ public class DebuggerMain implements Initializable {
     @FXML
     public void executeDiff() {
         //save old PT
+
+
+
         // Calculate top difference between current and last executed script
         // Find last state of common ASTNode
         // Use this state to build new interpreter in proof tree controller.
@@ -837,6 +848,36 @@ public class DebuggerMain implements Initializable {
 
     }
 
+
+
+
+    @Deprecated
+    public  void incremental() {
+        ProofScript oldScript = null; //used to be global var, that was set in selectSavepoint()
+
+        if (oldScript == null) {
+            return;
+        }
+        ProofScript newScript = scriptController.getMainScript().byName(scriptController.getCombinedAST()).get();
+
+        ASTDiff astDiff = new ASTDiff();
+        ProofScript scriptdiff = astDiff.diff(oldScript, newScript);
+        ASTNode pruneAstNode = scriptdiff.getBody().get(0);
+
+        Set<PTreeNode<KeyData>> ptnodes = model.getDebuggerFramework().getPtreeManager().getNodes();
+        Iterator iterator = ptnodes.iterator();
+        while (iterator.hasNext()) {
+            PTreeNode<KeyData> ptn = (PTreeNode<KeyData>) iterator.next();
+            if(ptn.getStatement().eq(pruneAstNode)) {
+                getFacade().getProof().pruneProof(ptn.getStateBeforeStmt().getSelectedGoalNode().getData().getNode());
+                break;
+            }
+        }
+
+
+        scriptController.setMainScript(oldScript);
+    }
+
     /**
      * Continue after the interpreter has reached a breakpoint
      *
@@ -928,12 +969,12 @@ public class DebuggerMain implements Initializable {
 
     @FXML
     public void saveAsScript() throws IOException {
-        File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps");
-        if (f != null) {
-           /* if(!f.exists()){
-                f.createNewFile();
-            }*/
-            saveScript(f);
+        FileChooser fc = new FileChooser();
+        File file = fc.showSaveDialog(btnInteractiveMode.getScene().getWindow());
+        if (file != null) {
+                saveScript(file);
+        } else {
+            Utils.showInfoDialog("","Select a destination", "No valid path has been selected.");
         }
     }
 
@@ -1146,16 +1187,76 @@ public class DebuggerMain implements Initializable {
 
     @FXML
     public void selectSavepoint(ActionEvent actionEvent) {
-        if (cboSavePoints.getValue() != null) {
+        SavePoint selected = cboSavePoints.getValue();
+
+        if (selected == null) {
+            Utils.showInfoDialog("Select Savepoint", "Select Savepoint", "There is no selected Savepoint. Select a Savepoint first.");
+            return;
+        }
+
+        int currentpos = model.getDebuggerFramework().getCurrentStatePointer().getStatement().getStartPosition().getLineNumber();
+
+        //check intpreter finishes with which script
+        if (model.getInterpreterState().equals(InterpreterThreadState.FINISHED)
+                || selected.getLineNumber() <= currentpos && currentpos > 0) {
+            Iterator<PTreeNode<KeyData>> iterator = model.getDebuggerFramework().getPtreeManager().getNodes().iterator();
+            PTreeNode<KeyData> pTreeNodeOfSave;
+            while (iterator.hasNext()) {
+                pTreeNodeOfSave = iterator.next();
+
+                if (pTreeNodeOfSave.getStatement().getStartPosition().getLineNumber() == selected.getLineNumber()) {
+                    FACADE.getProof().pruneProof(pTreeNodeOfSave.getStateBeforeStmt().getSelectedGoalNode().getData().getNode());
+                    inspectionViewsController.getActiveInspectionViewTab().activate(pTreeNodeOfSave, pTreeNodeOfSave.getStateAfterStmt());
+                    break;
+                }
+            }
+
+            //TODO: refresh GUI (Context + Script)
+            //State<KeyData> proofstate = KeyPersistentFacade.read(FACADE.getEnvironment(), FACADE.getProof(), new StringReader());
+
+        } else {
+
+
+        /*
+
+
+        // check if selected savepoint has been executed already -> prune to that savepoint
+
+
+        val statePointer = model.getDebuggerFramework().getCurrentStatePointer();
+        int currentpos = statePointer.getStatement().getStartPosition().getLineNumber();
+        if (model.getInterpreterState().equals(InterpreterThreadState.FINISHED)
+                || selected.getLineNumber() <= currentpos && currentpos > 0) {
+
+            System.out.println("Pruning to Savepoint.");
+
+                int line_statePointer = statePointer.getStatement().getStartPosition().getLineNumber();
+                int nrOfStepbacks = line_statePointer - selected.getLineNumber();
+
+                PTreeNode<KeyData> pTreeNodeOfSave = statePointer.getStepInvOver();
+                for (int i = 1; i <= nrOfStepbacks; i++) {
+                    pTreeNodeOfSave = statePointer.getStepInvOver();
+                }
+
+
+
+
+            model.getDebuggerFramework().getPtreeManager();
+            //TODO: find Node to prune
+            // FACADE.getProof().pruneProof(save);
+
+
+    }
+
+    */
+            //Hard Loading of Savepoint
             stopDebugMode(actionEvent);
-            SavePoint selected = cboSavePoints.getValue();
 
             try {
                 abortExecution();
             } catch (Exception e) {
                 e.printStackTrace();
             }
-
             /**
              * reload with selected savepoint
              */
@@ -1179,9 +1280,6 @@ public class DebuggerMain implements Initializable {
                     statusBar.publishMessage("Reloaded Sucessfully");
                 }
 
-                //TODO: check again
-                scriptController.getMainScript().getScriptArea().setSavepointMarker(selected.getLineNumber());
-                scriptController.getMainScript().getScriptArea().getCodeArea().setStyleClass(selected.getStartOffset(), selected.getEndOffset() + 1, "problem");
 
             } catch (ProofInputException | ProblemLoaderException e) {
                 LOGGER.error(e);
@@ -1190,13 +1288,18 @@ public class DebuggerMain implements Initializable {
                         e
                 );
             }
-
-            // executeScriptFromSavePoint(interpreterBuilder, selected);
         }
 
+        MainScriptIdentifier msi = scriptController.getMainScript();
+        msi.getScriptArea().setSavepointMarker(selected.getLineNumber());
+        //TODO underline ast
+
+        msi.getScriptArea().getCodeArea().setStyleClass(selected.getStartOffset(), selected.getEndOffset() + 1, "problem");
+        scriptExecutionController.executeScriptFromSavePoint(interpreterBuilder, selected);
     }
 
 
+
     @FXML
     public void showWelcomeDock(ActionEvent actionEvent) {
         if (!welcomePaneDock.isDocked() && !welcomePaneDock.isFloating()) {
@@ -1281,7 +1384,7 @@ public class DebuggerMain implements Initializable {
 
     public void openInKey(@Nullable ActionEvent event) {
         if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) {
-            Alert alert = new Alert(Alert.AlertType.INFORMATION, "No proof is loaded yet. If laoding a proof was invoked, proof state loading may take a while.", ButtonType.OK);
+            Alert alert = new Alert(Alert.AlertType.INFORMATION, "No proof is loaded yet. If loading a proof was invoked, proof state loading may take a while.", ButtonType.OK);
             alert.show();
             return;
         }
@@ -1293,10 +1396,14 @@ public class DebuggerMain implements Initializable {
             //keyWindow.getProofList().getModel().addProof();
             keyWindow.makePrettyView();
             keyWindow.setVisible(true);
+
+
         });
+
     }
 
 
+
     public class ContractLoaderService extends Service<List<Contract>> {
         @Override
         protected void succeeded() {

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

@@ -110,7 +110,7 @@ public class InteractiveModeController {
      */
     public void undo(javafx.event.ActionEvent actionEvent) {
         if (savepointslist.isEmpty()) {
-            Debug.log("Kein vorheriger Zustand."); //TODO: events fire
+            Debug.log("Kein vorheriger Zustand.");
             return;
         }
 

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

@@ -8,7 +8,9 @@ import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
 import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
 import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint;
+import edu.kit.iti.formal.psdbg.parser.ASTDiff;
 import edu.kit.iti.formal.psdbg.parser.Facade;
+import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
 import edu.kit.iti.formal.psdbg.parser.ast.Statements;
 import javafx.scene.control.Alert;
@@ -160,7 +162,10 @@ public class ScriptExecutionController {
     }
 
 
-    //TODO: calc diff
+    private ASTNode calculateDiff (ASTDiff dff) {
+
+        return null;
+    }
 
 
 }

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

@@ -458,9 +458,7 @@ public class ScriptArea extends BorderPane {
     public void setAlertMarker(int lineNumber) {
         gutter.getLineAnnotation(lineNumber - 1).setAlert(true);
     }
-    private void underline(int linenumber) {
 
-    }
 
 
     private boolean hasExecutionMarker() {

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

@@ -251,6 +251,15 @@
                                   </tooltip>
                               </Button>-->
 
+                        <Button  disable="false">
+                            <graphic>
+                                <MaterialDesignIconView glyphName="KEYBOARD_BACKSPACE" size="24.0"/>
+                            </graphic>
+                            <tooltip>
+                                <Tooltip text="Prune to savepoint"/>
+                            </tooltip>
+                        </Button>
+
                         <Button onAction="#continueAfterRun" disable="${controller.executeNotPossible}">
                             <graphic>
                                 <MaterialDesignIconView glyphName="PLAY_CIRCLE_OUTLINE" size="24.0"/>