Highlighting of node in proof tree, interactive mode now working a bit better

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

@@ -128,7 +128,7 @@ public class DebuggerMain implements Initializable {
     private CheckMenuItem miProofTree;
 
     @FXML
-    private Button btnIM;
+    private ToggleButton btnInteractiveMode;
 
     private JavaArea javaArea = new JavaArea();
 
@@ -199,6 +199,7 @@ public class DebuggerMain implements Initializable {
         model.setDebugMode(false);
         scriptController = new ScriptController(dockStation);
         interactiveModeController = new InteractiveModeController(scriptController);
+        btnInteractiveMode.setSelected(false);
         inspectionViewsController = new InspectionViewsController(dockStation);
         activeInspectorDock = inspectionViewsController.getActiveInterpreterTabDock();
         //register the welcome dock in the center
@@ -499,7 +500,7 @@ public class DebuggerMain implements Initializable {
         Platform.runLater(() -> {
             scriptController.getDebugPositionHighlighter().remove();
             statusBar.publishSuccessMessage("Interpreter finished.");
-            btnIM.setDisable(false);
+            btnInteractiveMode.setDisable(false);
             assert model.getDebuggerFramework() != null;
             PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer();
             State<KeyData> lastState = statePointer.getStateAfterStmt();
@@ -858,8 +859,12 @@ public class DebuggerMain implements Initializable {
 
     @FXML
     public void interactiveMode(ActionEvent actionEvent) {
-        interactiveModeController.setActivated(true);
-        interactiveModeController.start(getFacade().getProof(), getInspectionViewsController().getActiveInspectionViewTab().getModel());
+        if (btnInteractiveMode.isSelected()) {
+            interactiveModeController.start(getFacade().getProof(), getInspectionViewsController().getActiveInspectionViewTab().getModel());
+
+        } else {
+            interactiveModeController.stop();
+        }
 
 
     }

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

@@ -67,6 +67,7 @@ public class InteractiveModeController {
     public void stop() {
         Events.unregister(this);
         String c = getCasesAsString();
+        scriptController.getDockNode(scriptArea).close();
         Events.fire(new Events.InsertAtTheEndOfMainScript(c));
     }
 

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

@@ -309,17 +309,19 @@ public class ProofTree extends BorderPane {
         }
 
         if (n.childrenCount() == 0) {
-            ti.getChildren().add(new TreeItem<>(new TreeNode(
-                    n.isClosed() ? "CLOSED GOAL" : "OPEN GOAL", null)));
+            TreeItem<TreeNode> e = new TreeItem<>(new TreeNode(
+                    n.isClosed() ? "CLOSED GOAL" : "OPEN GOAL", null));
+
+            ti.getChildren().add(e);
             return ti;
         }
 
         Node node = n.child(0);
         if (n.childrenCount() == 1) {
-            ti.getChildren().add(new TreeItem<>(new TreeNode(toString(node), node)));
+            ti.getChildren().add(new TreeItem<>(new TreeNode(node.serialNr() + ": " + toString(node), node)));
             while (node.childrenCount() == 1) {
                 node = node.child(0);
-                ti.getChildren().add(new TreeItem<>(new TreeNode(toString(node), node)));
+                ti.getChildren().add(new TreeItem<>(new TreeNode(node.serialNr() + ": " + toString(node), node)));
             }
         }
 
@@ -364,20 +366,24 @@ public class ProofTree extends BorderPane {
             }
         };
         tftc.setConverter(stringConverter);
-
-        //tftc.itemProperty().addListener((p, o, n) -> repaint(tftc));
+        tftc.itemProperty().addListener((p, o, n) -> {
+            if (n != null)
+                repaint(tftc);
+        });
 
         //colorOfNodes.addListener((InvalidationListener) o -> repaint(tftc));
         return tftc;
     }
 
-    /*private void repaint(TextFieldTreeCell<TreeNode> tftc) {
+    private void repaint(TextFieldTreeCell<TreeNode> tftc) {
         Node n = tftc.getItem().node;
         tftc.setStyle("");
-        if (n != null) {
+        if (n != null && n.leaf()) {
             if (n.isClosed()) {
-                colorOfNodes.putIfAbsent(n, "green");
+                colorOfNodes.putIfAbsent(n, "seagreen");
                 //tftc.setStyle("-fx-background-color: greenyellow");
+            } else {
+                colorOfNodes.putIfAbsent(n, "darkred");
             }
             if (colorOfNodes.containsKey(n)) {
                 tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";");
@@ -385,7 +391,7 @@ public class ProofTree extends BorderPane {
         }
         expandRootToItem(tftc.getTreeItem());
 
-    }*/
+    }
 
     public Object getColorOfNodes() {
         return colorOfNodes.get();

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

@@ -15,8 +15,6 @@ import javafx.beans.value.ChangeListener;
 import javafx.beans.value.ObservableValue;
 import javafx.collections.FXCollections;
 import javafx.collections.ObservableMap;
-import org.antlr.v4.runtime.CharStream;
-import org.antlr.v4.runtime.CharStreams;
 import org.apache.commons.io.FileUtils;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
@@ -122,46 +120,6 @@ public class ScriptController {
         return getDockNode(findEditor(filepath));
     }
 
-    private DockNode getDockNode(ScriptArea editor) {
-        if (editor == null) {
-            return null;
-        }
-        return openScripts.get(editor);
-    }
-
-    /**
-     * Create a new Tab in the ScriptTabPane containing the contents of the file given as argument
-     *
-     * @param filePath to file that should be loaded to new tab
-     * @return refernce to new scriptArea in new tab
-     * @throws IOException if an Exception occurs while loading file
-     */
-    public ScriptArea createNewTab(File filePath) throws IOException {
-        filePath = filePath.getAbsoluteFile();
-        if (findEditor(filePath) == null) {
-            ScriptArea area = new ScriptArea();
-            area.mainScriptProperty().bindBidirectional(mainScript);
-            area.setFilePath(filePath);
-            DockNode dockNode = createDockNode(area);
-            openScripts.put(area, dockNode);
-
-            if (filePath.exists()) {
-                String code = FileUtils.readFileToString(filePath, "utf-8");
-                if (!area.textProperty().getValue().isEmpty()) {
-                    area.deleteText(0, area.textProperty().getValue().length());
-                }
-                area.setText(code);
-            }
-
-
-            return area;
-        } else {
-            logger.info("File already exists. Will not load it again");
-            ScriptArea area = findEditor(filePath);
-            return area;
-        }
-    }
-
     /**
      * Create new DockNode for ScriptArea Tab
      *
@@ -178,7 +136,7 @@ public class ScriptController {
         if (lastScriptArea == null)
             dockNode.dock(parent, DockPos.LEFT);
         else
-            dockNode.dock(parent, DockPos.LEFT, getDockNode(lastScriptArea));
+            dockNode.dock(parent, DockPos.CENTER, getDockNode(lastScriptArea));
 
         area.dirtyProperty().addListener(new ChangeListener<Boolean>() {
             @Override
@@ -200,6 +158,46 @@ public class ScriptController {
         return dockNode;
     }
 
+    /**
+     * Create a new Tab in the ScriptTabPane containing the contents of the file given as argument
+     *
+     * @param filePath to file that should be loaded to new tab
+     * @return refernce to new scriptArea in new tab
+     * @throws IOException if an Exception occurs while loading file
+     */
+    public ScriptArea createNewTab(File filePath) throws IOException {
+        filePath = filePath.getAbsoluteFile();
+        if (findEditor(filePath) == null) {
+            ScriptArea area = new ScriptArea();
+            area.mainScriptProperty().bindBidirectional(mainScript);
+            area.setFilePath(filePath);
+            DockNode dockNode = createDockNode(area);
+            openScripts.put(area, dockNode);
+
+            if (filePath.exists()) {
+                String code = FileUtils.readFileToString(filePath, "utf-8");
+                if (!area.textProperty().getValue().isEmpty()) {
+                    area.deleteText(0, area.textProperty().getValue().length());
+                }
+                area.setText(code);
+            }
+
+
+            return area;
+        } else {
+            logger.info("File already exists. Will not load it again");
+            ScriptArea area = findEditor(filePath);
+            return area;
+        }
+    }
+
+    public DockNode getDockNode(ScriptArea editor) {
+        if (editor == null) {
+            return null;
+        }
+        return openScripts.get(editor);
+    }
+
     /**
      * Get all breakpoints in the current area
      *

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

@@ -6,15 +6,25 @@ script test(){
     exLeft;
     andLeft;
     eqSymm formula = `agatha = butler`;
-    nnf_imp2or formula=`\foral S w6;(hates(agatha,w6) -> hates(butler,w6))`;
+    nnf_imp2or formula=`\forall S w6;(hates(agatha,w6) -> hates(butler,w6))`;
 
 }
 
-
 script SolveAgathaRiddle_1() {
     impRight;
     andLeft;
     notLeft;
+    repeat { andLeft; }
+    exLeft;
+    andLeft;
+    eqSymm formula = `agatha = butler`;
+    auto;
+}
+
+script SolveAgathaRiddle_2() {
+    impRight;
+    andLeft;
+    notLeft;
 
     andLeft;
     andLeft;
@@ -31,23 +41,7 @@ script SolveAgathaRiddle_1() {
     exLeft;
     andLeft;
     eqSymm formula = `agatha = butler`;
+    nnf_imp2or formula=`\forall S w6;(hates(agatha,w6) -> hates(butler,w6))`;
     auto;
-
-    //nnf_imp2or on= `hates(agatha, w6) -> hates(butler, w6)`;
-    //nnf_imp2or; -> wirft hier ScriptCommandNotApplicableException
-    //wirft ansonsten immer java.lang.RuntimeException: de.uka.ilkd.key.macros.scripts.meta.ConversionException: Could not convert value hates(agatha, w6) -> hates(butler, w6) to type interface de.uka.ilkd.key.logic.Term
-    //	at
-    //nnf_imp2or formula= `hates(agatha, w6) -> hates(butler, w6)`;
-    //nnf_imp2or on = `hates(agatha, w6) -> hates(butler, w6)` formula=` \forall S w6; (hates(agatha, w6) -> hates(butler, w6))`;
 }
 
-script SolveAgathaRiddle_2() {
-    impRight;
-    andLeft;
-    notLeft;
-    repeat { andLeft; }
-    exLeft;
-    andLeft;
-    eqSymm formula = `agatha = butler`;
-    auto;
-}
\ No newline at end of file

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/bubbleSort/Bubblesort.java

@@ -9,8 +9,7 @@ class Bubblesort {
 	@*/
 	
     public int[] bubbleSort(int[] arr) {
-        int temp = 0;  
-		
+        int temp = 0;
 		/*@
 			@	loop_invariant 0 <= i && i <= arr.length;
 			@	loop_invariant (\forall int a,b; a >= arr.length - i && b <= arr.length && a < b && i > 0; arr[a] <= arr[b]);
@@ -18,7 +17,6 @@ class Bubblesort {
 			@	decreases arr.length - i;
 			@*/
          for(int i=0; i < arr.length; i++){  
-			
 			/*@
 			@	loop_invariant 1 <= j && j <= arr.length - i + 1;
 			@	assignable arr[*], temp;
@@ -41,7 +39,7 @@ class Bubblesort {
 	/*@ public normal_behaviour
 	@	requires arr != null;
 	@	requires arr.length > 0;
-	@	ensures true;
+	@	ensures \result == true;
 	@*/
 	public boolean test(int[] arr) {
 		arr = bubbleSort(arr);

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

@@ -3,36 +3,8 @@ script t1(){
     cases{
        case match `?X >= 0,?X > 0  ==>`:
            cut `?X = 0`[?X \ X];
-           auto;
-
+           foreach{
+             auto;
+           }
     }
-    //foreach{
-    //    auto;
-    //}
-
-}
-
-
-
-script t2(){
-    symbex;
-    cases{
-       case match '.*x.*':
-            auto;
-
-	   default:
-	       auto;
-
-    }
-
-}
-
-
-script t(){
-    symbex;
-    foreach{
-       simp_heap;
-
-    }
-
 }

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

@@ -275,7 +275,7 @@
                             </tooltip>
                         </Button>
 
-                        <Button fx:id="btnIM" onAction="#interactiveMode" disable="true">
+                        <ToggleButton fx:id="btnInteractiveMode" onAction="#interactiveMode" disable="true">
                             <!--disable="${! controller.debugMode}"-->
                             <graphic>
                                 <MaterialDesignIconView glyphName="HAND_POINTING_RIGHT" size="24.0"/>
@@ -283,7 +283,7 @@
                             <tooltip>
                                 <Tooltip text="Start/Stop Interactive Mode"/>
                             </tooltip>
-                        </Button>
+                        </ToggleButton>
 
                         <Pane HBox.hgrow="ALWAYS"/>
                         <Label text="Windows:"/>