From 96b2b78374a2bd1a9b7b5d5c072c32c20d48f97c Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Thu, 17 Aug 2017 02:43:16 +0200 Subject: [PATCH] planning for conceptual merge of actions --- .../DebuggerMainWindowController.java | 366 ++++++++++-------- .../kit/formal/gui/controls/LineMapping.java | 11 +- .../kit/formal/gui/controls/ScriptArea.java | 171 ++++---- .../kit/formal/gui/controls/SequentView.java | 31 +- .../graphs/ProofTreeController.java | 73 +++- src/main/resources/DebuggerMain.fxml | 11 +- 6 files changed, 373 insertions(+), 290 deletions(-) diff --git a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java index 821f26e7..c051003a 100644 --- a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java +++ b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.speclang.Contract; import edu.kit.formal.gui.ProofScriptDebugger; import edu.kit.formal.gui.controls.*; +import edu.kit.formal.gui.model.Breakpoint; import edu.kit.formal.gui.model.InspectionModel; import edu.kit.formal.interpreter.Interpreter; import edu.kit.formal.interpreter.InterpreterBuilder; @@ -42,6 +43,7 @@ import java.net.URL; import java.nio.charset.Charset; import java.util.List; import java.util.ResourceBundle; +import java.util.Set; import java.util.concurrent.ExecutorService; import java.util.concurrent.Executors; @@ -128,6 +130,18 @@ public class DebuggerMainWindowController implements Initializable { scriptController.mainScriptProperty().bindBidirectional(statusBar.mainScriptIdentifierProperty()); + + } + + /** + * If the mouse moves other toolbar button, the help text should display in the status bar + */ + private void registerToolbarToStatusBar() { + /*toolbar.getChildrenUnmodifiable().forEach( + n -> n.setOnMouseEntered(statusBar.getTooltipHandler())); + + buttonStartInterpreter.setOnMouseEntered(statusBar.getTooltipHandler()); + */ } /** @@ -209,19 +223,26 @@ public class DebuggerMainWindowController implements Initializable { } + public InspectionViewsController getInspectionViewsController() { + return inspectionViewsController; + } - /** - * If the mouse moves other toolbar button, the help text should display in the status bar - */ - private void registerToolbarToStatusBar() { - /*toolbar.getChildrenUnmodifiable().forEach( - n -> n.setOnMouseEntered(statusBar.getTooltipHandler())); + public KeYProofFacade getFacade() { + return FACADE; + } - buttonStartInterpreter.setOnMouseEntered(statusBar.getTooltipHandler()); - */ + public void showCodeDock(ActionEvent actionEvent) { + if (!javaAreaDock.isDocked()) { + javaAreaDock.dock(dockStation, DockPos.RIGHT); + } } //region Actions: Execution + @FXML + public void executeToBreakpoint() { + + } + @FXML public void executeScript() { if (proofTreeController.isAlreadyExecuted()) { @@ -256,6 +277,27 @@ public class DebuggerMainWindowController implements Initializable { } } + public File getJavaFile() { + return javaFile.get(); + } + //endregion + + public void setJavaFile(File javaFile) { + this.javaFile.set(javaFile); + } + + public File getKeyFile() { + return keyFile.get(); + } + + /** + * Reload the KeY environment, to execute the script again + * TODO: reload views + * + * @param file + * @param keyfile + * @return + */ public Task reloadEnvironment(File file, boolean keyfile) { Task task = new Task() { @Override @@ -272,25 +314,6 @@ public class DebuggerMainWindowController implements Initializable { return task; } - - @FXML - public void executeScriptFromCursor() { - InterpreterBuilder ib = FACADE.buildInterpreter(); - // ib.inheritState(interpreterService.interpreterProperty().get()); - /*LineMapping lm = new LineMapping(scriptArea.getText()); - int line = lm.getLine(scriptArea.getCaretPosition()); - int inLine = lm.getCharInLine(scriptArea.getCaretPosition()); - - ib.ignoreLinesUntil(scriptController.getSelectedScriptArea().getCaretPosition()); - executeScript(ib, true);*/ - } - - @FXML - public void executeInDebugMode() { - executeScript(FACADE.buildInterpreter(), true); - } - //endregion - /** * Execute the script that with using the interpreter that is build using teh interpreterbuilder * @@ -298,7 +321,10 @@ public class DebuggerMainWindowController implements Initializable { * @param debugMode */ private void executeScript(InterpreterBuilder ib, boolean debugMode) { - + Set breakpoints = scriptController.getBreakpoints(); + if (proofTreeController.isAlreadyExecuted()) { + proofTreeController.saveGraphs(); + } this.debugMode.set(debugMode); statusBar.publishMessage("Parse ..."); try { @@ -311,7 +337,7 @@ public class DebuggerMainWindowController implements Initializable { proofTreeController.setCurrentInterpreter(currentInterpreter); proofTreeController.setMainScript(scripts.get(0)); statusBar.publishMessage("Executing script " + scripts.get(0).getName()); - proofTreeController.executeScript(this.debugMode.get(), statusBar); + proofTreeController.executeScript(this.debugMode.get(), statusBar, breakpoints); //highlight signature of main script //scriptController.setDebugMark(scripts.get(0).getStartPosition().getLineNumber()); } catch (RecognitionException e) { @@ -319,6 +345,82 @@ public class DebuggerMainWindowController implements Initializable { } } + public void openKeyFile(File keyFile) { + if (keyFile != null) { + setKeyFile(keyFile); + setInitialDirectory(keyFile.getParentFile()); + Task task = FACADE.loadKeyFileTask(keyFile); + task.setOnSucceeded(event -> { + statusBar.publishMessage("Loaded key sourceName: %s", keyFile); + statusBar.stopProgress(); + getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals()); + }); + + task.setOnFailed(event -> { + statusBar.stopProgress(); + event.getSource().exceptionProperty().get(); + Utils.showExceptionDialog("Could not load sourceName", "Key sourceName loading error", "", + (Throwable) event.getSource().exceptionProperty().get() + ); + }); + + ProgressBar bar = new ProgressBar(); + bar.progressProperty().bind(task.progressProperty()); + executorService.execute(task); + } + } + + public void openJavaFile(File javaFile) { + if (javaFile != null) { + setJavaFile(javaFile); + initialDirectory.set(javaFile.getParentFile()); + contractLoaderService.start(); + } + } + + public void setKeyFile(File keyFile) { + this.keyFile.set(keyFile); + } + + @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. + // execute residual script + + + } + + //deprecated + @FXML + public void executeScriptFromCursor() { + InterpreterBuilder ib = FACADE.buildInterpreter(); + //b.inheritState(interpreterService.interpreterProperty().get()); + + // Get State before cursor + // use goalnode to build new interpreter in proof tree controller. + // + + + //LineMapping lm = new LineMapping(scriptArea.getText()); + //int line = lm.getLine(scriptArea.getCaretPosition()); + //int inLine = lm.getCharInLine(scriptArea.getCaretPosition()); + + //ib.ignoreLinesUntil(scriptController.getSelectedScriptArea().getCaretPosition()); + //executeScript(ib, true); + } + + @FXML + public void executeInDebugMode() { + executeScript(FACADE.buildInterpreter(), true); + } + + + //endregion + + //region Santa's Little Helper //region Actions: Menu @FXML @@ -335,21 +437,47 @@ public class DebuggerMainWindowController implements Initializable { } } - @FXML - public void saveScript() { + private File openFileChooserOpenDialog(String title, String description, String... fileEndings) { + FileChooser fileChooser = getFileChooser(title, description, fileEndings); + //File sourceName = fileChooser.showOpenDialog(inspectionViewsController.getInspectionViewTab().getGoalView().getScene().getWindow()); + File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow()); + if (file != null) setInitialDirectory(file.getParentFile()); + return file; + } + + public void openScript(File scriptFile) { + assert scriptFile != null; + setInitialDirectory(scriptFile.getParentFile()); try { - scriptController.saveCurrentScript(); + String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset()); + ScriptArea area = scriptController.createNewTab(scriptFile); } catch (IOException e) { - Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save current script", e); - + Utils.showExceptionDialog("Exception occured", "", + "Could not load sourceName " + scriptFile, e); } } - private void saveScript(File scriptFile) { + private FileChooser getFileChooser(String title, String description, String[] fileEndings) { + FileChooser fileChooser = new FileChooser(); + fileChooser.setTitle(title); + fileChooser.setSelectedExtensionFilter(new FileChooser.ExtensionFilter(description, fileEndings)); + if (initialDirectory.get() == null) + setInitialDirectory(new File("src/test/resources/edu/kit/formal/interpreter/contraposition/")); + + if (!initialDirectory.get().exists()) + setInitialDirectory(new File(".")); + + fileChooser.setInitialDirectory(initialDirectory.get()); + return fileChooser; + } + + @FXML + public void saveScript() { try { - scriptController.saveCurrentScriptAs(scriptFile); + scriptController.saveCurrentScript(); } catch (IOException e) { - Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save to file " + scriptFile.getName(), e); + Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save current script", e); + } } @@ -364,15 +492,27 @@ public class DebuggerMainWindowController implements Initializable { } } - public void openScript(File scriptFile) { - assert scriptFile != null; - setInitialDirectory(scriptFile.getParentFile()); + /** + * Creates a filechooser dialog + * + * @param title of the dialog + * @param description of the files + * @param fileEndings sourceName that should be shown + * @return + */ + private File openFileChooserSaveDialog(String title, String description, String... fileEndings) { + FileChooser fileChooser = getFileChooser(title, description, fileEndings); + // File sourceName = fileChooser.showSaveDialog(inspectionViewsController.getInspectionViewTab().getGoalView().getScene().getWindow()); + File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow()); + if (file != null) setInitialDirectory(file.getParentFile()); + return file; + } + + private void saveScript(File scriptFile) { try { - String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset()); - ScriptArea area = scriptController.createNewTab(scriptFile); + scriptController.saveCurrentScriptAs(scriptFile); } catch (IOException e) { - Utils.showExceptionDialog("Exception occured", "", - "Could not load sourceName " + scriptFile, e); + Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save to file " + scriptFile.getName(), e); } } @@ -381,31 +521,7 @@ public class DebuggerMainWindowController implements Initializable { File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps"); openKeyFile(keyFile); } - - public void openKeyFile(File keyFile) { - if (keyFile != null) { - setKeyFile(keyFile); - setInitialDirectory(keyFile.getParentFile()); - Task task = FACADE.loadKeyFileTask(keyFile); - task.setOnSucceeded(event -> { - statusBar.publishMessage("Loaded key sourceName: %s", keyFile); - statusBar.stopProgress(); - getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals()); - }); - - task.setOnFailed(event -> { - statusBar.stopProgress(); - event.getSource().exceptionProperty().get(); - Utils.showExceptionDialog("Could not load sourceName", "Key sourceName loading error", "", - (Throwable) event.getSource().exceptionProperty().get() - ); - }); - - ProgressBar bar = new ProgressBar(); - bar.progressProperty().bind(task.progressProperty()); - executorService.execute(task); - } - } + //endregion /** * Save KeY proof as proof file @@ -417,67 +533,15 @@ public class DebuggerMainWindowController implements Initializable { LOGGER.error("saveProof not implemented!!!"); } - - - //endregion - - //region Santa's Little Helper - - @FXML - protected void loadJavaFile() { - File javaFile = openFileChooserOpenDialog("Select Java File", "Java Files", "java"); - openJavaFile(javaFile); - } - - public void openJavaFile(File javaFile) { - if (javaFile != null) { - setJavaFile(javaFile); - initialDirectory.set(javaFile.getParentFile()); - contractLoaderService.start(); - } - } - public void openJavaFile() { loadJavaFile(); showCodeDock(null); } - /** - * Creates a filechooser dialog - * - * @param title of the dialog - * @param description of the files - * @param fileEndings sourceName that should be shown - * @return - */ - private File openFileChooserSaveDialog(String title, String description, String... fileEndings) { - FileChooser fileChooser = getFileChooser(title, description, fileEndings); - // File sourceName = fileChooser.showSaveDialog(inspectionViewsController.getInspectionViewTab().getGoalView().getScene().getWindow()); - File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow()); - if (file != null) setInitialDirectory(file.getParentFile()); - return file; - } - - private File openFileChooserOpenDialog(String title, String description, String... fileEndings) { - FileChooser fileChooser = getFileChooser(title, description, fileEndings); - //File sourceName = fileChooser.showOpenDialog(inspectionViewsController.getInspectionViewTab().getGoalView().getScene().getWindow()); - File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow()); - if (file != null) setInitialDirectory(file.getParentFile()); - return file; - } - - private FileChooser getFileChooser(String title, String description, String[] fileEndings) { - FileChooser fileChooser = new FileChooser(); - fileChooser.setTitle(title); - fileChooser.setSelectedExtensionFilter(new FileChooser.ExtensionFilter(description, fileEndings)); - if (initialDirectory.get() == null) - setInitialDirectory(new File("src/test/resources/edu/kit/formal/interpreter/contraposition/")); - - if (!initialDirectory.get().exists()) - setInitialDirectory(new File(".")); - - fileChooser.setInitialDirectory(initialDirectory.get()); - return fileChooser; + @FXML + protected void loadJavaFile() { + File javaFile = openFileChooserOpenDialog("Select Java File", "Java Files", "java"); + openJavaFile(javaFile); } public void stepOver(ActionEvent actionEvent) { @@ -490,16 +554,10 @@ public class DebuggerMainWindowController implements Initializable { PTreeNode newState = proofTreeController.stepBack(); } - - public KeYProofFacade getFacade() { - return FACADE; - } - //region Property public boolean isDebugMode() { return debugMode.get(); } - //endregion public void setDebugMode(boolean debugMode) { this.debugMode.set(debugMode); @@ -529,12 +587,6 @@ public class DebuggerMainWindowController implements Initializable { scriptController.newScript(); } - public void showCodeDock(ActionEvent actionEvent) { - if (!javaAreaDock.isDocked()) { - javaAreaDock.dock(dockStation, DockPos.RIGHT); - } - } - public void showWelcomeDock(ActionEvent actionEvent) { if (!welcomePaneDock.isDocked()) { welcomePaneDock.dock(dockStation, DockPos.CENTER); @@ -580,10 +632,6 @@ public class DebuggerMainWindowController implements Initializable { return proofTreeController; } - public InspectionViewsController getInspectionViewsController() { - return inspectionViewsController; - } - public ExecutorService getExecutorService() { return executorService; } @@ -608,26 +656,10 @@ public class DebuggerMainWindowController implements Initializable { return welcomePane; } - public File getJavaFile() { - return javaFile.get(); - } - - public void setJavaFile(File javaFile) { - this.javaFile.set(javaFile); - } - public ObjectProperty javaFileProperty() { return javaFile; } - public File getKeyFile() { - return keyFile.get(); - } - - public void setKeyFile(File keyFile) { - this.keyFile.set(keyFile); - } - public ObjectProperty keyFileProperty() { return keyFile; } @@ -657,16 +689,6 @@ public class DebuggerMainWindowController implements Initializable { } public class ContractLoaderService extends Service> { - @Override - protected Task> createTask() { - return FACADE.getContractsForJavaFileTask(getJavaFile()); - } - - @Override - protected void failed() { - Utils.showExceptionDialog("", "", "", exceptionProperty().get()); - } - @Override protected void succeeded() { statusBar.publishMessage("Contract loaded"); @@ -683,6 +705,16 @@ public class DebuggerMainWindowController implements Initializable { } }); } + + @Override + protected void failed() { + Utils.showExceptionDialog("", "", "", exceptionProperty().get()); + } + + @Override + protected Task> createTask() { + return FACADE.getContractsForJavaFileTask(getJavaFile()); + } } //endregion diff --git a/src/main/java/edu/kit/formal/gui/controls/LineMapping.java b/src/main/java/edu/kit/formal/gui/controls/LineMapping.java index baf4e288..f15205f9 100644 --- a/src/main/java/edu/kit/formal/gui/controls/LineMapping.java +++ b/src/main/java/edu/kit/formal/gui/controls/LineMapping.java @@ -8,6 +8,9 @@ import java.util.List; * @version 1 (04.06.17) */ public class LineMapping { + /** + * Position of new lines in the given string value. + */ private List marks = new ArrayList<>(); public LineMapping(String value) { @@ -29,14 +32,14 @@ public class LineMapping { return marks.size(); } - public int getLineStart(int line) { - return marks.get(line); - } - public int getLineEnd(int line) { return getLineStart(line + 1) - 1; } + public int getLineStart(int line) { + return marks.get(line); + } + public int getCharInLine(int caretPosition) { return caretPosition - getLineStart(getLine(caretPosition)); } diff --git a/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java b/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java index 0c957650..5d59d92a 100644 --- a/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java +++ b/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java @@ -149,29 +149,43 @@ public class ScriptArea extends CodeArea { } - private void highlightNonExecutionArea() { - if (hasExecutionMarker()) { - getStyleSpans(0, getExecutionMarkerPosition()).forEach(span -> { - span.getStyle().add("NON_EXE_AREA"); - }); - //setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA")); - } - } + private void installPopup() { + javafx.stage.Popup popup = new javafx.stage.Popup(); + setMouseOverTextDelay(Duration.ofSeconds(1)); + addEventHandler(MouseOverTextEvent.MOUSE_OVER_TEXT_BEGIN, e -> { + int chIdx = e.getCharacterIndex(); + popup.getContent().setAll( + createPopupInformation(chIdx) + ); - private boolean hasExecutionMarker() { - return getText().contains(EXECUTION_MARKER); + Point2D pos = e.getScreenPosition(); + popup.show(this, pos.getX(), pos.getY() + 10); + }); +/* + addEventHandler(MouseOverTextEvent.MOUSE_OVER_TEXT_END, e -> { + popup.hide(); + });*/ + + popup.setAutoHide(true); } - public void showContextMenu(MouseEvent mouseEvent) { - if (contextMenu.isShowing()) - contextMenu.hide(); + private void updateMainScriptMarker() { + try { + MainScriptIdentifier ms = mainScript.get(); + LOGGER.debug("ScriptArea.updateMainScriptMarker"); - if (mouseEvent.getButton() == MouseButton.SECONDARY) { - contextMenu.setAutoHide(true); - contextMenu.show(this, mouseEvent.getScreenX(), mouseEvent.getScreenY()); - mouseEvent.consume(); - } else { + if (ms != null && filePath.get().getAbsolutePath().equals(ms.getSourceName())) { + System.out.println(ms); + CharStream stream = CharStreams.fromString(getText(), filePath.get().getAbsolutePath()); + Optional ps = ms.find(Facade.getAST(stream)); + if (ps.isPresent()) { + setMainMarker(ps.get().getStartPosition().getLineNumber()); + return; + } + } + setMainMarker(-1); + } catch (NullPointerException e) { } } @@ -190,44 +204,30 @@ public class ScriptArea extends CodeArea { }); } - private void updateMainScriptMarker() { + private void highlightProblems() { + LinterStrategy ls = LinterStrategy.getDefaultLinter(); try { - MainScriptIdentifier ms = mainScript.get(); - LOGGER.debug("ScriptArea.updateMainScriptMarker"); - - if (ms != null && filePath.get().getAbsolutePath().equals(ms.getSourceName())) { - System.out.println(ms); - CharStream stream = CharStreams.fromString(getText(), filePath.get().getAbsolutePath()); - Optional ps = ms.find(Facade.getAST(stream)); - - if (ps.isPresent()) { - setMainMarker(ps.get().getStartPosition().getLineNumber()); - return; + problems.setAll(ls.check(Facade.getAST(CharStreams.fromString(getText())))); + for (LintProblem p : problems) { + for (Token tok : p.getMarkTokens()) { + Set problem = new HashSet<>(); + problem.add("problem"); + setStyle(tok.getStartIndex(), + tok.getStopIndex() + 1, problem); } } - setMainMarker(-1); - } catch (NullPointerException e) { + } catch (Exception e) { + //catch parsing exceptions } } - private void installPopup() { - javafx.stage.Popup popup = new javafx.stage.Popup(); - setMouseOverTextDelay(Duration.ofSeconds(1)); - addEventHandler(MouseOverTextEvent.MOUSE_OVER_TEXT_BEGIN, e -> { - int chIdx = e.getCharacterIndex(); - popup.getContent().setAll( - createPopupInformation(chIdx) - ); - - Point2D pos = e.getScreenPosition(); - popup.show(this, pos.getX(), pos.getY() + 10); - }); -/* - addEventHandler(MouseOverTextEvent.MOUSE_OVER_TEXT_END, e -> { - popup.hide(); - });*/ - - popup.setAutoHide(true); + private void highlightNonExecutionArea() { + if (hasExecutionMarker()) { + getStyleSpans(0, getExecutionMarkerPosition()).forEach(span -> { + span.getStyle().add("NON_EXE_AREA"); + }); + //setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA")); + } } private Node createPopupInformation(int chIdx) { @@ -245,20 +245,30 @@ public class ScriptArea extends CodeArea { return box; } - private void highlightProblems() { - LinterStrategy ls = LinterStrategy.getDefaultLinter(); - try { - problems.setAll(ls.check(Facade.getAST(CharStreams.fromString(getText())))); - for (LintProblem p : problems) { - for (Token tok : p.getMarkTokens()) { - Set problem = new HashSet<>(); - problem.add("problem"); - setStyle(tok.getStartIndex(), - tok.getStopIndex() + 1, problem); - } - } - } catch (Exception e) { - //catch parsing exceptions + public void setMainMarker(int lineNumber) { + gutter.lineAnnotations.forEach(a -> a.setMainScript(false)); + if (lineNumber > 0) + gutter.getLineAnnotation(lineNumber - 1).setMainScript(true); + } + + private boolean hasExecutionMarker() { + return getText().contains(EXECUTION_MARKER); + } + + public int getExecutionMarkerPosition() { + return getText().lastIndexOf(EXECUTION_MARKER); + } + + public void showContextMenu(MouseEvent mouseEvent) { + if (contextMenu.isShowing()) + contextMenu.hide(); + + if (mouseEvent.getButton() == MouseButton.SECONDARY) { + contextMenu.setAutoHide(true); + contextMenu.show(this, mouseEvent.getScreenX(), mouseEvent.getScreenY()); + mouseEvent.consume(); + } else { + } } @@ -274,11 +284,6 @@ public class ScriptArea extends CodeArea { return mainScript; } - public void setText(String text) { - clear(); - insertText(0, text); - } - private void toggleBreakpoint(int idx) { GutterAnnotation a = gutter.getLineAnnotation(idx); a.setBreakpoint(!a.isBreakpoint()); @@ -296,12 +301,6 @@ public class ScriptArea extends CodeArea { return filePath; } - public void setMainMarker(int lineNumber) { - gutter.lineAnnotations.forEach(a -> a.setMainScript(false)); - if (lineNumber > 0) - gutter.getLineAnnotation(lineNumber - 1).setMainScript(true); - } - public Collection getBreakpoints() { List list = new ArrayList<>(); int line = 0; @@ -384,6 +383,11 @@ public class ScriptArea extends CodeArea { //Events.unregister(this); } + public void setText(String text) { + clear(); + insertText(0, text); + } + private String getTextWithoutMarker() { return getText().replace("" + EXECUTION_MARKER, ""); } @@ -403,7 +407,7 @@ public class ScriptArea extends CodeArea { String tapName = tap.getApp().taclet().displayName(); SequentFormula seqForm = tap.getPio().sequentFormula(); - //transofrm term to parsable string representation + //transform term to parsable string representation String term = Utils.toPrettyTerm(seqForm.formula()); @@ -429,12 +433,6 @@ public class ScriptArea extends CodeArea { } - - - public int getExecutionMarkerPosition() { - return getText().lastIndexOf(EXECUTION_MARKER); - } - private static class GutterView extends HBox { private final SimpleObjectProperty annotation = new SimpleObjectProperty<>(); @@ -484,6 +482,10 @@ public class ScriptArea extends CodeArea { addPlaceholder(); } + public GutterAnnotation getAnnotation() { + return annotation.get(); + } + private void addPlaceholder() { Label lbl = new Label(); lbl.setMinWidth(12); @@ -491,11 +493,6 @@ public class ScriptArea extends CodeArea { getChildren().add(lbl); } - - public GutterAnnotation getAnnotation() { - return annotation.get(); - } - public void setAnnotation(GutterAnnotation annotation) { this.annotation.set(annotation); } diff --git a/src/main/java/edu/kit/formal/gui/controls/SequentView.java b/src/main/java/edu/kit/formal/gui/controls/SequentView.java index 927c8bd2..e582b4b2 100644 --- a/src/main/java/edu/kit/formal/gui/controls/SequentView.java +++ b/src/main/java/edu/kit/formal/gui/controls/SequentView.java @@ -59,6 +59,18 @@ public class SequentView extends CodeArea { mouseEvent.consume(); } + private void hightlightRange(int start, int end) { + try { + clearHighlight(); + setStyleClass(start, end, "sequent-highlight"); + } catch (IllegalStateException e) { + } + } + + private void clearHighlight() { + clearStyle(0, getLength()); + } + public void onMouseClick(MouseEvent e) { if (menu != null && menu.isShowing()) { menu.hide(); @@ -94,18 +106,6 @@ public class SequentView extends CodeArea { } - private void hightlightRange(int start, int end) { - try { - clearHighlight(); - setStyleClass(start, end, "sequent-highlight"); - } catch (IllegalStateException e) { - } - } - - private void clearHighlight() { - clearStyle(0, getLength()); - } - public void update(Observable o) { Services services = node.get().proof().getEnv().getServicesForEnvironment(); NamespaceSet nss = services.getNamespaces(); @@ -130,8 +130,15 @@ public class SequentView extends CodeArea { clear(); insertText(0, backend.getString()); if (node.get().isClosed()) { + System.out.println("Closed " + node.get().sequent()); 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"); + } } diff --git a/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java b/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java index 998742cf..5b6bebda 100644 --- a/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java +++ b/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java @@ -1,9 +1,11 @@ package edu.kit.formal.interpreter.graphs; import com.google.common.eventbus.Subscribe; +import com.google.common.graph.MutableValueGraph; import edu.kit.formal.gui.controller.Events; import edu.kit.formal.gui.controller.PuppetMaster; import edu.kit.formal.gui.controls.DebuggerStatusBar; +import edu.kit.formal.gui.model.Breakpoint; import edu.kit.formal.interpreter.Interpreter; import edu.kit.formal.interpreter.InterpretingService; import edu.kit.formal.interpreter.data.GoalNode; @@ -19,6 +21,7 @@ import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import java.util.List; +import java.util.Set; /** * Class controlling and maintaining proof tree structure for debugger and handling step functions for the debugger @@ -138,17 +141,18 @@ public class ProofTreeController { } - /** - * Build the control flow graph for looking up step-edges for the given script inligning called script commands + * Sets the properties that may notify GUI about statechanges with new state values * - * @param mainScript + * @param state */ - private void buildControlFlowGraph(ProofScript mainScript) { - this.controlFlowGraphVisitor = new ControlFlowVisitor(currentInterpreter.getFunctionLookup()); - mainScript.accept(controlFlowGraphVisitor); - System.out.println("CFG\n" + controlFlowGraphVisitor.asdot()); - + private void setNewState(State state) { + setCurrentGoals(state == null ? null : state.getGoals()); + setCurrentSelectedGoal(state == null ? null : state.getSelectedGoalNode()); + setCurrentHighlightNode(statePointer.getScriptstmt()); + LOGGER.debug("New State from this command: {}@{}", + this.statePointer.getScriptstmt().getNodeName(), + this.statePointer.getScriptstmt().getStartPosition()); } //TODO handle endpoint @@ -189,7 +193,7 @@ public class ProofTreeController { /** * Step Back one Node in the stategraph * - * @return + * @return PTreeNode of current pointer */ public PTreeNode stepBack() { PTreeNode current = this.statePointer; @@ -214,6 +218,17 @@ public class ProofTreeController { return null; } + /** + * Execute script with breakpoints + * @param debugMode + * @param statusBar + * @param breakpoints + */ + public void executeScript(boolean debugMode, DebuggerStatusBar statusBar, Set breakpoints) { + breakpoints.forEach(breakpoint -> blocker.addBreakpoint(breakpoint.getLineNumber())); + executeScript(debugMode, statusBar); + } + /** * Execute the script that is identified by the mainscript. * If this method is executed with debug mode true, it executes only statements after invoking the methods stepOver() and stepInto() @@ -243,6 +258,7 @@ public class ProofTreeController { this.stateGraphWrapper.install(currentInterpreter); this.stateGraphWrapper.addChangeListener(graphChangedListener); + blocker.getStepUntilBlock().set(1); } @@ -265,19 +281,22 @@ public class ProofTreeController { } /** - * Sets the properties that may notify GUI about statechanges with new state values + * Build the control flow graph for looking up step-edges for the given script inligning called script commands * - * @param state + * @param mainScript */ - private void setNewState(State state) { - setCurrentGoals(state==null? null : state.getGoals()); - setCurrentSelectedGoal(state==null?null:state.getSelectedGoalNode()); - setCurrentHighlightNode(statePointer.getScriptstmt()); - LOGGER.debug("New State from this command: {}@{}", - this.statePointer.getScriptstmt().getNodeName(), - this.statePointer.getScriptstmt().getStartPosition()); + private void buildControlFlowGraph(ProofScript mainScript) { + this.controlFlowGraphVisitor = new ControlFlowVisitor(currentInterpreter.getFunctionLookup()); + mainScript.accept(controlFlowGraphVisitor); + System.out.println("CFG\n" + controlFlowGraphVisitor.asdot()); + } + /** + * Handle the event that the script was modified + * + * @param mod + */ @Subscribe public void handle(Events.ScriptModificationEvent mod) { LOGGER.debug("ProofTreeController.handleScriptModificationEvent"); @@ -287,6 +306,24 @@ public class ProofTreeController { this.setCurrentGoals(currentInterpreter.getCurrentGoals()); } + /** + * Save all data structures to compare before reexecution + */ + public void saveGraphs() { + MutableValueGraph stateGraph = stateGraphWrapper.getStateGraph(); + MutableValueGraph ctrlFlow = controlFlowGraphVisitor.getGraph(); + } + + + private boolean compareCtrlFlowNodes(ControlFlowNode newNode, ControlFlowNode oldNode) { + return newNode.getScriptstmt().getNodeName().equals(oldNode.getScriptstmt().getNodeName()); + + } + + private boolean comparePTreeNodes(PTreeNode newTreeNode, PTreeNode oldTreeNode) { + + return false; + } /************************************************************************************************************** * diff --git a/src/main/resources/DebuggerMain.fxml b/src/main/resources/DebuggerMain.fxml index 2dc88a6e..ce259745 100644 --- a/src/main/resources/DebuggerMain.fxml +++ b/src/main/resources/DebuggerMain.fxml @@ -4,7 +4,6 @@ - @@ -92,13 +91,21 @@ + + + + + -- GitLab