adding userinteraction window + and as a testcase added ApplyEq Example +...

adding userinteraction window + and as a testcase added ApplyEq Example + scripttree added contextmenu though refresh has to be fixed

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

@@ -140,6 +140,22 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
                 state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
             }
         } catch (ScriptException e) {
+            //TODO: adding UserinteractionWindow
+            /*TODO: possible cases not applicable, because
+                command not recognized
+                command multiple matches -> need more specification with on + formula
+
+                command not complete -> missig parameters
+                solution:
+                if(e.getMessage().equals("Not a unique \\assumes instantiation")) {
+                    //TODO: open UserinteractionWindow
+
+                    //TODO: apply completed TacletApp
+
+                    //TODO: insert into script
+
+                }
+             */
             if (interpreter.isStrictMode()) {
                 throw new ScriptCommandNotApplicableException(e, c, map);
             } else {

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/applyEq/ApplyEqExample.java

+package edu.kit.iti.formal.psdbg.examples.applyEq;
+
+import edu.kit.iti.formal.psdbg.examples.Example;
+
+
+public class ApplyEqExample extends Example {
+
+    public ApplyEqExample() {
+        setName("ApplyEq");
+        defaultInit(getClass());
+    }
+
+}
+

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

@@ -36,6 +36,7 @@ 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.ProofScript;
 import edu.kit.iti.formal.psdbg.storage.KeyPersistentFacade;
@@ -51,12 +52,14 @@ import javafx.event.EventHandler;
 import javafx.fxml.FXML;
 import javafx.fxml.FXMLLoader;
 import javafx.fxml.Initializable;
+import javafx.scene.Scene;
 import javafx.scene.control.*;
 import javafx.scene.layout.BorderPane;
 import javafx.scene.web.WebEngine;
 import javafx.scene.web.WebView;
 import javafx.stage.FileChooser;
 import javafx.stage.Modality;
+import javafx.stage.Stage;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 import org.apache.commons.io.FileUtils;
@@ -1326,14 +1329,29 @@ public class DebuggerMain implements Initializable {
         if(startnode == null) return;
         stg.createGraph(startnode, FACADE.getProof().root());
 
-        TreeItem<AbstractTreeNode> item = (stg.toView());
+        scriptTreeView.setModel(model);
+        scriptTreeView.setFACADE(FACADE);
 
-        scriptTreeView.setTree(item);
+        scriptTreeView.setStg(stg);
+        scriptTreeView.toView();
+
+        /*TreeItem<AbstractTreeNode> item = (stg.toView());
 
+        scriptTreeView.setTree(item);
+*/
 
 
     }
 
+    @FXML
+    public void showUserInteractionW(ActionEvent actionEvent) {
+        Stage stage = new Stage();
+        stage.setTitle("Userinteraction");
+        Scene scene = new Scene(new UserinteractionWindow());
+        stage.setScene(scene);
+
+        stage.show();
+    }
 
     public DockNode getJavaAreaDock() {
         return javaAreaDock;

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

@@ -325,6 +325,14 @@ public class InteractiveModeController {
                 model.setSelectedGoalNodeToShow(last);
         } catch (Exception e) {
             if (e.getClass().equals(ScriptException.class)) {
+                if (e.getMessage().equals("Not a unique \\assumes instantiation")) {
+                    //TODO: open UserinteractionWindow
+
+                    //TODO: apply completed TacletApp
+
+                    //TODO: insert into script
+
+                }
                 System.out.println("e.getMessage() = " + e.getMessage());
                 throw new ScriptCommandNotApplicableException(e, c, map);
 

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

@@ -24,9 +24,7 @@ public class ProofTreeContextMenu extends javafx.scene.control.ContextMenu {
     MenuItem showSequent = new MenuItem("Show Sequent");
     MenuItem showGoal = new MenuItem("Show in Goal List");
     MenuItem expandAllNodes = new MenuItem("Expand Tree");
-    MenuItem showScriptTree = new MenuItem("Show ScriptTree");
 
-    //TODO: zum Testen
 
 
     private ProofTree proofTree;
@@ -88,8 +86,7 @@ public class ProofTreeContextMenu extends javafx.scene.control.ContextMenu {
             proofTree.expandRootToLeaves(proofTree.getTreeProof().getRoot());
         });
         //TODO SCRIPTTREE ACTION
-        //showScriptTree.setOnAction(event -> proofTree.getTreeScriptCreation().showScriptTree());
-        getItems().setAll(refresh, expandAllNodes, new SeparatorMenuItem(), copy, createCases, showSequent, showGoal, showScriptTree);
+        getItems().setAll(refresh, expandAllNodes, new SeparatorMenuItem(), copy, createCases, showSequent, showGoal);
         setAutoFix(true);
         setAutoHide(true);
     }

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

+package edu.kit.iti.formal.psdbg.gui.controls;
+
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
+import de.uka.ilkd.key.pp.LogicPrinter;
+import edu.kit.iti.formal.psdbg.LabelFactory;
+import edu.kit.iti.formal.psdbg.gui.controller.Events;
+import javafx.collections.ObservableList;
+import javafx.scene.control.Menu;
+import javafx.scene.control.MenuItem;
+import javafx.scene.control.SeparatorMenuItem;
+import javafx.scene.control.TreeItem;
+
+public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu {
+    MenuItem copyBranchLabel = new MenuItem("Branch Label");
+    MenuItem copyProgramLines = new MenuItem("Program Lines");
+    MenuItem createCases = new MenuItem("Created Case for Open Goals");
+    MenuItem refresh = new MenuItem("Refresh (TOFIX)");
+    MenuItem showSequent = new MenuItem("Show Sequent");
+    MenuItem showGoal = new MenuItem("Show in Goal List");
+    MenuItem expandAllNodes = new MenuItem("Expand Tree");
+
+    private ScriptTreeView scriptTreeView;
+
+    public ScriptTreeContextMenu(ScriptTreeView scriptTreeView) {
+        this.scriptTreeView = scriptTreeView;
+
+        refresh.setOnAction(event -> scriptTreeView.setTree(scriptTreeView.toView()));
+        refresh.setGraphic(new MaterialDesignIconView(MaterialDesignIcon.REFRESH));
+
+        expandAllNodes.setOnAction((event) -> {
+            expandRootToLeaves(scriptTreeView.treeView.getRoot());
+        });
+
+        getItems().setAll(refresh, expandAllNodes); //, new SeparatorMenuItem(), createCases, showSequent, showGoal);
+        setAutoFix(true);
+        setAutoHide(true);
+        /*
+        copyBranchLabel.setOnAction(evt -> proofTree.consumeNode(n -> Utils.intoClipboard(
+                LabelFactory.getBranchingLabel(n)), "Copied!"));
+
+        copyProgramLines.setOnAction(evt -> {
+            proofTree.consumeNode(n -> {
+                Utils.intoClipboard(
+                        LabelFactory.getProgramLines(n));
+            }, "Copied!");
+        });
+
+        MenuItem copySequent = new MenuItem("Sequent");
+        copySequent.setOnAction(evt -> {
+            proofTree.consumeNode(n -> {
+                assert proofTree.getServices() != null : "set KeY services!";
+                String s = LogicPrinter.quickPrintSequent(n.sequent(), proofTree.getServices());
+                Utils.intoClipboard(s);
+            }, "Copied!");
+        });
+
+        MenuItem copyRulesLabel = new MenuItem("Rule labels");
+        copyRulesLabel.setOnAction(evt -> {
+            proofTree.consumeNode(n -> {
+                Utils.intoClipboard(
+                        LabelFactory.getRuleLabel(n));
+            }, "Copied!");
+        });
+
+        MenuItem copyProgramStatements = new MenuItem("Statements");
+        copyProgramStatements.setOnAction(event -> {
+            proofTree.consumeNode(n -> {
+                Utils.intoClipboard(
+                        LabelFactory.getProgramStatmentLabel(n));
+            }, "Copied!");
+        });
+
+        Menu copy = new Menu("Copy", new MaterialDesignIconView(MaterialDesignIcon.CONTENT_COPY),
+                copyBranchLabel, copyProgramLines,
+                copyProgramStatements, copyRulesLabel,
+                copySequent);
+
+        createCases.setOnAction(this::onCreateCases);
+
+
+        showSequent.setOnAction((evt) ->
+                proofTree.consumeNode(n -> Events.fire(new Events.ShowSequent(n)), ""));
+
+        showGoal.setOnAction((evt) -> proofTree.consumeNode(n -> Events.fire(new Events.SelectNodeInGoalList(n)), "Found!"));
+
+
+        //TODO SCRIPTTREE ACTION
+        getItems().setAll(refresh, expandAllNodes, new SeparatorMenuItem(), copy, createCases, showSequent, showGoal);
+        setAutoFix(true);
+        setAutoHide(true);
+*/
+    }
+
+    static void expandRootToLeaves(TreeItem candidate) {
+        if (candidate != null) {
+            if (!candidate.isLeaf()) {
+                candidate.setExpanded(true);
+                ObservableList<TreeItem> children = candidate.getChildren();
+                children.forEach(treeItem -> expandRootToLeaves(treeItem));
+
+            }
+        }
+    }
+}

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

@@ -183,10 +183,7 @@ public class ScriptTreeGraph {
            // mapping.forEach((node, abstractTreeNode) -> System.out.println("node.serialNr() = " + node.serialNr() + " " + abstractTreeNode.toTreeNode().label));
         }
 
-    /**
-     * returns treeItem that represents current Script tree
-     * @return
-     */
+        /*
     public TreeItem<AbstractTreeNode> toView () {
         TreeItem<AbstractTreeNode> treeItem;
         if(rootNode == null) {
@@ -235,6 +232,7 @@ public class ScriptTreeGraph {
             }
             return treeItem;
         }
+        */
 
         private class ScriptVisitor extends DefaultASTVisitor<Void> {
 

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

@@ -4,15 +4,15 @@ import com.sun.javafx.css.Style;
 import de.uka.ilkd.key.proof.Node;
 import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
 import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.*;
+import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel;
+import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
+import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
 import javafx.beans.binding.Bindings;
 import javafx.beans.property.MapProperty;
 import javafx.beans.property.SimpleMapProperty;
 import javafx.collections.FXCollections;
 import javafx.fxml.FXML;
-import javafx.scene.control.ColorPicker;
-import javafx.scene.control.TreeCell;
-import javafx.scene.control.TreeItem;
-import javafx.scene.control.TreeView;
+import javafx.scene.control.*;
 import javafx.scene.control.cell.TextFieldTreeCell;
 import javafx.scene.layout.Background;
 import javafx.scene.layout.BackgroundFill;
@@ -22,6 +22,7 @@ import javafx.util.StringConverter;
 import lombok.Setter;
 
 import java.awt.*;
+import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
 
@@ -30,6 +31,15 @@ public class ScriptTreeView extends BorderPane {
     @Setter
     private ScriptTreeGraph stg;
 
+    private ContextMenu contextMenu;
+
+    private ScriptTreeNode rootNode;
+    private Map<Node, AbstractTreeNode> mapping;
+
+    @Setter
+    private DebuggerMainModel model;
+    @Setter
+    private KeYProofFacade FACADE;
     /**
      * Contains color of nodes
      */
@@ -43,7 +53,11 @@ public class ScriptTreeView extends BorderPane {
     public ScriptTreeView(DebuggerMain main) {
         Utils.createWithFXML(this);
         treeView.setCellFactory(this::cellFactory);
+        stg = new ScriptTreeGraph();
 
+        setOnContextMenuRequested(evt -> {
+            getContextMenu().show(this, evt.getScreenX(), evt.getScreenY());
+        });
     }
 
     public void setTree(TreeItem<AbstractTreeNode> tree) {
@@ -82,27 +96,46 @@ public class ScriptTreeView extends BorderPane {
      * returns treeItem that represents current Script tree
      * @return
      */
+    public TreeItem<AbstractTreeNode> toView() {
+        TreeItem<AbstractTreeNode> treeItem;
+        PTreeNode startnode;
+        try {
+            startnode = (model.getDebuggerFramework() != null) ?
+                    model.getDebuggerFramework().getPtreeManager().getStartNode() :
+                    null;
+        } catch (NullPointerException e) {
+            treeItem = new TreeItem<>(new AbstractTreeNode(null));
+            DummyGoalNode dummy = new DummyGoalNode(null, false);
+            treeItem.getChildren().add(new TreeItem<>(dummy));
 
-    /*
-    public TreeItem<TreeNode> toView () {
-        TreeItem<TreeNode> treeItem;
-        ScriptTreeNode rootNode = stg.getRootNode();
-        Map<Node, AbstractTreeNode> mapping = stg.getMapping();
-        if(rootNode == null) {
-            treeItem = new TreeItem<>(new TreeNode("Proof", null));
+            this.setTree(treeItem);
+            return treeItem;
+        }
+
+        //No script executed
+        if (startnode == null) {
+            System.out.println("Entered maybe redundaant toview(inside) method"); //TODO
+            treeItem = new TreeItem<>(new AbstractTreeNode(null));
             DummyGoalNode dummy = new DummyGoalNode(null, false);
-            treeItem.getChildren().add(new TreeItem<>(dummy.toTreeNode()));
+            treeItem.getChildren().add(new TreeItem<>(dummy));
+
+            this.setTree(treeItem);
             return treeItem;
         }
-        treeItem = new TreeItem<>(new TreeNode("Proof", rootNode.getNode()));
+        stg.createGraph(startnode, FACADE.getProof().root());
+
+        rootNode = stg.getRootNode();
+        mapping = stg.getMapping();
+
+        treeItem = new TreeItem<>(new AbstractTreeNode(null));
 
 
         List<AbstractTreeNode> children = mapping.get(rootNode.getNode()).getChildren();
         if (children == null) return treeItem;
-        treeItem.getChildren().add(new TreeItem<>(mapping.get(rootNode.getNode()).toTreeNode()));
+        treeItem.getChildren().add(new TreeItem<>(mapping.get(rootNode.getNode())));
 
         while (children.size() == 1) {
-            treeItem.getChildren().add(new TreeItem<>(children.get(0).toTreeNode()));
+            treeItem.getChildren().add(new TreeItem<>(children.get(0)));
             children = children.get(0).getChildren();
             if(children == null) return treeItem;
         }
@@ -110,18 +143,20 @@ public class ScriptTreeView extends BorderPane {
         if (children.size() != 0) {
             children.forEach(k -> treeItem.getChildren().add(rekursiveToView(k)));
         }
+
+        this.setTree(treeItem);
         return treeItem;
     }
 
-    private TreeItem<TreeNode> rekursiveToView (AbstractTreeNode current){
-        TreeItem<TreeNode> treeItem = new TreeItem<>(current.toTreeNode()); //
+    private TreeItem<AbstractTreeNode> rekursiveToView(AbstractTreeNode current) {
+        TreeItem<AbstractTreeNode> treeItem = new TreeItem<>(current); //
 
         List<AbstractTreeNode> children = current.getChildren();
 
 
         while (children != null && children.size() == 1) {
             if(children.get(0) == null) return treeItem;
-            treeItem.getChildren().add(new TreeItem<>(children.get(0).toTreeNode()));
+            treeItem.getChildren().add(new TreeItem<>(children.get(0)));
             children = children.get(0).getChildren();
         }
         if (children == null) {
@@ -133,7 +168,7 @@ public class ScriptTreeView extends BorderPane {
         }
         return treeItem;
     }
-*/
+
     private void repaint(TextFieldTreeCell<AbstractTreeNode> tftc) {
         AbstractTreeNode item = tftc.getItem();
         Node n = item.getNode();
@@ -141,7 +176,9 @@ public class ScriptTreeView extends BorderPane {
         tftc.setStyle("");
         if (n != null) {
             if(item instanceof ScriptTreeNode) {
-                tftc.setStyle("-fx-text-fill: grey");
+                if (!item.isSucc()) {
+                    tftc.setStyle("-fx-text-fill: grey");
+                }
             } else if (item instanceof BranchLabelNode) {
                 tftc.setStyle("-fx-text-fill: blue");
             } else if (item instanceof ForeachTreeNode) {
@@ -160,16 +197,13 @@ public class ScriptTreeView extends BorderPane {
                 }
             }
 
-
-                    //tftc.setStyle("-fx-background-color: greenyellow");
-                    //tftc.setStyle("-fx-background-color: " + stg.colorOfNodes.get(n) + ";");
-
-
-
             }
+    }
 
-
-
-
+    public ContextMenu getContextMenu() {
+        if (contextMenu == null) {
+            contextMenu = new ScriptTreeContextMenu(this);
+        }
+        return contextMenu;
     }
 }

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

+package edu.kit.iti.formal.psdbg.gui.controls;
+
+import javafx.fxml.FXML;
+import javafx.scene.control.Button;
+import javafx.scene.control.TextArea;
+import javafx.scene.layout.BorderPane;
+
+public class UserinteractionWindow extends BorderPane {
+
+    @FXML
+    Button cancelButton;
+
+    @FXML
+    Button applyButton;
+
+    @FXML
+    TextArea tacletDescription;
+
+    public UserinteractionWindow() {
+        Utils.createWithFXML(this);
+
+    }
+}

ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example

 edu.kit.iti.formal.psdbg.examples.contraposition.ContrapositionExample
 edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample
+edu.kit.iti.formal.psdbg.examples.applyEq.ApplyEqExample
 edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample
 edu.kit.iti.formal.psdbg.examples.java.maxtriplet.MaxTripletExample
 #edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/applyEq/problem.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.
+//
+
+// Input file for KeY standalone prover version 0.497
+\sorts {
+	S;
+}
+
+\functions {
+	S a;
+	S b;
+	S c;
+	S d;
+}
+
+\problem {
+    ((a = b) & (a = c) & (b = d)) -> a = d
+}
\ No newline at end of file

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/applyEq/script.kps

+script interaction() {
+    impRight;
+    andLeft;
+    andLeft;
+    // apply 'applyEq' on 'a' in 'a = d'
+}
+
+script mock_interaction() {
+    impRight;
+    andLeft;
+    andLeft;
+    applyEq;
+}
+
+script mock_interaction_1() {
+    impRight;
+    andLeft;
+    andLeft;
+    applyEq formula=`a = d` occ=0 on=`a`;
+}
\ No newline at end of file

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

@@ -186,6 +186,7 @@
                                 </CheckMenuItem>
                                 <CheckMenuItem fx:id="miScriptTree" onAction="#showScriptTree" text="Show Script Tree" accelerator="Ctrl+r">
 
+
                                <graphic>
                                    <ImageView>
                                    <image>
@@ -198,6 +199,8 @@
                                </graphic>
 
                            </CheckMenuItem>
+                                <CheckMenuItem fx:id="miUserInter" onAction="#showUserInteractionW"
+                                               text="Show Userinteraction Window"/>
                            <CheckMenuItem fx:id="miCommandHelp" onAction="#showCommandHelp"
                                           accelerator="F1"
                                           text="Show Command Help">

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

+<?xml version="1.0" encoding="UTF-8"?>
+
+<?import javafx.scene.control.Button?>
+<?import javafx.scene.control.TextArea?>
+<?import javafx.scene.layout.BorderPane?>
+<?import javafx.scene.text.Text?>
+
+<fx:root prefHeight="400.0" prefWidth="600.0" type="edu.kit.iti.formal.psdbg.gui.controls.UserinteractionWindow"
+         xmlns="http://javafx.com/javafx/8.0.121" xmlns:fx="http://javafx.com/fxml/1">
+    <top>
+        <BorderPane>
+            <top>
+                <Text text="Selected Taclet:"/>
+            </top>
+            <center>
+                <TextArea fx:id="tacletDescription">
+                </TextArea>
+            </center>
+        </BorderPane>
+    </top>
+
+    <center>
+
+    </center>
+
+    <bottom>
+        <BorderPane>
+            <left>
+                <Button fx:id="cancelButton" text="Cancel"/>
+            </left>
+            <right>
+                <Button fx:id="applyButton" text="Apply"/>
+            </right>
+        </BorderPane>
+
+
+    </bottom>
+</fx:root>