Commit 5f18506f authored by Sarah Grebing's avatar Sarah Grebing

Merge remote-tracking branch 'origin/master'

parents a280e9f6 b1f5abcc
Pipeline #16977 failed with stages
in 1 minute and 27 seconds
...@@ -114,6 +114,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -114,6 +114,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
s.setSignature(sig); s.setSignature(sig);
} }
s.setBody((Statements) ctx.body.accept(this)); s.setBody((Statements) ctx.body.accept(this));
s.getBody().setParent(s);
return s; return s;
} }
......
...@@ -161,10 +161,10 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -161,10 +161,10 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
} }
private Value evaluate(GoalNode<T> g, Expression expr) { private Value evaluate(GoalNode<T> g, Expression expr) {
enterScope(expr); //enterScope(expr);
Evaluator<T> evaluator = new Evaluator<>(g.getAssignments(), g); Evaluator<T> evaluator = new Evaluator<>(g.getAssignments(), g);
evaluator.setMatcher(matcherApi); evaluator.setMatcher(matcherApi);
exitScope(expr); //exitScope(expr);
return evaluator.eval(expr); return evaluator.eval(expr);
} }
......
...@@ -134,7 +134,7 @@ public class DebuggerFramework<T> { ...@@ -134,7 +134,7 @@ public class DebuggerFramework<T> {
private void run() { private void run() {
try { try {
interpreter.interpret(mainScript); interpreter.interpret(mainScript);
//dummyproofnode ptreeManager.fireStatePointerChanged();
succeedListener.accept(this); succeedListener.accept(this);
} catch (Exception e) { } catch (Exception e) {
error = e; error = e;
......
package edu.kit.iti.formal.psdbg; package edu.kit.iti.formal.psdbg.interpreter.dbg;
import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
public class StepIntoCommand<T> extends DebuggerCommand<T> { public class StepIntoCommand<T> extends DebuggerCommand<T> {
@Override @Override
public void execute(DebuggerFramework<T> dbg) { public void execute(DebuggerFramework<T> dbg) {
PTreeNode<T> statePointer = dbg.getStatePointer(); PTreeNode<T> statePointer = dbg.getStatePointer();
assert statePointer != null; assert statePointer != null;
if (statePointer.isAtomic()) { if (statePointer.isAtomic()) { // atomic same as step over
new StepOverCommand<T>().execute(dbg); new StepOverCommand<T>().execute(dbg);
} else { } else {
dbg.releaseUntil(new Blocker.CounterBlocker(1)); if (statePointer.getStepInto() != null) { // if there is already an step into take it!
dbg.setStatePointer(statePointer.getStepInto());
} else {
if (!statePointer.isLastNode()) { // execute non last commands, one step wide!
dbg.releaseUntil(new Blocker.CounterBlocker(1));
}
}
} }
} }
} }
...@@ -114,7 +114,7 @@ public class ContractChooser extends Dialog<Contract> { ...@@ -114,7 +114,7 @@ public class ContractChooser extends Dialog<Contract> {
text.getChildren().add(contract); text.getChildren().add(contract);
text.getChildren().add(name); text.getChildren().add(name);
text.getChildren().add(new Text("\n")); text.getChildren().add(new Text("\n"));
//text.getChildren().add(tcontent); //text.getChildren().addCell(tcontent);
for (String line : content.split("\n")) { for (String line : content.split("\n")) {
if (line.contains(":")) { if (line.contains(":")) {
......
...@@ -20,6 +20,8 @@ import edu.kit.iti.formal.psdbg.examples.Examples; ...@@ -20,6 +20,8 @@ import edu.kit.iti.formal.psdbg.examples.Examples;
import edu.kit.iti.formal.psdbg.fmt.DefaultFormatter; import edu.kit.iti.formal.psdbg.fmt.DefaultFormatter;
import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger; import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger;
import edu.kit.iti.formal.psdbg.gui.controls.*; import edu.kit.iti.formal.psdbg.gui.controls.*;
import edu.kit.iti.formal.psdbg.gui.graph.Graph;
import edu.kit.iti.formal.psdbg.gui.graph.GraphView;
import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel; import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel;
import edu.kit.iti.formal.psdbg.gui.model.InspectionModel; import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
import edu.kit.iti.formal.psdbg.gui.model.InterpreterThreadState; import edu.kit.iti.formal.psdbg.gui.model.InterpreterThreadState;
...@@ -69,8 +71,6 @@ import java.util.*; ...@@ -69,8 +71,6 @@ import java.util.*;
import java.util.concurrent.*; import java.util.concurrent.*;
import java.util.stream.Collectors; import java.util.stream.Collectors;
import org.reactfx.util.Timer;
/** /**
* Controller for the Debugger MainWindow * Controller for the Debugger MainWindow
* *
...@@ -88,76 +88,53 @@ public class DebuggerMain implements Initializable { ...@@ -88,76 +88,53 @@ public class DebuggerMain implements Initializable {
@Getter @Getter
private final DebuggerMainModel model = new DebuggerMainModel(); private final DebuggerMainModel model = new DebuggerMainModel();
private final GraphView graphView = new GraphView();
private final Graph.PTreeGraph graph = graphView.getGraph();
private final DockNode graphViewNode = new DockNode(graphView, "Debug graph");
private InspectionViewsController inspectionViewsController; private InspectionViewsController inspectionViewsController;
private ScriptController scriptController; private ScriptController scriptController;
@FXML @FXML
private DebuggerStatusBar statusBar; private DebuggerStatusBar statusBar;
@FXML @FXML
private DockPane dockStation; private DockPane dockStation;
@FXML @FXML
private ToggleButton togBtnCommandHelp; private ToggleButton togBtnCommandHelp;
@FXML @FXML
private ToggleButton togBtnProofTree; private ToggleButton togBtnProofTree;
@FXML @FXML
private ToggleButton togBtnActiveInspector; private ToggleButton togBtnActiveInspector;
@FXML @FXML
private ToggleButton togBtnWelcome; private ToggleButton togBtnWelcome;
@FXML @FXML
private ToggleButton togBtnCodeDock; private ToggleButton togBtnCodeDock;
@FXML @FXML
private CheckMenuItem miCommandHelp; private CheckMenuItem miCommandHelp;
@FXML @FXML
private CheckMenuItem miCodeDock; private CheckMenuItem miCodeDock;
@FXML @FXML
private CheckMenuItem miWelcomeDock; private CheckMenuItem miWelcomeDock;
@FXML @FXML
private CheckMenuItem miActiveInspector; private CheckMenuItem miActiveInspector;
@FXML @FXML
private CheckMenuItem miProofTree; private CheckMenuItem miProofTree;
@FXML @FXML
private ToggleButton btnInteractiveMode; private ToggleButton btnInteractiveMode;
private JavaArea javaArea = new JavaArea(); private JavaArea javaArea = new JavaArea();
private DockNode javaAreaDock = new DockNode(javaArea, "Java Source", private DockNode javaAreaDock = new DockNode(javaArea, "Java Source",
new MaterialDesignIconView(MaterialDesignIcon.CODEPEN) new MaterialDesignIconView(MaterialDesignIcon.CODEPEN)
); );
//----------------------------------------------------------------------------------------------------------------- //-----------------------------------------------------------------------------------------------------------------
private ProofTree proofTree = new ProofTree(); private ProofTree proofTree = new ProofTree();
private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree"); private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree");
private WelcomePane welcomePane = new WelcomePane(this); private WelcomePane welcomePane = new WelcomePane(this);
private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT)); private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT));
private DockNode activeInspectorDock; private DockNode activeInspectorDock;
private CommandHelp commandHelp = new CommandHelp(); private CommandHelp commandHelp = new CommandHelp();
private DockNode commandHelpDock = new DockNode(commandHelp, "DebuggerCommand Help"); private DockNode commandHelpDock = new DockNode(commandHelp, "DebuggerCommand Help");
private InteractiveModeController interactiveModeController; private InteractiveModeController interactiveModeController;
@FXML @FXML
private Menu examplesMenu; private Menu examplesMenu;
private Timer interpreterThreadTimer; private Timer interpreterThreadTimer;
@Subscribe @Subscribe
...@@ -303,6 +280,8 @@ public class DebuggerMain implements Initializable { ...@@ -303,6 +280,8 @@ public class DebuggerMain implements Initializable {
* @see {@link #handleStatePointer(PTreeNode)} * @see {@link #handleStatePointer(PTreeNode)}
*/ */
private void handleStatePointerUI(PTreeNode<KeyData> node) { private void handleStatePointerUI(PTreeNode<KeyData> node) {
graph.addPartiallyAndMark(node);
if (node != null) { if (node != null) {
getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt()); getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt());
scriptController.getDebugPositionHighlighter().highlight(node.getStatement()); scriptController.getDebugPositionHighlighter().highlight(node.getStatement());
...@@ -326,7 +305,7 @@ public class DebuggerMain implements Initializable { ...@@ -326,7 +305,7 @@ public class DebuggerMain implements Initializable {
showCodeDock(null); showCodeDock(null);
}); });
//add listener for linehighlighting when changing selection in inspectionview //addCell listener for linehighlighting when changing selection in inspectionview
getInspectionViewsController().getActiveInspectionViewTab().getModel().highlightedJavaLinesProperty(). getInspectionViewsController().getActiveInspectionViewTab().getModel().highlightedJavaLinesProperty().
addListener((observable, oldValue, newValue) -> { addListener((observable, oldValue, newValue) -> {
if (newValue != null) { if (newValue != null) {
...@@ -346,6 +325,19 @@ public class DebuggerMain implements Initializable { ...@@ -346,6 +325,19 @@ public class DebuggerMain implements Initializable {
} }
//region Actions: Menu
/*@FXML
public void saveAsScript() throws IOException {
File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps");
if (f != null) {
/* if(!f.exists()){
f.createNewFile();
}
saveScript(f);
}
}*/
public KeYProofFacade getFacade() { public KeYProofFacade getFacade() {
return FACADE; return FACADE;
} }
...@@ -365,19 +357,6 @@ public class DebuggerMain implements Initializable { ...@@ -365,19 +357,6 @@ public class DebuggerMain implements Initializable {
}); });
} }
//region Actions: Menu
/*@FXML
public void saveAsScript() throws IOException {
File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps");
if (f != null) {
/* if(!f.exists()){
f.createNewFile();
}
saveScript(f);
}
}*/
public void showCodeDock(ActionEvent actionEvent) { public void showCodeDock(ActionEvent actionEvent) {
if (!javaAreaDock.isDocked()) { if (!javaAreaDock.isDocked()) {
javaAreaDock.dock(dockStation, DockPos.RIGHT); javaAreaDock.dock(dockStation, DockPos.RIGHT);
...@@ -474,7 +453,6 @@ public class DebuggerMain implements Initializable { ...@@ -474,7 +453,6 @@ public class DebuggerMain implements Initializable {
} }
} }
/** /**
* Execute the script that with using the interpreter that is build using the interpreterbuilder * Execute the script that with using the interpreter that is build using the interpreterbuilder
* *
...@@ -535,12 +513,46 @@ public class DebuggerMain implements Initializable { ...@@ -535,12 +513,46 @@ public class DebuggerMain implements Initializable {
}); });
} }
@FXML
public void debugGraph(ActionEvent event) {
if (!graphViewNode.isDocked() && !graphViewNode.isFloating()) {
graphViewNode.dock(dockStation, DockPos.CENTER);
}
graph.clear(true);
for (PTreeNode<KeyData> n : model.getDebuggerFramework().getStates()) {
graph.addCell(n);
}
for (PTreeNode<KeyData> n : model.getDebuggerFramework().getStates()) {
if (n.getStepOver() != null) {
graph.addEdge(n, n.getStepOver(), "over");
}
if (n.getStepInto() != null) {
graph.addEdge(n, n.getStepInto(), "into");
}
if (n.getStepInvOver() != null) {
graph.addEdge(n, n.getStepInvOver(), "revo");
}
if (n.getStepInvInto() != null) {
graph.addEdge(n, n.getStepInvInto(), "otni");
}
if (n.getStepReturn() != null) {
graph.addEdge(n, n.getStepReturn(), "rtrn");
}
}
}
@FXML @FXML
public void debugPrintDot(@Nullable ActionEvent ae) { public void debugPrintDot(@Nullable ActionEvent ae) {
if (model.getDebuggerFramework() == null) { if (model.getDebuggerFramework() == null) {
statusBar.publishErrorMessage("can print debug info, no debugger started!"); statusBar.publishErrorMessage("can print debug info, no debugger started!");
return; return;
} }
debugGraph(ae);
try (PrintWriter out = new PrintWriter(new FileWriter("debug.dot"))) { try (PrintWriter out = new PrintWriter(new FileWriter("debug.dot"))) {
out.println("digraph G {"); out.println("digraph G {");
for (PTreeNode<KeyData> n : model.getDebuggerFramework().getStates()) { for (PTreeNode<KeyData> n : model.getDebuggerFramework().getStates()) {
...@@ -729,6 +741,7 @@ public class DebuggerMain implements Initializable { ...@@ -729,6 +741,7 @@ public class DebuggerMain implements Initializable {
/** /**
* Reload a problem from the beginning * Reload a problem from the beginning
*
* @param event * @param event
*/ */
@FXML @FXML
...@@ -765,6 +778,7 @@ public class DebuggerMain implements Initializable { ...@@ -765,6 +778,7 @@ public class DebuggerMain implements Initializable {
} }
@FXML @FXML
public void closeProgram() { public void closeProgram() {
System.exit(0); System.exit(0);
...@@ -914,6 +928,7 @@ public class DebuggerMain implements Initializable { ...@@ -914,6 +928,7 @@ public class DebuggerMain implements Initializable {
/** /**
* Perform a step back * Perform a step back
* Does stepinto back * Does stepinto back
*
* @param actionEvent * @param actionEvent
*/ */
public void stepBack(ActionEvent actionEvent) { public void stepBack(ActionEvent actionEvent) {
...@@ -1048,7 +1063,7 @@ public class DebuggerMain implements Initializable { ...@@ -1048,7 +1063,7 @@ public class DebuggerMain implements Initializable {
webEngine.load(url); webEngine.load(url);
DockNode dn = new DockNode(browser); DockNode dn = new DockNode(browser);
dn.setTitle("ScriptLanguage Description"); dn.setTitle("ScriptLanguage Description");
//this.dockStation.getChildren().add(dn); //this.dockStation.getChildren().addCell(dn);
dn.dock(dockStation, DockPos.LEFT); dn.dock(dockStation, DockPos.LEFT);
} }
......
...@@ -77,7 +77,7 @@ public class Events { ...@@ -77,7 +77,7 @@ public class Events {
@RequiredArgsConstructor @RequiredArgsConstructor
/** /**
* Event that should be fired when a new goal node was created to inform view * Event that should be fired when a new goal node was created to inform view
* components s.t. they can update their view * components s.t. they can updateTarget their view
*/ */
public static class EventForNewGoalView { public static class EventForNewGoalView {
private final ASTNode correspodingASTNode; private final ASTNode correspodingASTNode;
......
...@@ -41,7 +41,7 @@ public class ASTNodeHiglightListener<T> { ...@@ -41,7 +41,7 @@ public class ASTNodeHiglightListener<T> {
if (currentInterpreter != null) deinstall(interpreter); if (currentInterpreter != null) deinstall(interpreter);
int i = interpreter.getEntryListeners().size(); int i = interpreter.getEntryListeners().size();
interpreter.getEntryListeners().add(0, list); interpreter.getEntryListeners().add(0, list);
// interpreter.getExitListeners().add(0, exitListener); // interpreter.getExitListeners().addCell(0, exitListener);
currentInterpreter = interpreter; currentInterpreter = interpreter;
} }
......
...@@ -143,7 +143,7 @@ public class InspectionView extends BorderPane { ...@@ -143,7 +143,7 @@ public class InspectionView extends BorderPane {
Mode.LIVING.name(), Mode.LIVING.name(),
Mode.POSTMORTEM.name() Mode.POSTMORTEM.name()
); );
getStyleClass().add(mode.get().name()); getStyleClass().addCell(mode.get().name());
}); });
*/ */
} }
......
...@@ -344,9 +344,9 @@ public class ProofTree extends BorderPane { ...@@ -344,9 +344,9 @@ public class ProofTree extends BorderPane {
/* if(!label.equals("Proof")) { /* if(!label.equals("Proof")) {
TreeItem<TreeNode> self = new TreeItem<>(new TreeNode(n.serialNr() + ": " + toString(n), n)); TreeItem<TreeNode> self = new TreeItem<>(new TreeNode(n.serialNr() + ": " + toString(n), n));
ti.getChildren().add(self); ti.getChildren().addCell(self);
}*/ }*/
// ti.getChildren().add(e); // ti.getChildren().addCell(e);
return ti; return ti;
...@@ -373,7 +373,7 @@ public class ProofTree extends BorderPane { ...@@ -373,7 +373,7 @@ public class ProofTree extends BorderPane {
TreeItem<TreeNode> populate = populate(childNode.getNodeInfo().getBranchLabel(), childNode); TreeItem<TreeNode> populate = populate(childNode.getNodeInfo().getBranchLabel(), childNode);
// TreeItem<TreeNode> self = new TreeItem<>(new TreeNode(childNode.serialNr() + ": " + toString(childNode), childNode)); // TreeItem<TreeNode> self = new TreeItem<>(new TreeNode(childNode.serialNr() + ": " + toString(childNode), childNode));
// populate.getChildren().add(0, self); // populate.getChildren().addCell(0, self);
ti.getChildren().add(populate); ti.getChildren().add(populate);
} else { } else {
...@@ -385,11 +385,11 @@ public class ProofTree extends BorderPane { ...@@ -385,11 +385,11 @@ public class ProofTree extends BorderPane {
} }
} }
/* node.childrenIterator().forEachRemaining(child -> ti.getChildren().add( /* node.childrenIterator().forEachRemaining(child -> ti.getChildren().addCell(
populate(child.getNodeInfo().getBranchLabel(), child))); populate(child.getNodeInfo().getBranchLabel(), child)));
*/ */
//node.children().forEach(child -> //node.children().forEach(child ->
// ti.getChildren().add(populate(child.getNodeInfo().getBranchLabel(), child))); // ti.getChildren().addCell(populate(child.getNodeInfo().getBranchLabel(), child)));
} }
return ti; return ti;
......
...@@ -337,13 +337,13 @@ public class ScriptArea extends BorderPane { ...@@ -337,13 +337,13 @@ public class ScriptArea extends BorderPane {
codeArea.setStyleSpans(0, codeArea.getStyleSpans(0, getExecutionMarkerPosition()).mapStyles(styleMapper)); codeArea.setStyleSpans(0, codeArea.getStyleSpans(0, getExecutionMarkerPosition()).mapStyles(styleMapper));
//this results in a NotSupportedOperation Exception because the add to an immutable list is not allowed //this results in a NotSupportedOperation Exception because the addCell to an immutable list is not allowed
/* getStyleSpans(0, getExecutionMarkerPosition()).forEach(span -> { /* getStyleSpans(0, getExecutionMarkerPosition()).forEach(span -> {
Collection<String> style = span.getStyle(); Collection<String> style = span.getStyle();
if (style.isEmpty()) { if (style.isEmpty()) {
setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA")); setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA"));
} else { } else {
style.add("NON_EXE_AREA"); style.addCell("NON_EXE_AREA");
} }
}); });
*/ */
......
...@@ -117,7 +117,7 @@ public class SequentMatcher extends BorderPane { ...@@ -117,7 +117,7 @@ public class SequentMatcher extends BorderPane {
services); services);
ObservableList<Map<String, MatchPath>> resultlist = FXCollections.observableArrayList(matchings); ObservableList<Map<String, MatchPath>> resultlist = FXCollections.observableArrayList(matchings);
//If no matchings found, add "No matchings found" //If no matchings found, addCell "No matchings found"
if (resultlist.isEmpty()) { if (resultlist.isEmpty()) {
matchingsView.setVisible(false); matchingsView.setVisible(false);
nomatchings.setVisible(true); nomatchings.setVisible(true);
......
...@@ -257,7 +257,7 @@ public class TacletContextMenu extends ContextMenu { ...@@ -257,7 +257,7 @@ public class TacletContextMenu extends ContextMenu {
// Items for insertion of hidden terms appear in a submenu. // Items for insertion of hidden terms appear in a submenu.
/*if (insertHiddenController.isResponsible(item)) { /*if (insertHiddenController.isResponsible(item)) {
insertHiddenController.add(item); insertHiddenController.addCell(item);
} else */ } else */
{ {
// If one of the sets contains the rule it is considered rare // If one of the sets contains the rule it is considered rare
...@@ -415,10 +415,10 @@ public class TacletContextMenu extends ContextMenu { ...@@ -415,10 +415,10 @@ public class TacletContextMenu extends ContextMenu {
String inputText) { String inputText) {
TextInputDialog dialog = new TextInputDialog(inputText); TextInputDialog dialog = new TextInputDialog(inputText);
// Get the Stage and add KeY Icon. // Get the Stage and addCell KeY Icon.
/* Stage stage = (Stage) dialog.getDialogPane().getScene().getWindow(); /* Stage stage = (Stage) dialog.getDialogPane().getScene().getWindow();
stage.getIcons() stage.getIcons()
.add(new Image(NUIConstants.KEY_APPLICATION_WINDOW_ICON_PATH)); .addCell(new Image(NUIConstants.KEY_APPLICATION_WINDOW_ICON_PATH));
dialog.setTitle("Abbreviation Dialog"); dialog.setTitle("Abbreviation Dialog");
dialog.setHeaderText(header); dialog.setHeaderText(header);
dialog.setContentText(message); dialog.setContentText(message);
......
...@@ -261,8 +261,8 @@ public class Utils { ...@@ -261,8 +261,8 @@ public class Utils {
GridPane expContent = new GridPane(); GridPane expContent = new GridPane();
expContent.setMaxWidth(Double.MAX_VALUE); expContent.setMaxWidth(Double.MAX_VALUE);
expContent.add(label, 0, 0); expContent.addCell(label, 0, 0);
expContent.add(textArea, 0, 1); expContent.addCell(textArea, 0, 1);
alert.getDialogPane().setExpandableContent(expContent); alert.getDialogPane().setExpandableContent(expContent);
*/ */
......
package edu.kit.iti.formal.psdbg.gui.graph;
import javafx.scene.Node;
import javafx.scene.control.Label;
import javafx.scene.input.DragEvent;
import javafx.scene.layout.Pane;
import javafx.scene.layout.VBox;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import lombok.Setter;
import java.util.Arrays;