Commit 2c0303f2 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

bug fix and interim state

parent f0a7e8cf
Pipeline #11952 passed with stage
in 2 minutes and 23 seconds
...@@ -225,16 +225,22 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -225,16 +225,22 @@ public class DebuggerMainWindowController implements Initializable {
pc.setCurrentInterpreter(currentInterpreter); pc.setCurrentInterpreter(currentInterpreter);
pc.setMainScript(scripts.get(0)); pc.setMainScript(scripts.get(0));
pc.executeScript(this.debugMode.get());
//set all listeners
pc.currentGoalsProperty().addListener((o, old, fresh) -> { pc.currentGoalsProperty().addListener((o, old, fresh) -> {
if (fresh != null) { if (fresh != null) {
model.currentGoalNodesProperty().setAll(fresh); model.setCurrentGoalNodes(fresh);
// model.currentGoalNodesProperty().setAll(fresh);
} }
}); });
pc.executeScript(this.debugMode.get()); pc.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> {
pc.currentGoalsProperty().addListener((observable, oldValue, newValue) -> { if (newValue != null) {
model.setCurrentGoalNodes(newValue); model.setCurrentSelectedGoalNode(newValue);
}
}); });
pc.startHighlightPositionPropertyProperty().addListener((observable, oldValue, newValue) -> { pc.startHighlightPositionPropertyProperty().addListener((observable, oldValue, newValue) -> {
if (newValue.getLineNumber() > -1) { if (newValue.getLineNumber() > -1) {
tabPane.getSelectedScriptArea().highlightStmt(newValue.getLineNumber(), "line-highlight-postmortem"); tabPane.getSelectedScriptArea().highlightStmt(newValue.getLineNumber(), "line-highlight-postmortem");
...@@ -430,7 +436,7 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -430,7 +436,7 @@ public class DebuggerMainWindowController implements Initializable {
} }
public void stopDebugMode(ActionEvent actionEvent) { public void stopDebugMode(ActionEvent actionEvent) {
tabPane.getSelectedScriptArea().removeDebugHighlight();
//linenumberMainscript from model? //linenumberMainscript from model?
//tabPane.getActiveScriptAreaTab().getScriptArea().removeHighlightStmt(lineNumberMainScript); //tabPane.getActiveScriptAreaTab().getScriptArea().removeHighlightStmt(lineNumberMainScript);
//inspectionViewTabPane.getInspectionViewTab.clear(); //inspectionViewTabPane.getInspectionViewTab.clear();
......
...@@ -48,6 +48,9 @@ public class InspectionViewTabPane extends TabPane { ...@@ -48,6 +48,9 @@ public class InspectionViewTabPane extends TabPane {
tab.refresh(model); tab.refresh(model);
}); });
bindGoalNodesWithCurrentTab(model); bindGoalNodesWithCurrentTab(model);
model.javaFileProperty().addListener((observable, oldValue, newValue) -> {
tab.setShowCode(true);
});
this.getTabs().add(tab); this.getTabs().add(tab);
} }
......
...@@ -250,6 +250,9 @@ public class ScriptArea extends CodeArea { ...@@ -250,6 +250,9 @@ public class ScriptArea extends CodeArea {
} }
public void removeDebugHighlight() {
// removeHighlightStmt(this.getMainScript().getLineNumber());
}
public void unsetDebugMark(int lineNumberOfSigMainScript) { public void unsetDebugMark(int lineNumberOfSigMainScript) {
removeHighlightStmt(lineNumberOfSigMainScript - 1); removeHighlightStmt(lineNumberOfSigMainScript - 1);
} }
...@@ -313,6 +316,7 @@ public class ScriptArea extends CodeArea { ...@@ -313,6 +316,7 @@ public class ScriptArea extends CodeArea {
d.show((Node) event.getTarget(), event.getScreenX(), event.getScreenY()); d.show((Node) event.getTarget(), event.getScreenX(), event.getScreenY());
} }
private static class GutterView extends HBox { private static class GutterView extends HBox {
private final SimpleObjectProperty<GutterAnnotation> annotation = new SimpleObjectProperty<>(); private final SimpleObjectProperty<GutterAnnotation> annotation = new SimpleObjectProperty<>();
......
...@@ -99,10 +99,18 @@ public class ProofTreeController { ...@@ -99,10 +99,18 @@ public class ProofTreeController {
}; };
/**
*
*/
public ProofTreeController() { public ProofTreeController() {
//get state from blocker, who communicates with interpreter //get state from blocker, who communicates with interpreter
this.currentSelectedGoal.bindBidirectional(blocker.currentSelectedGoalProperty()); //this.currentSelectedGoal.bindBidirectional(blocker.currentSelectedGoalProperty());
blocker.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> {
Platform.runLater(() -> {
this.setCurrentSelectedGoal(newValue);
});
});
blocker.currentGoalsProperty().addListener((observable, oldValue, newValue) -> { blocker.currentGoalsProperty().addListener((observable, oldValue, newValue) -> {
Platform.runLater(() -> { Platform.runLater(() -> {
this.setCurrentGoals(newValue); this.setCurrentGoals(newValue);
...@@ -136,7 +144,7 @@ public class ProofTreeController { ...@@ -136,7 +144,7 @@ public class ProofTreeController {
//TODO handle endpoint //TODO handle endpoint
/** /**
* StepOver and return the node to shich the state pointer is pointing to * StepOver and return the node to which the state pointer is pointing to
* *
* @return * @return
*/ */
...@@ -152,7 +160,7 @@ public class ProofTreeController { ...@@ -152,7 +160,7 @@ public class ProofTreeController {
} }
//get next node //get next node
PTreeNode nextNode = stateGraphWrapper.getStepOver(currentPointer); PTreeNode nextNode = stateGraphWrapper.getStepOver(currentPointer);
//if nextnode is null ask interpreter //if nextnode is null ask interpreter to execute next statement and compute next state
if (nextNode != null) { if (nextNode != null) {
this.statePointer = nextNode; this.statePointer = nextNode;
setNewState(statePointer.getState()); setNewState(statePointer.getState());
...@@ -173,9 +181,15 @@ public class ProofTreeController { ...@@ -173,9 +181,15 @@ public class ProofTreeController {
* @return * @return
*/ */
public PTreeNode stepBack() { public PTreeNode stepBack() {
PTreeNode current = statePointer; PTreeNode current = this.statePointer;
this.statePointer = stateGraphWrapper.getStepBack(current); if (current != null) {
setNewState(statePointer.getState()); this.statePointer = stateGraphWrapper.getStepBack(current);
if (this.statePointer != null) {
setNewState(statePointer.getState());
} else {
this.statePointer = current;
}
}
//setHighlightStmt(this.statePointer.getScriptstmt().getStartPosition(), this.statePointer.getScriptstmt().getStartPosition()); //setHighlightStmt(this.statePointer.getScriptstmt().getStartPosition(), this.statePointer.getScriptstmt().getStartPosition());
return statePointer; return statePointer;
...@@ -189,7 +203,12 @@ public class ProofTreeController { ...@@ -189,7 +203,12 @@ public class ProofTreeController {
return null; return null;
} }
/**
* 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()
*
* @param debugMode
*/
public void executeScript(boolean debugMode) { public void executeScript(boolean debugMode) {
blocker.deinstall(); blocker.deinstall();
blocker.install(currentInterpreter); blocker.install(currentInterpreter);
...@@ -207,9 +226,10 @@ public class ProofTreeController { ...@@ -207,9 +226,10 @@ public class ProofTreeController {
this.stateGraphWrapper.addChangeListener(graphChangedListener); this.stateGraphWrapper.addChangeListener(graphChangedListener);
blocker.getStepUntilBlock().set(1); blocker.getStepUntilBlock().set(1);
} }
//create interpreter service and start
interpreterService.interpreterProperty().set(currentInterpreter); interpreterService.interpreterProperty().set(currentInterpreter);
interpreterService.mainScriptProperty().set(mainScript); interpreterService.mainScriptProperty().set(mainScript);
interpreterService.start(); interpreterService.start();
......
...@@ -9,4 +9,18 @@ script f(){ ...@@ -9,4 +9,18 @@ script f(){
script g(){ script g(){
impLeft; impLeft;
}
\ No newline at end of file }
script t(i:int, j:int){
symbex;
cases{
case match `x > 0 ==> `:{
}
case match `x <= 0 ==> `:{
}
}
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment