diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java index c148a223dcb8299048b7f61fb816f345a13b739f..c19adb553ebde06ce02ee1a8b8cfee29da0bf772 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java +++ b/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 statePointer = model.getDebuggerFramework().getStatePointer(); State 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(); + } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java index c96f04c029304a470da1786c7ada459d06ccfc52..ca6c1ff9ae2fa883fceb92e0f4a7675a80d3764d 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java +++ b/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)); } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java index 4e761af79140abc465b4e6267195cc79efb74003..6b8437c67fb79ddd1001e232912072e59a7dfd6d 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java +++ b/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 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 tftc) { + private void repaint(TextFieldTreeCell 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(); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java index fc7a0a7189049c36e034707c3045d5611490faa6..24841c2a18e78db0653fbe5de2a70b73232cc6a1 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java +++ b/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() { @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 * diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/script.kps index 9505412c2a392b9a36e5dfeefc67a9c98469f75a..ed9faa0af8a241485c331e383a4aee4e8dbae472 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/script.kps +++ b/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 diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/bubbleSort/Bubblesort.java b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/bubbleSort/Bubblesort.java index 098a439a84b199ae5ac5982217c18ec00e17c11e..fcac401854d6d0d5ad9807c00e73bfcc7feab29b 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/bubbleSort/Bubblesort.java +++ b/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); diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps index 4438d3226cff548c2d252097300d47fe92b37199..395b1ea3c8085f51329f59a9823701b965d4a413 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps +++ b/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; - - } - } diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml index b7a516bc745dea5225a854002acbcee3d1010d3e..a67772f5e0d6246312af844a6ad3ee55ffa0e52a 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml @@ -275,7 +275,7 @@ - +