diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java index 1ce0da08a67c9ef5e34d5c3483cdf97082eedfd9..cda241aa354ba9b7709dc06071f482d6e1356a1b 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java @@ -114,6 +114,7 @@ public class TransformAst implements ScriptLanguageVisitor { s.setSignature(sig); } s.setBody((Statements) ctx.body.accept(this)); + s.getBody().setParent(s); return s; } diff --git a/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java b/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java index fe3d2ad436ade2158a399586a20d0759d88a6caf..5ded9d2224b15427813444d7cdfaf4ab437e7239 100644 --- a/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java +++ b/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java @@ -98,13 +98,9 @@ public class MatcherFacadeTest { shouldMatch("1*j", "1 + ?Y", "[]"); shouldMatch("1*j", "1 * ?Y", "[{?Y=j}]"); + //does not match shouldMatch("1*j", "?Y * 1", "[{?Y=j}]"); - - //shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]); - //shouldMatch("f(a) ==> f(a), f(b)" , "f(a) ==> f(?X)", [{?X=a}]); - //shouldNotMatch("f(a) ==> f(a), f(b)" , "f(?X) ==> f(?X), f(a)"); - } @Test diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/StepIntoCommand.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/StepIntoCommand.java deleted file mode 100644 index 911693f6747dbe5c4e87f84245230b445067d19a..0000000000000000000000000000000000000000 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/StepIntoCommand.java +++ /dev/null @@ -1,16 +0,0 @@ -package edu.kit.iti.formal.psdbg; - -import edu.kit.iti.formal.psdbg.interpreter.dbg.*; - -public class StepIntoCommand extends DebuggerCommand { - @Override - public void execute(DebuggerFramework dbg) { - PTreeNode statePointer = dbg.getStatePointer(); - assert statePointer != null; - if (statePointer.isAtomic()) { - new StepOverCommand().execute(dbg); - } else { - dbg.releaseUntil(new Blocker.CounterBlocker(1)); - } - } -} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java index 0fdb9c37cdcd797dd50cd94e41d247d828ddc47e..b90c0816e4ded2bd7efd8b6f764d2974cb26ad02 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java @@ -1,6 +1,5 @@ package edu.kit.iti.formal.psdbg.interpreter; -import de.uka.ilkd.key.api.ProofApi; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.Term; @@ -163,10 +162,11 @@ public class KeYMatcher implements MatcherApi { private Value toValueTerm(KeyData currentState, Term matched) { String reprTerm = LogicPrinter.quickPrintTerm(matched, currentState.getEnv().getServices()); - + //Hack: to avoid newlines + String reprTermReformatted = reprTerm.trim(); return new Value<>( new TermType(new SortType(matched.sort())), - reprTerm + reprTermReformatted ); } diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java index d1a8edd1ba5fc5e521fae501ea932dc2203a74fc..1df5264e5f466f2d8ad0f4565760ef2e813e5d51 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java @@ -4,7 +4,6 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.macros.scripts.EngineState; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; -import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import edu.kit.iti.formal.psdbg.interpreter.Interpreter; @@ -15,10 +14,14 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import lombok.Getter; import lombok.RequiredArgsConstructor; +import org.apache.commons.io.IOUtils; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.key_project.util.collection.ImmutableList; +import java.io.IOException; +import java.net.URISyntaxException; +import java.net.URL; import java.util.Collection; import java.util.HashMap; import java.util.Iterator; @@ -61,7 +64,11 @@ public class ProofScriptCommandBuilder implements CommandHandler { GoalNode expandedNode = state.getSelectedGoalNode(); KeyData kd = expandedNode.getData(); Map map = new HashMap<>(); - params.asMap().forEach((k, v) -> map.put(k.getIdentifier(), v.getData().toString())); + params.asMap().forEach((k, v) -> { + System.out.println("v.getData().toString() = " + v.getData().toString()); + map.put(k.getIdentifier(), v.getData().toString()); + } + ); try { EngineState estate = new EngineState(kd.getProof()); estate.setGoal(kd.getNode()); @@ -100,6 +107,17 @@ public class ProofScriptCommandBuilder implements CommandHandler { @Override public String getHelp(CallStatement call) { ProofScriptCommand c = commands.get(call.getCommand()); + + URL res = getClass().getResource("/commands/" + call.getCommand() + ".html"); + try { + return IOUtils.toString(res.toURI(), "utf-8"); + } catch (NullPointerException | IOException | URISyntaxException e) { + return "No Help found for " + call.getCommand(); + + } + + /* + StringBuilder html = new StringBuilder(); @@ -150,5 +168,6 @@ public class ProofScriptCommandBuilder implements CommandHandler { html.append(""); return html.toString(); + */ } } diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/auto.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/auto.html new file mode 100644 index 0000000000000000000000000000000000000000..566549bdf8fae810809c1a81066000687cb338f6 --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/auto.html @@ -0,0 +1,10 @@ + + + + + Title + + + + + \ No newline at end of file diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java index ece8248a880ee25e75605d81b1b5c049dd48929e..f5c760a7f205c393537112aaebd5c045cac34564 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java @@ -161,10 +161,10 @@ public class Interpreter extends DefaultASTVisitor } private Value evaluate(GoalNode g, Expression expr) { - enterScope(expr); + //enterScope(expr); Evaluator evaluator = new Evaluator<>(g.getAssignments(), g); evaluator.setMatcher(matcherApi); - exitScope(expr); + //exitScope(expr); return evaluator.eval(expr); } diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java index e6ca416b7933570eabf6949ebfaacfa7249b481d..a6d102a7e876d44906fc52239f50f03b8872b4d5 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java @@ -134,7 +134,7 @@ public class DebuggerFramework { private void run() { try { interpreter.interpret(mainScript); - //dummyproofnode + ptreeManager.fireStatePointerChanged(); succeedListener.accept(this); } catch (Exception e) { error = e; diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java index 54976417a5df252798d3543191ce45d1e5735fc9..7fd6f6b09b8e289bcb3bc3b3ccd0e8185cfffd51 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java @@ -76,7 +76,7 @@ public class ProofTreeManager { int ctxLength = node.getContext().length; // We got a step deeper in the ASTNode stack. - // So we a caller + // So we have a caller if (getContextDepth() < ctxLength) { pushContext(); intoCurrentContext(node); diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoCommand.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoCommand.java new file mode 100644 index 0000000000000000000000000000000000000000..e3ff7deaa875083a143d7e2418d0977ace29cc98 --- /dev/null +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoCommand.java @@ -0,0 +1,20 @@ +package edu.kit.iti.formal.psdbg.interpreter.dbg; + +public class StepIntoCommand extends DebuggerCommand { + @Override + public void execute(DebuggerFramework dbg) { + PTreeNode statePointer = dbg.getStatePointer(); + assert statePointer != null; + if (statePointer.isAtomic()) { // atomic same as step over + new StepOverCommand().execute(dbg); + } else { + 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)); + } + } + } + } +} diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java index 9d86bab7e7a2f256151c308623b6432963c64d23..75676a3011357fb77c945a6b07f2af76ca29b318 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java @@ -1,20 +1,21 @@ package edu.kit.iti.formal.psdbg.interpreter.dbg; -import lombok.val; - public class StepIntoReverseCommand extends DebuggerCommand { @Override public void execute(DebuggerFramework dbg) throws DebuggerException { - val statePointer = dbg.getCurrentStatePointer(); - PTreeNode stepBack = statePointer.getStepInvInto() != null ? - statePointer.getStepInvInto() : - statePointer.getStepInvOver(); + PTreeNode statePointer = dbg.getStatePointer(); + assert statePointer != null; - if (stepBack == null) { - info("There is no previous state to the current one."); + if (statePointer.getStepInvInto() != null) { + dbg.setStatePointer(statePointer.getStepInvInto()); + } else { + if (statePointer.getStepInvOver() != null) { + PTreeNode statementBefore = statePointer.getStepInvOver(); + dbg.setStatePointer(statementBefore); + } else{ + dbg.setStatePointer(statePointer); + } } - dbg.setStatePointer(stepBack); - } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ContractChooser.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ContractChooser.java index 0002554714860cd323ff3140ef67036c4d889b97..c6dd7ecad85115a6358d1eb56f65fe369b4a6fc1 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ContractChooser.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ContractChooser.java @@ -114,7 +114,7 @@ public class ContractChooser extends Dialog { text.getChildren().add(contract); text.getChildren().add(name); text.getChildren().add(new Text("\n")); - //text.getChildren().add(tcontent); + //text.getChildren().addCell(tcontent); for (String line : content.split("\n")) { if (line.contains(":")) { 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 89536b76d5e8f9201a35ca9a855049656132183f..7d03b0c5c00d7b113fdfa5faac54f4a66e5c99ff 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 @@ -15,11 +15,12 @@ import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.speclang.Contract; import edu.kit.iti.formal.psdbg.ShortCommandPrinter; -import edu.kit.iti.formal.psdbg.StepIntoCommand; import edu.kit.iti.formal.psdbg.examples.Examples; import edu.kit.iti.formal.psdbg.fmt.DefaultFormatter; import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger; 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.InspectionModel; import edu.kit.iti.formal.psdbg.gui.model.InterpreterThreadState; @@ -28,6 +29,7 @@ import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade; import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; +import edu.kit.iti.formal.psdbg.interpreter.data.State; import edu.kit.iti.formal.psdbg.interpreter.dbg.*; import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; import javafx.application.Platform; @@ -88,76 +90,53 @@ public class DebuggerMain implements Initializable { @Getter 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 ScriptController scriptController; - @FXML private DebuggerStatusBar statusBar; - @FXML private DockPane dockStation; - @FXML private ToggleButton togBtnCommandHelp; - @FXML private ToggleButton togBtnProofTree; - @FXML private ToggleButton togBtnActiveInspector; - @FXML private ToggleButton togBtnWelcome; - @FXML private ToggleButton togBtnCodeDock; - @FXML private CheckMenuItem miCommandHelp; - @FXML private CheckMenuItem miCodeDock; - @FXML private CheckMenuItem miWelcomeDock; - @FXML private CheckMenuItem miActiveInspector; - @FXML private CheckMenuItem miProofTree; - @FXML private ToggleButton btnInteractiveMode; - private JavaArea javaArea = new JavaArea(); - private DockNode javaAreaDock = new DockNode(javaArea, "Java Source", new MaterialDesignIconView(MaterialDesignIcon.CODEPEN) ); - //----------------------------------------------------------------------------------------------------------------- private ProofTree proofTree = new ProofTree(); - private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree"); - private WelcomePane welcomePane = new WelcomePane(this); - private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT)); - private DockNode activeInspectorDock; - private CommandHelp commandHelp = new CommandHelp(); - private DockNode commandHelpDock = new DockNode(commandHelp, "DebuggerCommand Help"); - private InteractiveModeController interactiveModeController; - @FXML private Menu examplesMenu; - private Timer interpreterThreadTimer; @Subscribe @@ -303,6 +282,8 @@ public class DebuggerMain implements Initializable { * @see {@link #handleStatePointer(PTreeNode)} */ private void handleStatePointerUI(PTreeNode node) { + graph.addPartiallyAndMark(node); + if (node != null) { getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt()); scriptController.getDebugPositionHighlighter().highlight(node.getStatement()); @@ -326,7 +307,7 @@ public class DebuggerMain implements Initializable { showCodeDock(null); }); - //add listener for linehighlighting when changing selection in inspectionview + //addCell listener for linehighlighting when changing selection in inspectionview getInspectionViewsController().getActiveInspectionViewTab().getModel().highlightedJavaLinesProperty(). addListener((observable, oldValue, newValue) -> { if (newValue != null) { @@ -346,6 +327,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() { return FACADE; } @@ -365,19 +359,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) { if (!javaAreaDock.isDocked()) { javaAreaDock.dock(dockStation, DockPos.RIGHT); @@ -474,7 +455,6 @@ public class DebuggerMain implements Initializable { } } - /** * Execute the script that with using the interpreter that is build using the interpreterbuilder * @@ -527,20 +507,54 @@ public class DebuggerMain implements Initializable { btnInteractiveMode.setDisable(false); assert model.getDebuggerFramework() != null; btnInteractiveMode.setSelected(true); - /*PTreeNode statePointer = model.getDebuggerFramework().getStatePointer(); + PTreeNode statePointer = model.getDebuggerFramework().getStatePointer(); assert statePointer!=null; State lastState = statePointer.getStateAfterStmt(); getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState); - */ + }); } + @FXML + public void debugGraph(ActionEvent event) { + if (!graphViewNode.isDocked() && !graphViewNode.isFloating()) { + graphViewNode.dock(dockStation, DockPos.CENTER); + } + + graph.clear(true); + + for (PTreeNode n : model.getDebuggerFramework().getStates()) { + graph.addCell(n); + } + + for (PTreeNode 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 public void debugPrintDot(@Nullable ActionEvent ae) { if (model.getDebuggerFramework() == null) { statusBar.publishErrorMessage("can print debug info, no debugger started!"); return; } + + debugGraph(ae); + try (PrintWriter out = new PrintWriter(new FileWriter("debug.dot"))) { out.println("digraph G {"); for (PTreeNode n : model.getDebuggerFramework().getStates()) { @@ -729,6 +743,7 @@ public class DebuggerMain implements Initializable { /** * Reload a problem from the beginning + * * @param event */ @FXML @@ -765,6 +780,7 @@ public class DebuggerMain implements Initializable { } + @FXML public void closeProgram() { System.exit(0); @@ -893,7 +909,7 @@ public class DebuggerMain implements Initializable { * @param actionEvent */ public void stepInto(ActionEvent actionEvent) { - LOGGER.debug("DebuggerMain.stepOver"); + LOGGER.debug("DebuggerMain.stepInto"); try { if (model.getDebuggerFramework().getStatePointer().isAtomic()) { model.getDebuggerFramework().getStatePointerListener() @@ -914,8 +930,10 @@ public class DebuggerMain implements Initializable { /** * Perform a step back * Does stepinto back + * * @param actionEvent */ + @Deprecated public void stepBack(ActionEvent actionEvent) { LOGGER.debug("DebuggerMain.stepBack"); try { @@ -938,13 +956,26 @@ public class DebuggerMain implements Initializable { public void stepIntoReverse(ActionEvent actionEvent) { - LOGGER.debug("DebuggerMain.stepOverReverse"); + LOGGER.debug("DebuggerMain.stepIntoReverser"); try { + if (model.getDebuggerFramework().getStatePointer().isAtomic()) { + model.getDebuggerFramework().getStatePointerListener() + .add(new StepIntoReverseHandler(model.getStatePointer())); + } model.getDebuggerFramework().execute(new StepIntoReverseCommand<>()); } catch (DebuggerException e) { Utils.showExceptionDialog("", "", "", e); LOGGER.error(e); } + + +/* LOGGER.debug("DebuggerMain.stepOverReverse"); + try { + model.getDebuggerFramework().execute(new StepIntoReverseCommand<>()); + } catch (DebuggerException e) { + Utils.showExceptionDialog("", "", "", e); + LOGGER.error(e); + }*/ } public void stopDebugMode(ActionEvent actionEvent) { @@ -1048,7 +1079,7 @@ public class DebuggerMain implements Initializable { webEngine.load(url); DockNode dn = new DockNode(browser); dn.setTitle("ScriptLanguage Description"); - //this.dockStation.getChildren().add(dn); + //this.dockStation.getChildren().addCell(dn); dn.dock(dockStation, DockPos.LEFT); } @@ -1182,6 +1213,64 @@ public class DebuggerMain implements Initializable { node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea())); } } + + @RequiredArgsConstructor + private class StepIntoReverseHandler implements java.util.function.Consumer> { + private final PTreeNode original; + + @Override + public void accept(PTreeNode keyDataPTreeNode) { + Platform.runLater(this::acceptUI); + } + + public void acceptUI() { + model.getDebuggerFramework().getStatePointerListener().remove(this); + PTreeNode stepInvOver = model.getDebuggerFramework().getStatePointer(); + GoalNode beforeNode = stepInvOver.getStateBeforeStmt().getSelectedGoalNode(); + List> stateAfterStmt = stepInvOver.getStateAfterStmt().getGoals(); + + ProofTree ptree = new ProofTree(); + Proof proof = beforeNode.getData().getProof(); + + Node pnode = beforeNode.getData().getNode(); + // stateAfterStmt.forEach(keyDataGoalNode -> System.out.println("keyDataGoalNode.getData().getNode().serialNr() = " + keyDataGoalNode.getData().getNode().serialNr())); + + ptree.setProof(proof); + ptree.setRoot(pnode); + ptree.addNodeColor(pnode, "blueviolet"); + ptree.setDeactivateRefresh(true); + + if (stateAfterStmt.size() > 0) { + Set sentinels = proof.getSubtreeGoals(pnode) + .stream() + .map(Goal::node) + .collect(Collectors.toSet()); + ptree.getSentinels().addAll(sentinels); + sentinels.forEach(node -> ptree.addNodeColor(node, "blueviolet")); + } else { + Set sentinels = new HashSet<>(); + Iterator nodeIterator = beforeNode.getData().getNode().leavesIterator(); + while (nodeIterator.hasNext()) { + Node next = nodeIterator.next(); + + sentinels.add(next); + } + ptree.getSentinels().addAll(sentinels); + sentinels.forEach(node -> ptree.addNodeColor(node, "blueviolet")); + //traverseProofTreeAndAddSentinelsToLeaves(); + } + + + ptree.expandRootToSentinels(); + DockNode node = new DockNode(ptree, "Proof Tree for Step Inverse Into: " + + original.getStatement().accept(new ShortCommandPrinter()) + ); + + node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea())); + + } + } + //endregion } //deprecated diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/Events.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/Events.java index 701d5c5ff81578ec5d17d6630888552140789e6c..06c600a603b6d22037a8dab73f58f4cdbe79c18b 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/Events.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/Events.java @@ -77,7 +77,7 @@ public class Events { @RequiredArgsConstructor /** * 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 { private final ASTNode correspodingASTNode; diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ASTNodeHiglightListener.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ASTNodeHiglightListener.java index 6145311b54b6d603427639e3535627bd09e25734..31adf28b09490d0805db268499151d060b019b71 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ASTNodeHiglightListener.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ASTNodeHiglightListener.java @@ -41,7 +41,7 @@ public class ASTNodeHiglightListener { if (currentInterpreter != null) deinstall(interpreter); int i = interpreter.getEntryListeners().size(); interpreter.getEntryListeners().add(0, list); - // interpreter.getExitListeners().add(0, exitListener); + // interpreter.getExitListeners().addCell(0, exitListener); currentInterpreter = interpreter; } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java index 3860976eed37ef0c13808865510198310d0a0f36..4440e74a7935d8c76a6354ce0aff8b4926e4fc8b 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java @@ -143,7 +143,7 @@ public class InspectionView extends BorderPane { Mode.LIVING.name(), Mode.POSTMORTEM.name() ); - getStyleClass().add(mode.get().name()); + getStyleClass().addCell(mode.get().name()); }); */ } 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 d06c0ae8744231ead944ddd241f93743b002d6d0..53fec8a3b7ec789f6fe72fc9a672956b2cc8b9a7 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 @@ -344,9 +344,9 @@ public class ProofTree extends BorderPane { /* if(!label.equals("Proof")) { TreeItem 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; @@ -373,7 +373,7 @@ public class ProofTree extends BorderPane { TreeItem populate = populate(childNode.getNodeInfo().getBranchLabel(), childNode); // TreeItem self = new TreeItem<>(new TreeNode(childNode.serialNr() + ": " + toString(childNode), childNode)); - // populate.getChildren().add(0, self); + // populate.getChildren().addCell(0, self); ti.getChildren().add(populate); } else { @@ -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))); */ //node.children().forEach(child -> - // ti.getChildren().add(populate(child.getNodeInfo().getBranchLabel(), child))); + // ti.getChildren().addCell(populate(child.getNodeInfo().getBranchLabel(), child))); } return ti; diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java index 2cfb3c9bfe318b5ced3c914d6b59e50ef2d1080d..1d3c647a2b4570663820532024e1594b57f3d354 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java @@ -337,13 +337,13 @@ public class ScriptArea extends BorderPane { 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 -> { Collection style = span.getStyle(); if (style.isEmpty()) { setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA")); } else { - style.add("NON_EXE_AREA"); + style.addCell("NON_EXE_AREA"); } }); */ diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java index 7acfc21286e9bbf783b859f42119cb1cc86d9c69..3b5e587510944d72e47fa7c53d8e178eefd93626 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java @@ -117,7 +117,7 @@ public class SequentMatcher extends BorderPane { services); ObservableList> resultlist = FXCollections.observableArrayList(matchings); - //If no matchings found, add "No matchings found" + //If no matchings found, addCell "No matchings found" if (resultlist.isEmpty()) { matchingsView.setVisible(false); nomatchings.setVisible(true); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java index a12348b1e7c369615797c309edcfd42e0691efc1..f5fe8d287553f63fe744f5696181d1d4f7c067c5 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java @@ -154,7 +154,7 @@ public class SequentView extends CodeArea { insertText(0, backend.getString()); if (node.get().isClosed()) { this.setBorder(new Border(new BorderStroke(Color.GREEN, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT))); - this.getStyleClass().add("closed-sequent-view"); + // 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"); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java index 7b3aac4193a2d0efa43dc841a83204112673601b..3b2e382e3af950414f2925bbfca560ec9b07b272 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java @@ -257,7 +257,7 @@ public class TacletContextMenu extends ContextMenu { // Items for insertion of hidden terms appear in a submenu. /*if (insertHiddenController.isResponsible(item)) { - insertHiddenController.add(item); + insertHiddenController.addCell(item); } else */ { // If one of the sets contains the rule it is considered rare @@ -415,10 +415,10 @@ public class TacletContextMenu extends ContextMenu { String 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.getIcons() - .add(new Image(NUIConstants.KEY_APPLICATION_WINDOW_ICON_PATH)); + .addCell(new Image(NUIConstants.KEY_APPLICATION_WINDOW_ICON_PATH)); dialog.setTitle("Abbreviation Dialog"); dialog.setHeaderText(header); dialog.setContentText(message); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java index 0c31a2cfa94c27f27e9a0b936e661997ad79bfd1..736e39c4c76ab8980afe7a71a30a419b4a306d23 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java @@ -261,8 +261,8 @@ public class Utils { GridPane expContent = new GridPane(); expContent.setMaxWidth(Double.MAX_VALUE); - expContent.add(label, 0, 0); - expContent.add(textArea, 0, 1); + expContent.addCell(label, 0, 0); + expContent.addCell(textArea, 0, 1); alert.getDialogPane().setExpandableContent(expContent); */ diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Cell.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Cell.java new file mode 100644 index 0000000000000000000000000000000000000000..a0d1c9553628eff2c9c59c18049d990b2d79f194 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Cell.java @@ -0,0 +1,65 @@ +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; + +@RequiredArgsConstructor +public class Cell extends Pane { + @Getter + private final T cellId; + + /** + * if true, this cell is handled by the layouter. + */ + @Getter + @Setter + private boolean invalid = true; + + private Dragger dragger = new Dragger(this); + + public Cell(T cellId, Node... children) { + super(children); + getStyleClass().add("graph-cell"); + this.cellId = cellId; + } + + public Cell(T cellId, String... children) { + getStyleClass().add("graph-cell"); + this.cellId = cellId; + VBox hbox = new VBox(); + hbox.getStyleClass().add("vbox"); + getChildren().addAll(hbox); + Arrays.stream(children).forEachOrdered(s -> hbox.getChildren().add(new Label(s))); + } +} + +class Dragger { + private double mouseX; + private double mouseY; + + public Dragger(Node node) { + assert node != null; + node.setOnMousePressed(event -> { + mouseX = event.getSceneX(); + mouseY = event.getSceneY(); + }); + + node.setOnMouseDragged(event -> { + double deltaX = event.getSceneX() - mouseX; + double deltaY = event.getSceneY() - mouseY; + node.relocate(node.getLayoutX() + deltaX, node.getLayoutY() + deltaY); + mouseX = event.getSceneX(); + mouseY = event.getSceneY(); + }); + } +} + + diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/CellLayer.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/CellLayer.java new file mode 100644 index 0000000000000000000000000000000000000000..6c5aa2e714757b372f0cfa901f4b8470224b3ca4 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/CellLayer.java @@ -0,0 +1,7 @@ +package edu.kit.iti.formal.psdbg.gui.graph; + +import javafx.scene.layout.Pane; + +public class CellLayer extends Pane { + +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Edge.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Edge.java new file mode 100644 index 0000000000000000000000000000000000000000..6aabf7c4e38d8b110ef4084cd215e2ff89b4d58a --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Edge.java @@ -0,0 +1,144 @@ +package edu.kit.iti.formal.psdbg.gui.graph; + +import javafx.beans.Observable; +import javafx.beans.property.SimpleObjectProperty; +import javafx.beans.value.ObservableValue; +import javafx.geometry.Point2D; +import javafx.scene.Group; +import javafx.scene.control.Label; +import javafx.scene.paint.Paint; +import javafx.scene.shape.*; + +import java.util.Random; + +public class Edge extends Group { + private static Random r = new Random(); + protected SimpleObjectProperty> source = new SimpleObjectProperty<>(), target = new SimpleObjectProperty<>(); + private Line line = new Line(); + private Label label = new Label(); + private Circle circle = new Circle(); + private double shiftX, shiftY; + + public Edge(Cell source, Cell target, String label) { + setSource(source); + setTarget(target); + + shiftX = r.nextInt(50) - 25; + shiftY = r.nextInt(50) - 25; + + line = new Line(); + line.getStyleClass().addAll("edge", label); + circle.getStyleClass().addAll("edge", label); + this.label.getStyleClass().addAll("edge-label", label); + this.label.setText(label); + this.source.addListener(this::renewNode); + this.target.addListener(this::renewNode); + + + renewNode(this.source, null, source); + renewNode(this.target, null, target); + + getChildren().addAll(line, this.label, circle); + redraw(); + } + + private void renewNode(ObservableValue observableValue, Cell old, Cell nValue) { + if (old != null) { + old.layoutBoundsProperty().removeListener(this::redraw); + old.layoutXProperty().removeListener(this::redraw); + old.layoutYProperty().removeListener(this::redraw); + } + if (nValue != null) { + nValue.layoutBoundsProperty().addListener(this::redraw); + nValue.layoutXProperty().addListener(this::redraw); + nValue.layoutYProperty().addListener(this::redraw); + } + redraw(); + } + + void redraw() { + redraw(null); + } + + void redraw(Observable observable) { + double x1, y1, x2, y2; + if (getSource() == null || getTarget() == null) { + x1 = y1 = x2 = y2 = 0; + } else { + + x1 = getSource().getLayoutX() + getSource().getBoundsInParent().getWidth() / 2.0; + x2 = getTarget().getLayoutX() + getTarget().getBoundsInParent().getWidth() / 2.0; + + y1 = getSource().getLayoutY() + getSource().getBoundsInParent().getHeight() / 2.0; + y2 = getTarget().getLayoutY() + getTarget().getBoundsInParent().getHeight() / 2.0; + + } + + Point2D start = new Point2D(x1, y1); + Point2D end = new Point2D(x2, y2); + + Point2D midpoint = start.midpoint(end); + + label.relocate(midpoint.getX() + shiftX, shiftY + midpoint.getY()); + + line.setStartX(x1); + line.setStartY(y1); + line.setEndX(x2); + line.setEndY(y2); + + circle.setCenterX(x2); + circle.setCenterY(y2); + circle.setRadius(15); + + if (getTarget() != null) { + end = correctToRectangle(getTarget().getLayoutX(), + getTarget().getLayoutY(), getTarget().getWidth(), getTarget().getHeight()); + if (end != null) { + circle.setCenterX(end.getX()); + circle.setCenterY(end.getY()); + + line.setEndX(end.getX()); + line.setEndY(end.getY()); + } + } + } + + private Point2D correctToRectangle(double x, double y, double width, double height) { + Rectangle r = new Rectangle(x, y, width, height); + r.setStroke(Paint.valueOf("black")); + r.setStrokeWidth(1); + r.setFill(null); + try { + Path inter = (Path) Shape.intersect(line, r); + MoveTo mt = (MoveTo) inter.getElements().get(0); + return new Point2D(mt.getX(), mt.getY()); + } catch (ClassCastException | IndexOutOfBoundsException cce) { + //cce.printStackTrace(); + } + return null; + } + + public Cell getSource() { + return source.get(); + } + + public void setSource(Cell source) { + this.source.set(source); + } + + public SimpleObjectProperty> sourceProperty() { + return source; + } + + public Cell getTarget() { + return target.get(); + } + + public void setTarget(Cell target) { + this.target.set(target); + } + + public SimpleObjectProperty> targetProperty() { + return target; + } +} \ No newline at end of file diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Graph.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Graph.java new file mode 100644 index 0000000000000000000000000000000000000000..c7d433f4c6e60e6904ce080ccb271eb070f4caf7 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Graph.java @@ -0,0 +1,100 @@ +package edu.kit.iti.formal.psdbg.gui.graph; + +import edu.kit.iti.formal.psdbg.ShortCommandPrinter; +import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; +import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode; +import javafx.beans.property.SimpleListProperty; +import javafx.collections.FXCollections; +import javafx.collections.ObservableList; + +import java.util.HashMap; + +public class Graph { + final private SimpleListProperty> nodes = new SimpleListProperty<>(FXCollections.observableArrayList()); + private final SimpleListProperty> edges = new SimpleListProperty<>(FXCollections.observableArrayList()); + protected HashMap> map = new HashMap<>(); + + public ObservableList> getNodes() { + return nodes.get(); + } + + public void setNodes(ObservableList> nodes) { + this.nodes.set(nodes); + } + + public SimpleListProperty> nodesProperty() { + return nodes; + } + + public ObservableList> getEdges() { + return edges.get(); + } + + public void setEdges(ObservableList> edges) { + this.edges.set(edges); + } + + public SimpleListProperty> edgesProperty() { + return edges; + } + + public void clear(boolean clearMap) { + getEdges().clear(); + getNodes().clear(); + if (clearMap) map.clear(); + } + + public Cell getCell(T cellId) { + return map.get(cellId); + } + + + public static class PTreeGraph extends Graph> { + private Cell lastHighlightedCell; + + public Cell> addCell(PTreeNode n) { + if (map.containsKey(n)) { + return map.get(n); + } + Cell> cell = new Cell<>(n, + (String) n.getStatement().accept(new ShortCommandPrinter()), + "Line #" + n.getStatement().getStartPosition().getLineNumber(), + n.getStateBeforeStmt().getGoals().size() + "# goals" + ); + map.put(n, cell); + getNodes().add(cell); + return cell; + } + + public void addEdge(PTreeNode from, PTreeNode to, String label) { + Edge edge = new Edge(map.get(from), map.get(to), label); + getEdges().add(edge); + } + + public void addPartiallyAndMark(PTreeNode node) { + Cell cell = addCell(node); + + if (node.getStepOver() != null) { + addEdge(node, node.getStepOver(), "over"); + } + if (node.getStepInto() != null) { + addEdge(node, node.getStepInto(), "into"); + } + if (node.getStepInvOver() != null) { + addEdge(node, node.getStepInvOver(), "revo"); + } + if (node.getStepInvInto() != null) { + addEdge(node, node.getStepInvInto(), "otni"); + } + if (node.getStepReturn() != null) { + addEdge(node, node.getStepReturn(), "rtrn"); + } + + if (lastHighlightedCell != null) { + lastHighlightedCell.getStyleClass().remove("current-node"); + } + cell.getStyleClass().add("current-node"); + lastHighlightedCell = cell; + } + } +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/GraphView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/GraphView.java new file mode 100644 index 0000000000000000000000000000000000000000..65eca0cff58bc5093a778a20c8c089f43e644390 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/GraphView.java @@ -0,0 +1,76 @@ +package edu.kit.iti.formal.psdbg.gui.graph; + +import javafx.collections.ListChangeListener; +import javafx.collections.ObservableList; +import javafx.scene.Group; +import javafx.scene.control.ScrollPane; +import javafx.scene.layout.BorderPane; +import javafx.scene.layout.Pane; +import javafx.scene.layout.StackPane; + +/** + * @author Alexander Weigl + * @version 1 (17.01.18) + */ +public class GraphView extends BorderPane { + private Graph.PTreeGraph graph = new Graph.PTreeGraph(); + private Group canvas = new Group(); + //private ZoomableScrollPane scrollPane; + private MouseGestures mouseGestures; + + private Pane cellLayer = new Pane(); + private Pane edgeLayer = new Pane(); + private ScrollPane scrollPane = new ScrollPane(); + + + public GraphView() { + setCenter(scrollPane); + StackPane root = new StackPane(); + root.getStyleClass().add("graph"); + scrollPane.setContent(root); + root.getChildren().addAll(edgeLayer, cellLayer); + //canvas.getChildren().addCell(cellLayer); + mouseGestures = new MouseGestures(); + /*scrollPane = new ZoomableScrollPane(this); + scrollPane.setFitToWidth(true); + scrollPane.setFitToHeight(true);*/ + + edgeLayer.minWidthProperty().bind(scrollPane.widthProperty()); + edgeLayer.minHeightProperty().bind(scrollPane.heightProperty()); + cellLayer.minWidthProperty().bind(scrollPane.widthProperty()); + cellLayer.minHeightProperty().bind(scrollPane.heightProperty()); + + graph.getEdges().addListener((ListChangeListener) c -> { + while (c.next()) { + if (c.wasRemoved()) + edgeLayer.getChildren().removeAll(c.getRemoved()); + if (c.wasAdded()) + edgeLayer.getChildren().addAll(c.getAddedSubList()); + } + redraw(); + }); + + graph.getNodes().addListener((ListChangeListener) c -> { + while (c.next()) { + if (c.wasRemoved()) + cellLayer.getChildren().removeAll(c.getRemoved()); + if (c.wasAdded()) + cellLayer.getChildren().addAll(c.getAddedSubList()); + } + redraw(); + }); + + redraw(); + } + + public void redraw() { + //Layout layout = new RandomLayout(graph.getNodes()); + Layout layout = new HierarchicalLayout(graph); + layout.execute(); + graph.getEdges().forEach(Edge::redraw); + } + + public Graph.PTreeGraph getGraph() { + return graph; + } +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/HierarchicalLayout.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/HierarchicalLayout.java new file mode 100644 index 0000000000000000000000000000000000000000..6036bf84b6a9061292f2399c206e222ccebb6cff --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/HierarchicalLayout.java @@ -0,0 +1,68 @@ +package edu.kit.iti.formal.psdbg.gui.graph; + +import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; +import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode; +import lombok.RequiredArgsConstructor; + +import java.util.HashSet; +import java.util.Optional; +import java.util.Set; + +/** + * @author Alexander Weigl + * @version 1 (18.01.18) + */ +@RequiredArgsConstructor +public class HierarchicalLayout extends Layout { + public static final double MARGIN_TOP = 50.0; + public static final double MARGIN_LEFT = 50.0; + + private final Graph> graph; + double y = MARGIN_TOP; + double py = MARGIN_TOP; + + @Override + public void execute() { + Optional>> root = findRoot(); + if (!root.isPresent()) { + return; + } + int level = 0; + explore(root.get(), MARGIN_LEFT); + } + + private void explore(Cell> cell, double px) { + if (cell == null) + return; + double x = px; + double y = py + MARGIN_TOP; + py += MARGIN_TOP; + if (cell.isInvalid()) { + cell.relocate(x, y); + } else { + x = cell.getLayoutX(); + py = cell.getLayoutY(); + } + cell.setInvalid(false); + py += MARGIN_TOP; + + if (cell.getCellId().getStepInto() != null) { + explore(graph.getCell(cell.getCellId().getStepInto()), x + MARGIN_LEFT); + } + + if (cell.getCellId().getStepOver() != null) { + explore(graph.getCell(cell.getCellId().getStepOver()), x); + } + } + + private Optional>> findRoot() { + Set>> cells = new HashSet<>(graph.getNodes()); + graph.getEdges().forEach( + edge -> cells.remove(edge.getTarget()) + ); + if (cells.size() != 1) { + return Optional.empty(); + } + return Optional.of(cells.iterator().next()); + } +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Layout.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Layout.java new file mode 100644 index 0000000000000000000000000000000000000000..b2a461f79e1192443d76dd9e3958599411e773c4 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Layout.java @@ -0,0 +1,5 @@ +package edu.kit.iti.formal.psdbg.gui.graph; + +public abstract class Layout { + public abstract void execute(); +} \ No newline at end of file diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/MouseGestures.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/MouseGestures.java new file mode 100644 index 0000000000000000000000000000000000000000..91e5c200ac903c88501f062c5fbafc0cf48e3d4d --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/MouseGestures.java @@ -0,0 +1,51 @@ +package edu.kit.iti.formal.psdbg.gui.graph; + +import javafx.event.EventHandler; +import javafx.scene.Node; +import javafx.scene.input.MouseEvent; +import lombok.*; + +public class MouseGestures { + private final DragContext dragContext = new DragContext(); + private final EventHandler onMousePressedEventHandler = this::onPress; + private final EventHandler onMouseDraggedEventHandler = this::onDrag; + private final EventHandler onMouseReleasedEventHandler = this::onRelease; + + @Setter + @Getter + private double scale = 1; + + public void onRelease(MouseEvent event) { + + } + + private void onPress(MouseEvent event) { + Node node = (Node) event.getSource(); + dragContext.x = node.getBoundsInParent().getMinX() * scale - event.getScreenX(); + dragContext.y = node.getBoundsInParent().getMinY() * scale - event.getScreenY(); + } + private void onDrag(MouseEvent event) { + Node node = (Node) event.getSource(); + + double offsetX = event.getScreenX() + dragContext.x; + double offsetY = event.getScreenY() + dragContext.y; + + offsetX /= scale; + offsetY /= scale; + + node.relocate(offsetX, offsetY); + + } + + public void makeDraggable(final Node node) { + node.setOnMousePressed(onMousePressedEventHandler); + node.setOnMouseDragged(onMouseDraggedEventHandler); + node.setOnMouseReleased(onMouseReleasedEventHandler); + + } + + static class DragContext { + private double x; + private double y; + } +} \ No newline at end of file diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/RandomLayout.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/RandomLayout.java new file mode 100644 index 0000000000000000000000000000000000000000..eb094e68694f6225b25360b5b3ee691fd650f1a1 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/RandomLayout.java @@ -0,0 +1,29 @@ +package edu.kit.iti.formal.psdbg.gui.graph; + +import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; +import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode; +import javafx.collections.ObservableList; + +import java.util.ArrayList; +import java.util.List; +import java.util.Random; + +public class RandomLayout extends Layout { + private final List cells = new ArrayList<>(); + private Random rnd = new Random(); + + public RandomLayout(List> cells) { + this.cells.addAll(cells); + } + + public void execute() { + for (Cell cell : cells) { + if (cell.isInvalid()) { + double x = rnd.nextDouble() * 1000; + double y = rnd.nextDouble() * 1000; + cell.relocate(x, y); + } + cell.setInvalid(false); + } + } +} \ No newline at end of file diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/RectangleCell.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/RectangleCell.java new file mode 100644 index 0000000000000000000000000000000000000000..048ecc4672a433e25379594a7073c4a897c9af75 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/RectangleCell.java @@ -0,0 +1,19 @@ +package edu.kit.iti.formal.psdbg.gui.graph; + +import javafx.scene.paint.Color; +import javafx.scene.shape.Rectangle; + +/** + * @author Alexander Weigl + * @version 1 (17.01.18) + */ +public class RectangleCell extends Cell { + + public RectangleCell(String id) { + super(id); + Rectangle view = new Rectangle(50, 50); + view.setStroke(Color.DODGERBLUE); + view.setFill(Color.DODGERBLUE); + getChildren().add(view); + } +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/ZoomableScrollPane.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/ZoomableScrollPane.java new file mode 100644 index 0000000000000000000000000000000000000000..c6d75dd476d1a9a9329ddf500b0ffe7c9b917920 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/ZoomableScrollPane.java @@ -0,0 +1,127 @@ +package edu.kit.iti.formal.psdbg.gui.graph; + +import javafx.event.EventHandler; +import javafx.scene.Group; +import javafx.scene.Node; +import javafx.scene.control.ScrollPane; +import javafx.scene.input.ScrollEvent; +import javafx.scene.transform.Scale; + +public class ZoomableScrollPane extends ScrollPane { + private Group zoomGroup; + private Scale scaleTransform; + private Node content; + private double scaleValue = 1.0; + private double delta = 0.1; + + public ZoomableScrollPane(Node content) { + this.content = content; + Group contentGroup = new Group(); + zoomGroup = new Group(); + contentGroup.getChildren().add(zoomGroup); + zoomGroup.getChildren().add(content); + setContent(contentGroup); + scaleTransform = new Scale(scaleValue, scaleValue, 0, 0); + zoomGroup.getTransforms().add(scaleTransform); + + zoomGroup.setOnScroll(new ZoomHandler()); + } + + public double getScaleValue() { + return scaleValue; + } + + public void zoomToActual() { + zoomTo(1.0); + } + + public void zoomTo(double scaleValue) { + + this.scaleValue = scaleValue; + + scaleTransform.setX(scaleValue); + scaleTransform.setY(scaleValue); + + } + + public void zoomActual() { + + scaleValue = 1; + zoomTo(scaleValue); + + } + + public void zoomOut() { + scaleValue -= delta; + + if (Double.compare(scaleValue, 0.1) < 0) { + scaleValue = 0.1; + } + + zoomTo(scaleValue); + } + + public void zoomIn() { + + scaleValue += delta; + + if (Double.compare(scaleValue, 10) > 0) { + scaleValue = 10; + } + + zoomTo(scaleValue); + + } + + /** + * @param minimizeOnly If the content fits already into the viewport, then we don't + * zoom if this parameter is true. + */ + public void zoomToFit(boolean minimizeOnly) { + + double scaleX = getViewportBounds().getWidth() / getContent().getBoundsInLocal().getWidth(); + double scaleY = getViewportBounds().getHeight() / getContent().getBoundsInLocal().getHeight(); + + // consider current scale (in content calculation) + scaleX *= scaleValue; + scaleY *= scaleValue; + + // distorted zoom: we don't want it => we search the minimum scale + // factor and apply it + double scale = Math.min(scaleX, scaleY); + + // check precondition + if (minimizeOnly) { + + // check if zoom factor would be an enlargement and if so, just set + // it to 1 + if (Double.compare(scale, 1) > 0) { + scale = 1; + } + } + + // apply zoom + zoomTo(scale); + + } + + private class ZoomHandler implements EventHandler { + + @Override + public void handle(ScrollEvent scrollEvent) { + // if (scrollEvent.isControlDown()) + { + + if (scrollEvent.getDeltaY() < 0) { + scaleValue -= delta; + } else { + scaleValue += delta; + } + + zoomTo(scaleValue); + + scrollEvent.consume(); + } + } + } +} \ No newline at end of file diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less index 71dc82000d462b4ff5339e4a489afcdb9a032cf1..e2771c26b693f908fdcc3cb59b96f1c459a261fe 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less @@ -42,7 +42,6 @@ } - .EXE_MARKER { -fx-fill: @violet; -fx-border-color: red; @@ -135,7 +134,6 @@ -fx-font-size: 9pt; } - .java-area { -fx-background-color: @basenavy; // -fx-background-color: @base3; @@ -144,7 +142,6 @@ //-fx-font-size: 18pt; -fx-fill: @base01; - .ABSTRACT, .ASSERT, .BOOLEAN, .BREAK, .BYTE, .CASE, .CATCH, .CHAR, .CLASS, .CONST, .CONTINUE, .DEFAULT, .DO, .DOUBLE, .ELSE, .ENUM, .EXTENDS, .FINAL, .FINALLY, .FLOAT, .FOR, .IF, .GOTO, .IMPLEMENTS, .IMPORT, .INSTANCEOF, .INT, @@ -197,9 +194,9 @@ .line-highlight { -rtfx-background-color: @cyan; } - .line-un-highlight { - -rtfx-background-color: @basenavy; - } + .line-un-highlight { + -rtfx-background-color: @basenavy; + } } @@ -325,6 +322,7 @@ -fx-background-color: blueviolet; } } + /**********************************************************************************************************************/ .context-menu { @@ -333,3 +331,68 @@ -fx-font-size: 9pt; //-fx-font-size: 9pt; } + +/**********************************************************************************************************************/ + +.graph { + -fx-background-color: white; +} + +.graph-cell { + -fx-background-color: @base2; + /*-fx-border-color: black; + -fx-border-width: 1pt; + -fx-border-radius: 10pt;*/ + -fx-text-alignment: center; + -fx-row-valignment: center; +} + +.graph-cell.vbox { + -fx-spacing:3pt; + -fx-alignment: center; + -fx-fill-width: true; +} + +.graph-cell.current-node { + -fx-background-color: firebrick; + -fx-stroke: white; + + .label { + -fx-text-alignment:center; + -fx-alignment: center; + -fx-font-size: 120%; + -fx-text-fill: white; + } + +} + + +.graph-cell .label { + -fx-text-alignment: center; +} + +.edge.intro { + -fx-stroke: #6679aa; +} + +.edge.over { + -fx-stroke: #200080; +} + +.edge.otni { + -fx-stroke: #AA9766; +} + +.edge.revo { + -fx-stroke: #DFFF80; +} + +.edge.rtrn { + -fx-stroke: orangered; +} + +.edge-label { + -fx-background-color: antiquewhite; + -fx-stroke: navy; +} + diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html index c8c6f8c2f871f5c4d597a75494b51f63cbbc6c97..dd0476fa067981eea4bfea1fb547771da2724ec4 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html @@ -132,7 +132,7 @@ Commands in scripts This list of available script commands is subject to change and to extension. If you write your own script commands (s. below), please -add an explanation to this list here. The list is sorted alphabetically. +addCell an explanation to this list here. The list is sorted alphabetically. -- auto ------------------ @@ -197,7 +197,7 @@ autopilot full autopilot autopilot-prep preparation only autopilot split-prop propositional expansion w/ splits nosplit-prop propositional expansion w/o splits -simp-upd update simplification +simp-upd updateTarget simplification simp-heap heap simplification Examples: @@ -208,7 +208,7 @@ directly.) -- rule ------------------ -Apply a single rule onto the current sequent. As unnamed argument add +Apply a single rule onto the current sequent. As unnamed argument addCell the name of the taclet to be applied. If the taclet matches only once on the entire sequent, the rule is applied. If it matches more than once you need to specify more. In that case you can first specify the diff --git a/website/docs/img/ScreenShotGoalList.png b/website/docs/img/ScreenShotGoalList.png new file mode 100644 index 0000000000000000000000000000000000000000..9c83ba410ee402c9ca661c7e8e82d22f498f38c6 Binary files /dev/null and b/website/docs/img/ScreenShotGoalList.png differ diff --git a/website/docs/img/ScreenShotGoalList2.png b/website/docs/img/ScreenShotGoalList2.png new file mode 100644 index 0000000000000000000000000000000000000000..19b5f8e577b613db040b79a49e215fa4a1764df5 Binary files /dev/null and b/website/docs/img/ScreenShotGoalList2.png differ diff --git a/website/docs/img/ScreenshotGoalList3 b/website/docs/img/ScreenshotGoalList3 new file mode 100644 index 0000000000000000000000000000000000000000..750e196ac62eb8b7ffa4255b6c7b81a1e56c47b8 Binary files /dev/null and b/website/docs/img/ScreenshotGoalList3 differ diff --git a/website/docs/img/ScreenshotGoalList3.png b/website/docs/img/ScreenshotGoalList3.png new file mode 100644 index 0000000000000000000000000000000000000000..5d7f6b5403c0194bd3471935af63b59ee0cda3cf Binary files /dev/null and b/website/docs/img/ScreenshotGoalList3.png differ diff --git a/website/docs/img/thumb_ScreenshotBreakpoint.png b/website/docs/img/thumb_ScreenshotBreakpoint.png new file mode 100644 index 0000000000000000000000000000000000000000..5f4b934d782c66620d0dc7a3edb79036c30d0d02 Binary files /dev/null and b/website/docs/img/thumb_ScreenshotBreakpoint.png differ diff --git a/website/docs/img/thumb_ScreenshotGoalList.png b/website/docs/img/thumb_ScreenshotGoalList.png new file mode 100644 index 0000000000000000000000000000000000000000..c60e9072346179b31e83abdef1dcedb47767c3ea Binary files /dev/null and b/website/docs/img/thumb_ScreenshotGoalList.png differ diff --git a/website/docs/img/thumb_ScreenshotInteractive.png b/website/docs/img/thumb_ScreenshotInteractive.png new file mode 100644 index 0000000000000000000000000000000000000000..e98ca96494da6e36c15dbcf903e16d6e5f15c61f Binary files /dev/null and b/website/docs/img/thumb_ScreenshotInteractive.png differ diff --git a/website/docs/img/thumb_ScreenshotProofTree.png b/website/docs/img/thumb_ScreenshotProofTree.png new file mode 100644 index 0000000000000000000000000000000000000000..0c996687a260fca02072f107b2e9bc6912792bef Binary files /dev/null and b/website/docs/img/thumb_ScreenshotProofTree.png differ diff --git a/website/docs/img/thumb_ScreenshotStep.png b/website/docs/img/thumb_ScreenshotStep.png new file mode 100644 index 0000000000000000000000000000000000000000..ec14aa4f25da6b45704beb128db5105466409bf2 Binary files /dev/null and b/website/docs/img/thumb_ScreenshotStep.png differ diff --git a/website/docs/img/thump_ruleApp.png b/website/docs/img/thump_ruleApp.png new file mode 100644 index 0000000000000000000000000000000000000000..d31d0ac8e88384114b4d0655e8f0ec2d4bdf3c56 Binary files /dev/null and b/website/docs/img/thump_ruleApp.png differ diff --git a/website/docs/index.md b/website/docs/index.md index b056581d88168496d6b065de601008338987f656..f0f411b450fe0702123df0ad59dd8bd5877cd935 100644 --- a/website/docs/index.md +++ b/website/docs/index.md @@ -1,5 +1,4 @@ -

Proof Script Debugger for the KeY System

+# Proof Script Debugger for the KeY System -

The proof script debugger is a prototypical implementation +The proof script debugger is a prototypical implementation of an interaction concept for program verification systems that are rule based and use a program logic. The prototype is implemented on top of the interactive program verification system -KeY. KeY is an interactive program verification +[KeY](http://www.key-project.org. KeY is an interactive program verification system for Java program annotated with the Java Modeling Language (JML). -

-

+ The protypical implementation includes a proof scripting language that is tailored to the problem domain of program verification. The main features of the language are: -

    -
  1. integration of domain specific entities like goal, formula, term and rule as + +1. integration of domain specific entities like goal, formula, term and rule as first-class citizens into the language;
  2. -
  3. an expressive proof goal selection mechanism -
      -
    • to identify and select individual proof branches,
    • -
    • to easily switch between proof branches,
    • -
    • to select multiple branches for uniform treatment (multi-matching);
    • -
    -that is resilient to small changes in the proof
  4. -
  5. a repetition construct which allows repeated application of proof strategies;
  6. -
  7. support for proof exploration within the language.
  8. - - -
+1. an expressive proof goal selection mechanism + * to identify and select individual proof branches, + * to easily switch between proof branches, + * to select multiple branches for uniform treatment (multi-matching); + that is resilient to small changes in the proof +1. a repetition construct which allows repeated application of proof strategies; +1. support for proof exploration within the language. + + Together with the proof scripting language a debugging concept for failed proof attempts is implemented that leverages well-known concepts from program debugging to the analysis of failed proof attempts. -

-

Publications

-A full description of the language and debugging-concept is published at HVC 2017. +## Publications + +A full description of the language and debugging-concept +is published at [HVC 2017](hvc2017.pdf) + -

Features

+## Features
-
+

Inspection of different parts of the proof state

The different parts of the proof state can be inspected: @@ -75,40 +78,49 @@ A full description of the language and debugging-concept is published at

Explore the proof tree of KeY

- +
-
-

Stepwise evaluation of the proof script

-

- The proof script can be evaluated stepwise and by running to a set breakpoint. -

-

Set a breakpoint and run execution to breakpoint

- + +
+ Mark lines with an (conditional) breakpoint to pause the script execution. +
-
-

Step forward and step backward

- +
+

Stepwise evaluation for time travellers

+ +
+ Stepwise script execution: step over and into. + Our special offers for time travellers: Go backwards in time + and then Back to the Future,again! +
-
+

Interactive Rule Application

- -
+ +
+ Select rules for interactive application. +
-
-

+

+ +
+ + +## Downloads + +* PSDBG - **Version 1.0-FM** [JAR](~/releases/psdbg-1.0-fm.jar) + Special Version for Formal Methods + + +
-For Accessing the prototype, please contact the authors. - -

diff --git a/website/docs/language.md b/website/docs/language.md index 19f3cb635c145d9c4bba5b09101b80508d9650d5..ff207f5c6f76dd1b13f0831acb81daf5991536d1 100644 --- a/website/docs/language.md +++ b/website/docs/language.md @@ -27,7 +27,7 @@ var1 : type := value; var2 := value; ``` -Both statements declare a variable, in the later we directly assign a value, in +Both statements declare a variable, in the latter case (`var1` and `var2`) we directly assign a value, in the first form `var0` receives a default value. ### Types and Literals @@ -42,7 +42,7 @@ We have following types: `INT`, `TERM`, `String`. * `TERM` represents a term of sort `S` in KeY. - `S` can be any sort of KeY. If the sort is ommitied, then `S=Any`. + `S` can be any sort given by KeY. If the sort is ommitied, then `S=Any`. ``` `f(x)` @@ -59,9 +59,9 @@ We have following types: `INT`, `TERM`, `String`. ### Special Variables -Not all variables are equal +To expose settings of the underlying prover to the user we include special variables: -* `MAX_STEPS` : amount +* `MAX_STEPS` : amount denotes the maximum number of proof steps the underlying prover is allowed to perform diff --git a/website/mkdocs.yml b/website/mkdocs.yml index 6d5c114f7fad4c8e67acbd3e31e05bc22942f6ed..9ba237983e65807f4e9ae8da2ccd96b492921bb3 100644 --- a/website/mkdocs.yml +++ b/website/mkdocs.yml @@ -17,8 +17,8 @@ markdown_extensions: permalink: True separator: "_" - sane_lists - - mdx_math: - enable_dollar_delimiter: True #for use of inline $..$ + # - mdx_math: + # enable_dollar_delimiter: True #for use of inline $..$ -extra_javascript: ['https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS_HTML'] + #extra_javascript: ['https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS_HTML']