Merge branch 'LuluSequentMatcher2' into 'master'

Lulu sequent matcher2

See merge request !6

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

@@ -52,6 +52,7 @@ public class ProofScriptDebugger extends Application {
                     getClass().getResource("debugger-ui.css").toExternalForm(),
                     DockNode.class.getResource("default.css").toExternalForm()
             );
+            System.out.println(getClass().getResource("debugger-ui.css").toExternalForm());
 
             primaryStage.setTitle(NAME + " (" + VERSION + ") with KeY:" + KEY_VERSION);
             primaryStage.setScene(scene);

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

@@ -122,6 +122,10 @@ public class DebuggerMain implements Initializable {
     private CheckMenuItem miProofTree;
     @FXML
     private ToggleButton btnInteractiveMode;
+
+    @FXML
+    private Button interactive_undo;
+
     private JavaArea javaArea = new JavaArea();
     private DockNode javaAreaDock = new DockNode(javaArea, "Java Source",
             new MaterialDesignIconView(MaterialDesignIcon.CODEPEN)
@@ -329,18 +333,11 @@ public class DebuggerMain implements Initializable {
 
     }
 
-    //region Actions: Menu
-
-    /*@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);
+    @FXML
+    private void undo (ActionEvent e) {
+        interactiveModeController.undo(e);
     }
-    }*/
+
 
     public KeYProofFacade getFacade() {
         return FACADE;
@@ -1029,13 +1026,18 @@ public class DebuggerMain implements Initializable {
 
     @FXML
     public void interactiveMode(ActionEvent actionEvent) {
-        if (!btnInteractiveMode.isSelected()) {
+        if (btnInteractiveMode.isSelected()) {
+            assert model.getDebuggerFramework() != null;
+            interactiveModeController.setDebuggerFramework(model.getDebuggerFramework());
             interactiveModeController.setActivated(true);
             //SaG: this needs to be set to filter inapplicable rules
             this.getFacade().getEnvironment().getProofControl().setMinimizeInteraction(true);
             interactiveModeController.start(getFacade().getProof(), getInspectionViewsController().getActiveInspectionViewTab().getModel());
+
+            interactive_undo.setDisable(false);
         } else {
             interactiveModeController.stop();
+            interactive_undo.setDisable(true);
         }
     }
 
@@ -1246,6 +1248,7 @@ public class DebuggerMain implements Initializable {
             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);

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

@@ -17,6 +17,8 @@ import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 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.parser.PrettyPrinter;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
@@ -30,7 +32,10 @@ import lombok.val;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 import org.key_project.util.collection.ImmutableList;
+import recoder.util.Debug;
 
+import java.awt.event.ActionEvent;
+import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
@@ -49,17 +54,70 @@ public class InteractiveModeController {
 
     private InspectionModel model;
 
+    private DebuggerFramework<KeyData> debuggerFramework;
+    private PTreeNode<KeyData> nodeAtInteractionStart;
+
+    //needed for Undo-Operation
+    private ArrayList<CallStatement> savepointsstatement;
+    private ArrayList<Node> savepointslist;
+
+    private Proof currentProof;
 
     public void start(Proof currentProof, InspectionModel model) {
         Events.register(this);
         cases.clear();
+        this.currentProof = currentProof;
         currentProof.getSubtreeGoals(currentProof.root()).forEach(goal -> {
             cases.put(goal.node(), new Statements());
         });
         this.scriptArea = scriptController.newScript();
         this.model = model;
 
+        savepointslist = new ArrayList<>();
+        savepointsstatement = new ArrayList<>();
+        nodeAtInteractionStart = debuggerFramework.getStatePointer();
+
+    }
+
 
+    /**
+     * Undo the application of the last rule
+     */
+    public void undo(javafx.event.ActionEvent actionEvent) {
+        if(savepointslist.isEmpty()) {
+            Debug.log("Kein vorheriger Zustand."); //TODO: events fire
+            return;
+        }
+
+        val pruneNode = savepointslist.get(savepointslist.size()-1);
+        savepointslist.remove(pruneNode);
+        ImmutableList<Goal> goalsbeforePrune = currentProof.getSubtreeGoals(pruneNode);
+
+        currentProof.pruneProof(pruneNode);
+        ImmutableList<Goal> goalsafterPrune = currentProof.getSubtreeGoals(pruneNode);
+
+        ObservableList<GoalNode<KeyData>> goals = model.getGoals();
+        List<GoalNode<KeyData>> prunedChildren = goals.stream()
+                .filter(keyDataGoalNode -> goalsbeforePrune.contains(keyDataGoalNode.getData().getGoal()))
+                .collect(Collectors.toList());
+
+        KeyData kd = prunedChildren.get(0).getData();
+        goals.removeAll(prunedChildren);
+        GoalNode<KeyData> lastGoalNode = null;
+        for (Goal newGoalNode : goalsafterPrune) {
+            KeyData 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));
+
+        String c = getCasesAsString();
+        scriptArea.setText("" +
+                "//Preview \n" + c);
     }
 
     public void stop() {
@@ -127,6 +185,9 @@ public class InteractiveModeController {
     }
 
     private void applyRule(CallStatement call, Goal g) {
+        savepointslist.add(g.node());
+        savepointsstatement.add(call);
+
         ObservableList<GoalNode<KeyData>> goals = model.getGoals();
         GoalNode<KeyData> expandedNode;
         List<GoalNode<KeyData>> collect = goals.stream().filter(keyDataGoalNode -> keyDataGoalNode.getData().getGoal().equals(g)).collect(Collectors.toList());

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

@@ -40,7 +40,8 @@ public class SequentMatcher extends BorderPane {
     private final ObjectProperty<GoalNode<KeyData>> selectedGoalNodeToShow = new SimpleObjectProperty<>(this, "selectedGoalNodeToShow");
     public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
     @FXML
-    private SequentView sequentView;
+    private SequentViewForMatcher sequentView;
+
     @FXML
     private ListView<GoalNode<KeyData>> goalView;
     @FXML
@@ -73,6 +74,8 @@ public class SequentMatcher extends BorderPane {
 
         goals.addListener((observable, oldValue, newValue) -> goalView.setItems(newValue));
 
+
+        //Highlight Matchings
         matchingsView.getSelectionModel().selectedItemProperty().addListener((observable, oldValue, newValue) -> {
             if (newValue != null) {
                 newValue.forEach((name, mp) -> {
@@ -113,8 +116,12 @@ public class SequentMatcher extends BorderPane {
     }
 
     public void startMatch() {
+        sequentView.clearHighlight();
+
         Matchings matchings = MatcherFacade.matches(matchpattern.getText(), getSelectedGoalNodeToShow().getData().getNode().sequent(), true,
                 services);
+
+
         ObservableList<Map<String, MatchPath>> resultlist = FXCollections.observableArrayList(matchings);
 
         //If no matchings found, addCell "No matchings found"

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

+package edu.kit.iti.formal.psdbg.gui.controls;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.logic.NamespaceSet;
+import de.uka.ilkd.key.logic.PosInOccurrence;
+import de.uka.ilkd.key.logic.Sequent;
+import de.uka.ilkd.key.pp.*;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.settings.ProofIndependentSettings;
+import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
+import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade;
+import edu.kit.iti.formal.psdbg.termmatcher.Matchings;
+import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
+import javafx.beans.Observable;
+import javafx.beans.property.SimpleObjectProperty;
+import javafx.beans.value.ObservableBooleanValue;
+import javafx.scene.input.MouseButton;
+import javafx.scene.input.MouseEvent;
+import javafx.scene.layout.*;
+import javafx.scene.paint.Color;
+import org.fxmisc.richtext.CharacterHit;
+import org.fxmisc.richtext.CodeArea;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSLList;
+
+import java.io.StringWriter;
+import java.util.Collections;
+import java.util.Map;
+
+public class SequentViewForMatcher extends CodeArea {
+    private Services services;
+
+    private LogicPrinter lp;
+
+    private IdentitySequentPrintFilter filter;
+
+    private LogicPrinter.PosTableStringBackend backend;
+
+    private SimpleObjectProperty<de.uka.ilkd.key.proof.Goal> goal = new SimpleObjectProperty<>();
+
+    private SimpleObjectProperty<de.uka.ilkd.key.proof.Node> node = new SimpleObjectProperty<>();
+
+
+    private KeYProofFacade keYProofFacade;
+
+
+
+    public SequentViewForMatcher() {
+        getStyleClass().add("sequent-view");
+        setEditable(false);
+        node.addListener(this::update);
+    }
+
+
+
+
+
+    public void clearHighlight() {
+        clearStyle(0, getLength());
+    }
+
+
+
+
+    public void update(Observable o) {
+        Services services = node.get().proof().getEnv().getServicesForEnvironment();
+        NamespaceSet nss = services.getNamespaces();
+
+        Sequent sequent = node.get().sequent();
+        filter = new IdentitySequentPrintFilter();
+        filter.setSequent(sequent);
+
+
+        ProgramPrinter prgPrinter = new ProgramPrinter(new StringWriter());
+        this.backend = new LogicPrinter.PosTableStringBackend(80);
+
+        ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().setUseUnicode(true);
+        ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().setUsePretty(true);
+        NotationInfo.DEFAULT_UNICODE_ENABLED = true;
+        NotationInfo.DEFAULT_PRETTY_SYNTAX = true;
+
+        NotationInfo notation = new NotationInfo();
+        notation.refresh(services, true, true);
+
+        lp = new LogicPrinter(prgPrinter, notation, backend, services, false);
+        lp.printSequent(sequent);
+
+        clear();
+        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");
+        } else {
+            this.setBorder(new Border(new BorderStroke(Color.BLACK, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT)));
+            this.getStyleClass().remove("closed-sequent-view");
+            this.getStyleClass().add("sequent-view");
+        }
+    }
+
+    public Goal getGoal() {
+        return goal.get();
+    }
+
+    public void setGoal(Goal goal) {
+        this.goal.set(goal);
+    }
+
+    public SimpleObjectProperty<Goal> goalProperty() {
+        return goal;
+    }
+
+    public Node getNode() {
+        return node.get();
+    }
+
+    public void setNode(Node node) {
+        this.node.set(node);
+    }
+
+    public SimpleObjectProperty<Node> nodeProperty() {
+        return node;
+    }
+
+    public KeYProofFacade getKeYProofFacade() {
+        return keYProofFacade;
+    }
+
+    public void setKeYProofFacade(KeYProofFacade keYProofFacade) {
+        this.keYProofFacade = keYProofFacade;
+    }
+
+
+
+
+
+
+
+
+
+    public LogicPrinter.PosTableStringBackend getBackend() {
+        return backend;
+    }
+}

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

@@ -40,13 +40,11 @@ public class DebuggerMainModel {
     private ObjectProperty<InterpreterThreadState> interpreterState = new SimpleObjectProperty<>(this, "interpreterState",
             InterpreterThreadState.NO_THREAD);
 
-
     /**
      * True, iff the execution is not possible
      */
     private ObservableBooleanValue executeNotPossible = new SimpleBooleanProperty();//proofTreeController.executeNotPossibleProperty().or(FACADE.readyToExecuteProperty().not());
 
-
     /**
      *
      */

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/lulu/QuickSort.kps

@@ -46,6 +46,40 @@ cases{
 		
 }
 
+}
+
+script sort() {
+	autopilot_prep;
+
+	foreach{
+		simp_upd;
+		tryclose;
+	}
+
+// one open goal in der Bedingung: if(from < to) -> Post (split) -> Post (sort) ->
+
+seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)),length(array), any::select(heapAfter_split, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))))`;
+
+seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_split, array, arr(u))))`;
+
+
+seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort_0, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort, array, arr(u))))`;
+
+seqPermTrans formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_split, array, arr(u))))`;
+
+seqPermTrans formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort, array, arr(u))))`;
+
+seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort_0, array, arr(u))))`;
+
+auto;
+
+
 }
 
 script shorter(){

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

@@ -315,6 +315,16 @@
                             </tooltip>
                         </ToggleButton>
 
+                        <Button fx:id="interactive_undo" onAction="#undo" disable="true">
+                            <graphic>
+                                <MaterialDesignIconView glyphName="UNDO" size="24.0"/>
+                            </graphic>
+                            <tooltip>
+                                <Tooltip text="Undo"/>
+                            </tooltip>
+                        </Button>
+
+
                         <Pane HBox.hgrow="ALWAYS"/>
                         <Label text="Windows:"/>
                         <ToggleButton fx:id="togBtnCodeDock" onAction="#showCodeDock">

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.fxml

@@ -12,7 +12,8 @@
 <?import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView?>
 <?import edu.kit.iti.formal.psdbg.gui.controls.SectionPane?>
 <?import javafx.scene.layout.Pane?>
-<?import edu.kit.iti.formal.psdbg.gui.controls.SequentView?>
+<?import edu.kit.iti.formal.psdbg.gui.controls.SequentViewForMatcher?>
+
 <fx:root xmlns="http://javafx.com/javafx/8.0.121" xmlns:fx="http://javafx.com/fxml/1"
          type="edu.kit.iti.formal.psdbg.gui.controls.SequentMatcher">
     <center>
@@ -35,7 +36,7 @@
                     <SectionPane title="Sequent" minHeight="0.0" minWidth="0.0" prefHeight="633.0"
                                  prefWidth="341.0">
                         <center>
-                                <SequentView fx:id="sequentView"/>
+                                <SequentViewForMatcher fx:id="sequentView"/>
                         </center>
                     </SectionPane>
                         <SplitPane dividerPositions="0.28551136363636365" layoutX="11.0" layoutY="12.0"