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 72a4ed63b05592cfd73f406f32eca3dc991b347c..0aed81137fe2492843752a739cc1baf00e207159 100644 --- a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java +++ b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java @@ -4,10 +4,7 @@ import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.speclang.Contract; import edu.kit.formal.gui.controls.*; import edu.kit.formal.gui.model.RootModel; -import edu.kit.formal.interpreter.Interpreter; -import edu.kit.formal.interpreter.InterpreterBuilder; -import edu.kit.formal.interpreter.KeYProofFacade; -import edu.kit.formal.interpreter.ProofTreeController; +import edu.kit.formal.interpreter.*; import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.proofscriptparser.Facade; import edu.kit.formal.proofscriptparser.ast.ProofScript; @@ -102,8 +99,6 @@ public class DebuggerMainWindowController implements Initializable { private File initialDirectory; - - /** * Controller for debugging functions */ @@ -172,10 +167,12 @@ public class DebuggerMainWindowController implements Initializable { blocker.getBreakpoints().addAll(change.getSet()); });*/ - pc.currentGoalsProperty().addListener((o, old, fresh) -> { + /*pc.currentGoalsProperty().addListener((o, old, fresh) -> { model.currentGoalNodesProperty().setAll(fresh); }); - model.currentSelectedGoalNodeProperty().bind(pc.currentSelectedGoalProperty()); + model.currentSelectedGoalNodeProperty().bind(pc.currentSelectedGoalProperty());*/ + + //model.currentGoalNodesProperty().bind(pc.currentGoalsProperty()); CustomTabPaneSkin skin = new CustomTabPaneSkin(tabPane); @@ -226,6 +223,20 @@ public class DebuggerMainWindowController implements Initializable { pc.setMainScript(scripts.get(0)); pc.executeScript(this.debugMode.get()); + pc.currentGoalsProperty().addListener((o, old, fresh) -> { + if (fresh != null) { + model.currentGoalNodesProperty().setAll(fresh); + } + }); + model.currentSelectedGoalNodeProperty().bind(pc.currentSelectedGoalProperty()); + + /* pc.currentGoalsProperty().addListener((observable, oldValue, newValue) -> { + if(newValue != null) { + model.currentGoalNodesProperty().get(). + setAll(pc.currentGoalsProperty()); + } + });*/ + //highlight signature of main script tabPane.getSelectedScriptArea().setDebugMark(scripts.get(0).getStartPosition().getLineNumber()); } catch (RecognitionException e) { @@ -376,16 +387,19 @@ public class DebuggerMainWindowController implements Initializable { public void stepOver(ActionEvent actionEvent) { // blocker.getStepUntilBlock().addAndGet(1); // blocker.unlock(); - pc.stepOver(); + PTreeNode newState = pc.stepOver(); + // model.currentGoalNodesProperty().setAll(newState.getState().getGoals()); + // model.setCurrentSelectedGoalNode(newState.getState().getSelectedGoalNode()); } public void stepBack(ActionEvent actionEvent) { - pc.stepBack(); + PTreeNode newState = pc.stepBack(); + // model.currentGoalNodesProperty().setAll(newState.getState().getGoals()); + // model.setCurrentSelectedGoalNode(newState.getState().getSelectedGoalNode()); } - public KeYProofFacade getFacade() { return facade; } diff --git a/src/main/java/edu/kit/formal/gui/controller/ListGoalView.java b/src/main/java/edu/kit/formal/gui/controller/ListGoalView.java index d07fbb1def0eb4829e47a80aa3832616ce5a64d9..b1e2623a23fcb3bda5c31c4b68da90ec9c551188 100644 --- a/src/main/java/edu/kit/formal/gui/controller/ListGoalView.java +++ b/src/main/java/edu/kit/formal/gui/controller/ListGoalView.java @@ -4,8 +4,6 @@ import edu.kit.formal.gui.model.RootModel; import edu.kit.formal.interpreter.data.GoalNode; import edu.kit.formal.interpreter.data.KeyData; import javafx.beans.property.SimpleListProperty; -import javafx.beans.value.ChangeListener; -import javafx.beans.value.ObservableValue; import javafx.fxml.FXML; import javafx.fxml.FXMLLoader; import javafx.scene.control.ListCell; @@ -52,7 +50,7 @@ public class ListGoalView extends VBox { /** * Set Bindings and listener */ - public void init() { + /* public void init() { listOfGoalsView.itemsProperty().bind(this.rootModel.currentGoalNodesProperty()); listOfGoalsView.getSelectionModel().selectedItemProperty().addListener(new ChangeListener>() { @@ -63,7 +61,7 @@ public class ListGoalView extends VBox { }); } - +*/ private static class GoalNodeCell extends ListCell> { 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 660eaaef53118f73a90376c11f2f6ea12769d96f..ac7fab8b9ea853184a65c50b944809076b203e54 100644 --- a/src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java +++ b/src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java @@ -26,6 +26,9 @@ import java.util.concurrent.locks.ReentrantLock; public class PuppetMaster { private final Lock lock = new ReentrantLock(); private final Condition block = lock.newCondition(); + /** + * Properties that are changed, when new states are added using the blocker + */ private final SimpleObjectProperty>> currentGoals = new SimpleObjectProperty<>(); private final SimpleObjectProperty> currentSelectedGoal = new SimpleObjectProperty<>(); private Interpreter puppet; @@ -155,9 +158,9 @@ public class PuppetMaster { this.currentGoals.set(currentGoals); } - public SimpleObjectProperty>> currentGoalsProperty() { + /* public SimpleObjectProperty>> currentGoalsProperty() { return currentGoals; - } + }*/ public Set getBreakpoints() { return brkpnts; diff --git a/src/main/java/edu/kit/formal/gui/controls/InspectionViewTabPane.java b/src/main/java/edu/kit/formal/gui/controls/InspectionViewTabPane.java index 2094f0953ac1a338ded9e44fe7d04d0b03f5885e..fbb1a7c777e1669f595796468a81170ad22b1f36 100644 --- a/src/main/java/edu/kit/formal/gui/controls/InspectionViewTabPane.java +++ b/src/main/java/edu/kit/formal/gui/controls/InspectionViewTabPane.java @@ -52,11 +52,14 @@ public class InspectionViewTabPane extends TabPane { this.getTabs().add(tab); } + //TODO schauen wie Goallist ins model kommt public void bindGoalNodesWithCurrentTab(RootModel model) { + getActiveInspectionViewTab().getGoalView().itemsProperty().bind(model.currentGoalNodesProperty()); model.currentSelectedGoalNodeProperty().addListener((p, old, fresh) -> { getActiveInspectionViewTab().getGoalView().getSelectionModel().select(fresh); + /* TODO get lines of active statements marked lines javaSourceCode.getMarkedLines().clear(); javaSourceCode.getMarkedLines().addAll( diff --git a/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java b/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java index 80534aeacf166e9650966dda3fe5f2753138c16e..59f1f02babc93d60dc19fef6b71458e9976fe558 100644 --- a/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java +++ b/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java @@ -3,7 +3,9 @@ package edu.kit.formal.interpreter; import edu.kit.formal.gui.controller.PuppetMaster; import edu.kit.formal.interpreter.data.GoalNode; import edu.kit.formal.interpreter.data.KeyData; +import edu.kit.formal.interpreter.data.State; import edu.kit.formal.proofscriptparser.Visitor; +import edu.kit.formal.proofscriptparser.ast.Position; import edu.kit.formal.proofscriptparser.ast.ProofScript; import javafx.beans.property.ListProperty; import javafx.beans.property.ReadOnlyBooleanProperty; @@ -24,17 +26,36 @@ public class ProofTreeController { * To control stepping */ private final PuppetMaster blocker = new PuppetMaster(); - private final SimpleObjectProperty>> currentGoals = new SimpleObjectProperty<>(); - //= blocker.currentGoalsProperty(); - private final ListProperty> currentGoalList = new SimpleListProperty<>(FXCollections.observableArrayList()); + /** + * Goals of the state which is referenced by the statePointer + */ + private final ListProperty> currentGoals = new SimpleListProperty<>(FXCollections.observableArrayList()); + + /** + * Selected Goal of the state which is referenced by the statePointer + */ private final SimpleObjectProperty> currentSelectedGoal = new SimpleObjectProperty<>(); - //= blocker.currentSelectedGoalProperty(); - //new SimpleBooleanProperty(false); + + + /** + * Service to run interpreter in own thread + */ private InterpretingService interpreterService = new InterpretingService(blocker); + + /** + * To identify when interpreterservice is running + */ private ReadOnlyBooleanProperty executeNotPossible = interpreterService.runningProperty(); + /** + * Node that is updated whenever a new node is added to the stategraph (this can only happen in debug mode when stepover is invoked) + */ private SimpleObjectProperty nextComputedNode = new SimpleObjectProperty<>(); + private SimpleObjectProperty startHighlightPositionProperty = new SimpleObjectProperty<>(); + + private SimpleObjectProperty endHighlightPositionProperty = new SimpleObjectProperty<>(); + /** * Visitor to retrieve state graph */ @@ -52,29 +73,42 @@ public class ProofTreeController { private Interpreter currentInterpreter; /** - * Current State in graph + * Pointer to current selected state in graph */ private PTreeNode statePointer = null; - + /** + * Teh mainscipt that is executed + */ private ProofScript mainScript; /** - * Add a change listener for the stategraph + * Add a change listener for the stategraph, whenever a new node is added it receives an event */ private GraphChangedListener graphChangedListener = nodeAddedEvent -> { if (statePointer.equals(nodeAddedEvent.getLastPointer())) { + //set value of newly computed node nextComputedNode.setValue(nodeAddedEvent.getAddedNode()); + //setNewState(this.statePointer.getState()); } }; public ProofTreeController() { - this.currentGoals.bindBidirectional(blocker.currentGoalsProperty()); + + //get state from blocker, who communicates with interpreter this.currentSelectedGoal.bindBidirectional(blocker.currentSelectedGoalProperty()); + //add listener to nextcomputed node, that is updated whenever a new node is added to the stategraph + nextComputedNode.addListener((observable, oldValue, newValue) -> { + //update statepointer + this.statePointer = newValue; + setNewState(this.statePointer.getState()); + }); + + } @@ -91,55 +125,48 @@ public class ProofTreeController { } //TODO handle endpoint - //handle inconsistency + + /** + * StepOver and return the node to shich the state pointer is pointing to + * + * @return + */ public PTreeNode stepOver() { + //get current pointer into stategraph PTreeNode currentPointer = statePointer; - + //if pointer is null, we do not have a root yet if (currentPointer == null) { - System.out.println("StatePointer is null"); - } else { - if (this.statePointer.getState() != null && this.statePointer.getScriptstmt() != null) { - System.out.println("StatePointer is " + currentPointer.getScriptstmt().getNodeName() + currentPointer.getScriptstmt().getStartPosition()); - } else { - System.out.println("Possibly root node"); - } - PTreeNode nextNode = stateGraphVisitor.getStepOver(currentPointer); - - if (nextNode != null) { - this.statePointer = nextNode; - } else { - nextComputedNode.addListener((observable, oldValue, newValue) -> { - this.statePointer = newValue; - System.out.println("Added new Value to Statepointer: " + this.statePointer.getScriptstmt().getNodeName() + this.statePointer.getScriptstmt().getStartPosition()); - }); - //let interpreter run for one step - blocker.getStepUntilBlock().addAndGet(1); - blocker.unlock(); - - //stateGraphListener - - //this.statePointer = nextNode; - } + //ask for root + currentPointer = stateGraphVisitor.rootProperty().get(); + statePointer = currentPointer; } - - - return null; + PTreeNode nextNode = stateGraphVisitor.getStepOver(currentPointer); + if (nextNode != null) { + this.statePointer = nextNode; + setNewState(statePointer.getState()); + } else { + //no next node is present yet + //let interpreter run for one step and let listener handle updating the statepointer + blocker.getStepUntilBlock().addAndGet(1); + blocker.unlock(); + } + return statePointer; } //TODO handle endpoint of graph + + /** + * Step Back one Node in the stategraph + * @return + */ public PTreeNode stepBack() { PTreeNode current = statePointer; - this.statePointer = stateGraphVisitor.getStepBack(current); - if (this.statePointer == null) { + PTreeNode backState = stateGraphVisitor.getStepBack(current); + this.statePointer = backState; + setNewState(statePointer.getState()); + return statePointer; - } else { - this.currentGoals.set(this.statePointer.getState().getGoals()); - this.currentSelectedGoal.set(this.statePointer.getState().getSelectedGoalNode()); - } - System.out.println("PRED NODE \n\n" + this.statePointer.getState().getSelectedGoalNode().getData().getNode().serialNr() + ":" + - this.statePointer.getScriptstmt().getNodeName() + "@" + this.statePointer.getScriptstmt().getStartPosition() + "\n-------------------\n"); - return null; } public PTreeNode stepInto() { @@ -157,20 +184,17 @@ public class ProofTreeController { if (!debugMode) { blocker.getStepUntilBlock().set(-1); } else { + this.startHighlightPositionProperty.set(mainScript.getSignature().getStartPosition()); + this.endHighlightPositionProperty.set(mainScript.getSignature().getEndPosition()); //build CFG buildControlFlowGraph(mainScript); //build StateGraph this.stateGraphVisitor = new StateGraphVisitor(this.currentInterpreter, this.mainScript, this.controlFlowGraphVisitor); - // this.stateGraphVisitor = new StateGraphVisitor(blocker, this.mainScript, this.controlFlowGraphVisitor); + currentInterpreter.getEntryListeners().add(this.stateGraphVisitor); + //currentInterpreter.getExitListeners().add(this.stateGraphVisitor); this.stateGraphVisitor.addChangeListener(graphChangedListener); - // - // stateGraphVisitor.rootProperty().addListener((observable, oldValue, newValue) -> { - // this.statePointer = newValue; - // }); - this.statePointer = stateGraphVisitor.getRoot(); - blocker.getStepUntilBlock().set(1); } interpreterService.interpreterProperty().set(currentInterpreter); @@ -181,6 +205,17 @@ public class ProofTreeController { } + /** + * Sets the properties that may notify GUI about statechanges with new state values + * + * @param state + */ + private void setNewState(State state) { + this.setCurrentGoals(state.getGoals()); + this.setCurrentSelectedGoal(state.getSelectedGoalNode()); + System.out.println("New State from this command: " + this.statePointer.getScriptstmt().getNodeName() + "@" + this.statePointer.getScriptstmt().getStartPosition()); + } + /************************************************************************************************************** * * Getter and Setter @@ -205,10 +240,10 @@ public class ProofTreeController { } public void setCurrentGoals(List> currentGoals) { - this.currentGoals.set(currentGoals); + this.currentGoals.get().setAll(currentGoals); } - public SimpleObjectProperty>> currentGoalsProperty() { + public ListProperty> currentGoalsProperty() { return currentGoals; } @@ -233,4 +268,5 @@ public class ProofTreeController { } + } diff --git a/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java b/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java index 59509ce253b447ca48a768a6a1e6bf7f7a47331a..76be23f220e02b5da517fd79e0a3a3dbf79a7b2f 100644 --- a/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java +++ b/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java @@ -3,10 +3,11 @@ package edu.kit.formal.interpreter; import com.google.common.graph.MutableValueGraph; import com.google.common.graph.ValueGraphBuilder; -import edu.kit.formal.gui.controller.PuppetMaster; import edu.kit.formal.interpreter.data.KeyData; +import edu.kit.formal.interpreter.data.State; import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.ast.*; +import javafx.application.Platform; import javafx.beans.property.SimpleObjectProperty; import lombok.Getter; @@ -34,7 +35,7 @@ public class StateGraphVisitor extends DefaultASTVisitor { */ private Interpreter currentInterpreter; - private PuppetMaster blocker; + /** * Graph that is computed on the fly in order to allow stepping */ @@ -56,10 +57,7 @@ public class StateGraphVisitor extends DefaultASTVisitor { */ private ProgramFlowVisitor cfgVisitor; - /** - * Pointer for stepping - */ - private PTreeNode currentStatePointer; + private ProofScript mainScript; @@ -68,7 +66,8 @@ public class StateGraphVisitor extends DefaultASTVisitor { this.currentInterpreter = inter; this.cfgVisitor = cfgVisitor; this.mainScript = mainScript; - createRootNode(); + + //createRootNode(); } @@ -83,18 +82,29 @@ public class StateGraphVisitor extends DefaultASTVisitor { } - public void createRootNode() { - PTreeNode newStateNode = new PTreeNode(null); - newStateNode.setState(currentInterpreter.getCurrentState()); + public void createRootNode(ASTNode node) { + PTreeNode newStateNode = new PTreeNode(node); + newStateNode.setState(currentInterpreter.getCurrentState().copy()); stateGraph.addNode(newStateNode); this.root.set(newStateNode); lastNode = newStateNode; + + } + + public void setUpGraph() { + //create empty graph + stateGraph = ValueGraphBuilder.directed().build(); + } //careful TODO look for right edges //TODO handle endpoint of graph public PTreeNode getStepOver(PTreeNode statePointer) { + + if (statePointer == null) { + return this.rootProperty().get(); + } Set successors = this.stateGraph.successors(statePointer); if (successors.isEmpty()) { return null; @@ -150,23 +160,32 @@ public class StateGraphVisitor extends DefaultASTVisitor { * @return */ public Void createNewNode(ASTNode node) { + State lastState = lastNode.getState(); + //maybe delete + //lastNode.setState(currentInterpreter.getCurrentState()); PTreeNode newStateNode; newStateNode = new PTreeNode(node); - newStateNode.setState(currentInterpreter.getCurrentState()); - stateGraph.addNode(newStateNode); - + State currentState = currentInterpreter.getCurrentState().copy(); + System.out.println("Equals of states " + currentState.equals(lastState)); + newStateNode.setState(currentState); + stateGraph.addNode(newStateNode); stateGraph.putEdgeValue(lastNode, newStateNode, EdgeTypes.STATE_FLOW); fireNodeAdded(new NodeAddedEvent(lastNode, newStateNode)); lastNode = newStateNode; + return null; } @Override public Void visit(ProofScript proofScript) { - createNewNode(proofScript); + if (this.root.get() == null) { + createRootNode(proofScript); + } else { + createNewNode(proofScript); + } return null; } @@ -255,9 +274,10 @@ public class StateGraphVisitor extends DefaultASTVisitor { protected void fireNodeAdded(NodeAddedEvent nodeAddedEvent) { - System.out.println("New Node added " + nodeAddedEvent.toString()); changeListeners.forEach(list -> { - list.graphChanged(nodeAddedEvent); + Platform.runLater(() -> { + list.graphChanged(nodeAddedEvent); + }); }); }