From ae540f2f9264454f1516bf2392d62a1ce35153a8 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Mon, 5 Jun 2017 23:03:59 +0200 Subject: [PATCH] Repair and SectionPane/GoalOptionsMenu --- .../DebuggerMainWindowController.java | 44 +++++++++- .../formal/gui/controller/PuppetMaster.java | 8 +- .../formal/gui/controls/GoalOptionsMenu.java | 80 +++++++++++++++++++ .../kit/formal/gui/controls/ScriptArea.java | 3 + .../kit/formal/gui/controls/SectionPane.java | 66 +++++++++++++++ .../kit/formal/gui/controls/SequentView.java | 7 +- .../edu/kit/formal/gui/controls/Utils.java | 27 +++++++ .../interpreter/InterpreterBuilder.java | 24 +++++- .../formal/interpreter/KeYProofFacade.java | 9 +-- .../kit/formal/interpreter/data/KeyData.java | 77 ++++++++++++++++-- src/main/resources/DebuggerMain.fxml | 39 ++++----- src/main/resources/GoalView.fxml | 22 ++--- .../formal/gui/controls/GoalOptionsMenu.fxml | 25 ++++++ .../kit/formal/gui/controls/SectionPane.fxml | 20 +++++ src/main/resources/proofscriptdebugger.css | 24 +++++- 15 files changed, 421 insertions(+), 54 deletions(-) create mode 100644 src/main/java/edu/kit/formal/gui/controls/GoalOptionsMenu.java create mode 100644 src/main/java/edu/kit/formal/gui/controls/SectionPane.java create mode 100644 src/main/java/edu/kit/formal/gui/controls/Utils.java create mode 100644 src/main/resources/edu/kit/formal/gui/controls/GoalOptionsMenu.fxml create mode 100644 src/main/resources/edu/kit/formal/gui/controls/SectionPane.fxml diff --git a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java index e405f985..0ed0a8a9 100644 --- a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java +++ b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java @@ -4,6 +4,7 @@ import de.uka.ilkd.key.logic.op.IProgramMethod; import de.uka.ilkd.key.pp.ProgramPrinter; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.speclang.Contract; +import edu.kit.formal.gui.controls.GoalOptionsMenu; import edu.kit.formal.gui.controls.JavaArea; import edu.kit.formal.gui.controls.ScriptArea; import edu.kit.formal.gui.controls.SequentView; @@ -26,7 +27,9 @@ import javafx.concurrent.Task; import javafx.event.ActionEvent; import javafx.fxml.FXML; import javafx.fxml.Initializable; +import javafx.scene.Node; import javafx.scene.control.*; +import javafx.scene.input.MouseEvent; import javafx.scene.layout.GridPane; import javafx.scene.layout.Pane; import javafx.scene.layout.Priority; @@ -49,10 +52,13 @@ import java.util.concurrent.Executors; * Controller for the Debugger MainWindow * * @author S.Grebing + * @author Alexander Weigl */ public class DebuggerMainWindowController implements Initializable { private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false); + private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu(); + @FXML private Pane rootPane; @@ -171,7 +177,6 @@ public class DebuggerMainWindowController implements Initializable { /* TODO get lines of active statements marked lines javaSourceCode.getMarkedLines().clear(); javaSourceCode.getMarkedLines().addAll( - );*/ }); @@ -216,8 +221,7 @@ public class DebuggerMainWindowController implements Initializable { try { List scripts = Facade.getAST(scriptArea.getText()); lblStatusMessage.setText("Creating new Interpreter instance ..."); - ib.inheritState(interpreterService.interpreter.get()) - .setScripts(scripts); + ib.setScripts(scripts); Interpreter currentInterpreter = ib.build(); if (debugMode) { @@ -225,6 +229,7 @@ public class DebuggerMainWindowController implements Initializable { blocker.install(currentInterpreter); } interpreterService.interpreter.set(currentInterpreter); + interpreterService.mainScript.set(scripts.get(0)); interpreterService.start(); } catch (RecognitionException e) { showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e); @@ -372,6 +377,11 @@ public class DebuggerMainWindowController implements Initializable { blocker.unlock(); } + public void showGoalOptions(MouseEvent actionEvent) { + Node n = (Node) actionEvent.getTarget(); + goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY()); + } + public class ContractLoaderService extends Service> { @Override protected Task> createTask() { @@ -454,6 +464,7 @@ public class DebuggerMainWindowController implements Initializable { public GoalNodeListCell(ListView> goalNodeListView) { itemProperty().addListener(this::update); + goalOptionsMenu.selectedViewOptionProperty().addListener(this::update); } private void update(Observable observable) { @@ -462,7 +473,11 @@ public class DebuggerMainWindowController implements Initializable { return; } KeyData item = getItem().getData(); - setText(item.getNode().name()); + String text = "n/a"; + if (goalOptionsMenu.getSelectedViewOption() != null) { + text = goalOptionsMenu.getSelectedViewOption().getText(item); + } + setText(text); } } @@ -478,6 +493,27 @@ public class DebuggerMainWindowController implements Initializable { private final SimpleObjectProperty> interpreter = new SimpleObjectProperty<>(); private final SimpleObjectProperty mainScript = new SimpleObjectProperty<>(); + @Override + protected void succeeded() { + updateView(); + } + + @Override + protected void cancelled() { + updateView(); + } + + @Override + protected void failed() { + getException().printStackTrace(); + showExceptionDialog("Execution failed", "", "", getException()); + updateView(); + } + + private void updateView() { + blocker.publishState(); + } + @Override protected Task> createTask() { return new Task>() { diff --git a/src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java b/src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java index 4cb3984c..1cec2ccb 100644 --- a/src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java +++ b/src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java @@ -51,8 +51,10 @@ public class PuppetMaster { } public void deinstall(Interpreter interpreter) { - interpreter.getEntryListeners().remove(entryListener); - interpreter.getEntryListeners().remove(exitListener); + if (interpreter != null) { + interpreter.getEntryListeners().remove(entryListener); + interpreter.getEntryListeners().remove(exitListener); + } } public Void checkForHalt(ASTNode node) { @@ -72,7 +74,7 @@ public class PuppetMaster { return null; } - private void publishState() { + public void publishState() { System.out.println("PuppetMaster.publishState"); final State state = puppet.getCurrentState().copy(); Platform.runLater(() -> { diff --git a/src/main/java/edu/kit/formal/gui/controls/GoalOptionsMenu.java b/src/main/java/edu/kit/formal/gui/controls/GoalOptionsMenu.java new file mode 100644 index 00000000..a4496cf4 --- /dev/null +++ b/src/main/java/edu/kit/formal/gui/controls/GoalOptionsMenu.java @@ -0,0 +1,80 @@ +package edu.kit.formal.gui.controls; + +import com.google.common.collect.BiMap; +import com.google.common.collect.HashBiMap; +import edu.kit.formal.interpreter.data.KeyData; +import javafx.beans.property.ObjectProperty; +import javafx.beans.property.SimpleObjectProperty; +import javafx.fxml.FXML; +import javafx.scene.control.ContextMenu; +import javafx.scene.control.RadioMenuItem; +import javafx.scene.control.Toggle; +import javafx.scene.control.ToggleGroup; + +import java.util.function.Function; + +public class GoalOptionsMenu extends ContextMenu { + @FXML + private ToggleGroup toggleProjection; + + @FXML + private RadioMenuItem rmiShowSequent, rmiCFL, rmiCFS, rmiBranchLabels, rmiNodeNames, rmiRuleNames; + + private ObjectProperty selectedViewOption = new SimpleObjectProperty<>(); + + private BiMap optionMap = HashBiMap.create(6); + + public GoalOptionsMenu() { + Utils.createWithFXML(this); + + optionMap.put(rmiShowSequent, ViewOption.SEQUENT); + optionMap.put(rmiCFS, ViewOption.STATEMENTS); + optionMap.put(rmiCFL, ViewOption.PROGRAM_LINES); + optionMap.put(rmiBranchLabels, ViewOption.BRANCHING); + optionMap.put(rmiNodeNames, ViewOption.NAME); + optionMap.put(rmiRuleNames, ViewOption.RULES); + + toggleProjection.selectedToggleProperty().addListener((observable, oldValue, newValue) -> { + selectedViewOption.setValue(optionMap.get(newValue)); + }); + + selectedViewOption.addListener(o -> { + if (selectedViewOption.get() != null) + optionMap.inverse().get(selectedViewOption.get()).setSelected(true); + }); + + selectedViewOption.setValue(ViewOption.SEQUENT); + } + + + public ViewOption getSelectedViewOption() { + return selectedViewOption.get(); + } + + public ObjectProperty selectedViewOptionProperty() { + return selectedViewOption; + } + + public void setSelectedViewOption(ViewOption selectedViewOption) { + this.selectedViewOption.set(selectedViewOption); + } + + public enum ViewOption { + BRANCHING(KeyData::getBranchingLabel), + RULES(KeyData::getRuleLabel), + PROGRAM_LINES(KeyData::getProgramLinesLabel), + STATEMENTS(KeyData::getProgramStatementsLabel), + NAME(KeyData::getNameLabel), + SEQUENT(item -> item.getNode().sequent().toString()); + + private final Function projection; + + ViewOption(Function toString) { + projection = toString; + } + + public String getText(KeyData item) { + return projection.apply(item); + } + } +} \ No newline at end of file diff --git a/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java b/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java index d7992ddf..a68cf90b 100644 --- a/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java +++ b/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java @@ -220,6 +220,9 @@ public class ScriptArea extends CodeArea { lineNo.setTextFill(defaultTextFill); hbox.setPadding(defaultInsets); hbox.getStyleClass().add("lineno"); + + hbox.setStyle("-fx-cursor: hand"); + return hbox; } diff --git a/src/main/java/edu/kit/formal/gui/controls/SectionPane.java b/src/main/java/edu/kit/formal/gui/controls/SectionPane.java new file mode 100644 index 00000000..149f49ef --- /dev/null +++ b/src/main/java/edu/kit/formal/gui/controls/SectionPane.java @@ -0,0 +1,66 @@ +package edu.kit.formal.gui.controls; + +import javafx.beans.property.StringProperty; +import javafx.collections.ObservableList; +import javafx.fxml.FXML; +import javafx.fxml.FXMLLoader; +import javafx.scene.Node; +import javafx.scene.control.Label; +import javafx.scene.layout.BorderPane; +import javafx.scene.layout.HBox; + +import java.io.IOException; + +/** + * @author Alexander Weigl + * @version 1 (05.06.17) + */ +public class SectionPane extends BorderPane { + private StringProperty title; + + @FXML + private Label titleLabel; + + @FXML + private HBox northBox; + + @FXML + private HBox buttons; + + public SectionPane() { + super(); + FXMLLoader loader = new FXMLLoader(getClass().getResource("SectionPane.fxml")); + loader.setRoot(this); + loader.setController(this); + try { + loader.load(); + } catch (IOException e) { + e.printStackTrace(); + } + + title = titleLabel.textProperty(); + } + + public SectionPane(Node center) { + this(); + setCenter(center); + } + + + public String getTitle() { + return title.get(); + } + + public StringProperty titleProperty() { + return title; + } + + public void setTitle(String title) { + this.title.set(title); + } + + + public ObservableList getHeaderRight() { + return buttons.getChildren(); + } +} diff --git a/src/main/java/edu/kit/formal/gui/controls/SequentView.java b/src/main/java/edu/kit/formal/gui/controls/SequentView.java index d2c48eef..979617e2 100644 --- a/src/main/java/edu/kit/formal/gui/controls/SequentView.java +++ b/src/main/java/edu/kit/formal/gui/controls/SequentView.java @@ -72,8 +72,11 @@ public class SequentView extends CodeArea { } private void hightlightRange(int start, int end) { - clearHighlight(); - setStyleClass(start, end, "sequent-highlight"); + try { + clearHighlight(); + setStyleClass(start, end, "sequent-highlight"); + } catch (IllegalStateException e) { + } } private void clearHighlight() { diff --git a/src/main/java/edu/kit/formal/gui/controls/Utils.java b/src/main/java/edu/kit/formal/gui/controls/Utils.java new file mode 100644 index 00000000..0b2af841 --- /dev/null +++ b/src/main/java/edu/kit/formal/gui/controls/Utils.java @@ -0,0 +1,27 @@ +package edu.kit.formal.gui.controls; + +import javafx.fxml.FXMLLoader; + +import java.io.IOException; + +/** + * @author Alexander Weigl + * @version 1 (05.06.17) + */ +public class Utils { + private Utils() { + } + + public static void createWithFXML(Object node) { + FXMLLoader loader = new FXMLLoader( + node.getClass().getResource(node.getClass().getSimpleName() + ".fxml") + ); + loader.setController(node); + loader.setRoot(node); + try { + loader.load(); + } catch (IOException e) { + throw new RuntimeException("Could not load fxml", e); + } + } +} diff --git a/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java b/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java index eec0c1ae..0b6b856d 100644 --- a/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java +++ b/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java @@ -1,12 +1,14 @@ package edu.kit.formal.interpreter; import de.uka.ilkd.key.api.KeYApi; +import de.uka.ilkd.key.api.ProjectedNode; import de.uka.ilkd.key.api.ProofApi; import de.uka.ilkd.key.api.ScriptApi; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; import de.uka.ilkd.key.proof.Proof; +import edu.kit.formal.interpreter.data.GoalNode; import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.VariableAssignment; import edu.kit.formal.interpreter.funchdl.*; @@ -75,9 +77,9 @@ public class InterpreterBuilder { } public InterpreterBuilder proof(KeYEnvironment env, Proof proof) { - //TODO relax constructor of proofapi - //return proof(new ProofApi(proof, env)); - return this; + this.keyEnvironment = env; + this.proof = proof; + return proof(new ProofApi(proof, env)); } public InterpreterBuilder scriptCommands() { @@ -181,4 +183,20 @@ public class InterpreterBuilder { lookup.getBuilders().add(0, ignoreHandler); return this; } + + public InterpreterBuilder startState() { + if (proof == null || keyEnvironment == null) + throw new IllegalStateException("Call proof(..) before startState"); + + final ProofApi pa = new ProofApi(proof, keyEnvironment); + final ProjectedNode root = pa.getFirstOpenGoal(); + final KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof()); + final GoalNode startGoal = new GoalNode<>(null, keyData); + return startState(startGoal); + } + + private InterpreterBuilder startState(GoalNode startGoal) { + interpreter.newState(startGoal); + return this; + } } diff --git a/src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java b/src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java index 597bcf06..840ee107 100644 --- a/src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java +++ b/src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java @@ -89,17 +89,14 @@ public class KeYProofFacade { assert readyToExecute.getValue(); InterpreterBuilder interpreterBuilder = new InterpreterBuilder(); - interpreterBuilder.proof(environment.get(), proof.get()) + interpreterBuilder + .proof(environment.get(), proof.get()) + .startState() .macros() .scriptCommands() .scriptSearchPath(new File(".")); getProof().getProofIndependentSettings().getGeneralSettings().setOneStepSimplification(false); - // Set first state - final ProofApi pa = new ProofApi(getProof(), getEnvironment()); - final ProjectedNode root = pa.getFirstOpenGoal(); - final KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof()); - final GoalNode startGoal = new GoalNode<>(null, keyData); return interpreterBuilder; } diff --git a/src/main/java/edu/kit/formal/interpreter/data/KeyData.java b/src/main/java/edu/kit/formal/interpreter/data/KeyData.java index 4b3f403b..e1b0f3f7 100644 --- a/src/main/java/edu/kit/formal/interpreter/data/KeyData.java +++ b/src/main/java/edu/kit/formal/interpreter/data/KeyData.java @@ -3,10 +3,9 @@ package edu.kit.formal.interpreter.data; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; -import lombok.AllArgsConstructor; -import lombok.Data; -import lombok.EqualsAndHashCode; -import lombok.ToString; +import lombok.*; + +import java.util.function.Function; /** * @author Alexander Weigl @@ -16,10 +15,18 @@ import lombok.ToString; @AllArgsConstructor @ToString @EqualsAndHashCode +@RequiredArgsConstructor public class KeyData { - private Node node; - private KeYEnvironment env; - private Proof proof; + private static final String SEPARATOR = " // "; + private final Node node; + private final KeYEnvironment env; + private final Proof proof; + + private String branchingLabel, + ruleLabel, + programLinesLabel, + programStatementsLabel, + nameLabel; public KeyData(KeyData data, Node node) { env = data.env; @@ -29,5 +36,61 @@ public class KeyData { this.node = node; } + public String getRuleLabel() { + if (ruleLabel == null) { + ruleLabel = constructLabel((Node n) -> n.getAppliedRuleApp().rule().name().toString()); + } + return ruleLabel; + } + + private String constructLabel(Function projection) { + StringBuilder sb = new StringBuilder(); + Node cur = node; + do { + try { + String section = projection.apply(node); + if (section != null) { + sb.append(section); + sb.append(SEPARATOR); + } + } catch (Exception e) { + } + cur = cur.parent(); + } while (cur != null); + sb.append("$$"); + return sb.toString(); + } + + public String getBranchingLabel() { + if (branchingLabel == null) { + branchingLabel = constructLabel(n -> n.getNodeInfo().getBranchLabel()); + } + return branchingLabel; + } + + public String getNameLabel() { + if (nameLabel == null) { + nameLabel = constructLabel(Node::name); + } + return nameLabel; + } + + + public String getProgramLinesLabel() { + if (programLinesLabel == null) { + programLinesLabel = constructLabel(n -> + Integer.toString(n.getNodeInfo().getExecStatementPosition().getLine())); + } + return programLinesLabel; + } + + public String getProgramStatementsLabel() { + if (programStatementsLabel == null) { + programStatementsLabel = constructLabel(n -> + n.getNodeInfo().getFirstStatementString()); + } + return programStatementsLabel; + } + } diff --git a/src/main/resources/DebuggerMain.fxml b/src/main/resources/DebuggerMain.fxml index 20bacd67..ae030f4c 100644 --- a/src/main/resources/DebuggerMain.fxml +++ b/src/main/resources/DebuggerMain.fxml @@ -2,9 +2,7 @@ - - - + @@ -81,36 +79,41 @@ - - - + + + +
- + - - - + + + +
- - - - + +
- + diff --git a/src/main/resources/GoalView.fxml b/src/main/resources/GoalView.fxml index eb813937..a1229bb0 100644 --- a/src/main/resources/GoalView.fxml +++ b/src/main/resources/GoalView.fxml @@ -1,10 +1,12 @@ - - - - - - -