Debugging Strcuture and Controller first interface ideas

src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java

@@ -7,6 +7,7 @@ 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.data.KeyData;
 import edu.kit.formal.interpreter.data.State;
 import edu.kit.formal.proofscriptparser.Facade;
@@ -14,7 +15,6 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript;
 import javafx.beans.property.SimpleBooleanProperty;
 import javafx.beans.property.SimpleObjectProperty;
 import javafx.beans.value.ObservableBooleanValue;
-import javafx.collections.SetChangeListener;
 import javafx.concurrent.Service;
 import javafx.concurrent.Task;
 import javafx.event.ActionEvent;
@@ -52,7 +52,7 @@ public class DebuggerMainWindowController implements Initializable {
 
     private final PuppetMaster blocker = new PuppetMaster();
     private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false);
-    private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
+    // private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
 
     @FXML
     private Pane rootPane;
@@ -225,15 +225,18 @@ public class DebuggerMainWindowController implements Initializable {
             Interpreter<KeyData> currentInterpreter = ib.build();
 
             if (debugMode) {
-                blocker.getStepUntilBlock().set(1);
+                ProofTreeController pc = new ProofTreeController(currentInterpreter, scripts.get(0));
+                //blocker.getStepUntilBlock().set(1);
+
             }
             blocker.install(currentInterpreter);
 
-            System.out.println("Start of Script in: " + scripts.get(0).getStartPosition());
+            //highlight signature of main script
             tabPane.getSelectedScriptArea().setDebugMark(scripts.get(0).getStartPosition().getLineNumber());
 
             interpreterService.interpreter.set(currentInterpreter);
             interpreterService.mainScript.set(scripts.get(0));
+
             interpreterService.start();
         } catch (RecognitionException e) {
             showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
@@ -385,6 +388,11 @@ public class DebuggerMainWindowController implements Initializable {
         blocker.unlock();
     }
 
+    public void stepBack(ActionEvent actionEvent) {
+        System.out.println(blocker.getHistoryLogger());
+        blocker.unlock();
+    }
+
 
 
     public KeYProofFacade getFacade() {

src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java

 package edu.kit.formal.gui.controller;
 
+import edu.kit.formal.interpreter.HistoryListener;
 import edu.kit.formal.interpreter.Interpreter;
 import edu.kit.formal.interpreter.data.GoalNode;
 import edu.kit.formal.interpreter.data.KeyData;
@@ -29,10 +30,10 @@ public class PuppetMaster {
     private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoal = new SimpleObjectProperty<>();
     private Interpreter<KeyData> puppet;
     private AtomicInteger stepUntilBlock = new AtomicInteger(-1);
+    private HistoryListener historyLogger;
     private Set<Integer> brkpnts = new ConcurrentSkipListSet<>();
     private Visitor<Void> entryListener = new EntryListener();
     private Visitor<Void> exitListener = new ExitListener();
-
     public PuppetMaster() {
     }
 
@@ -40,6 +41,10 @@ public class PuppetMaster {
         install(puppet);
     }
 
+    public HistoryListener getHistoryLogger() {
+        return historyLogger;
+    }
+
     public void install(Interpreter<KeyData> interpreter) {
         if (puppet != null) deinstall(puppet);
         interpreter.getEntryListeners().add(entryListener);
@@ -56,6 +61,7 @@ public class PuppetMaster {
 
     public Void checkForHalt(ASTNode node) {
         System.out.println("node = [" + node + "]");
+
         //<0 run
         if (stepUntilBlock.get() > 0)
             stepUntilBlock.decrementAndGet();
@@ -74,11 +80,11 @@ public class PuppetMaster {
     }
 
     /**
-     * Publish state is called after the interpreter or debugger thread terminated. The resulting goals are set in teh root model
+     * Publish state is called after the interpreter or debugger thread terminated. The resulting goals are set in the root model
      */
     public void publishState() {
         System.out.println("PuppetMaster.publishState");
-        //puppet is null if sucessful interpreter state and publish state
+        //puppet is null if successful interpreter state and publish state
         if (puppet != null) {
 
             final State<KeyData> state = puppet.getCurrentState().copy();
@@ -165,6 +171,10 @@ public class PuppetMaster {
         deinstall(puppet);
     }
 
+    public void addHistoryLogger(HistoryListener historyLogger) {
+        this.historyLogger = historyLogger;
+    }
+
     private class EntryListener extends DefaultASTVisitor<Void> {
 
         @Override

src/main/java/edu/kit/formal/interpreter/EdgeTypes.java

+package edu.kit.formal.interpreter;
+
+/**
+ * Created by sarah on 6/20/17.
+ */
+public enum EdgeTypes {
+    STEP_INTO, STEP_OVER, STEP_BACK, STEP_RETURN;
+}

src/main/java/edu/kit/formal/interpreter/PTreeNode.java

+package edu.kit.formal.interpreter;
+
+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.ast.ASTNode;
+
+/**
+ * Inner class representing nodes in the graph
+ * A node contains a reference to the ASTNode and a reference to the corresponding interpreter state if this state is already interpreted, null otherwise.
+ */
+public class PTreeNode {
+    State<GoalNode<KeyData>> state;
+
+    ASTNode scriptstmt;
+
+    public PTreeNode(ASTNode node) {
+        this.setScriptstmt(node);
+    }
+
+    public State<GoalNode<KeyData>> getState() {
+        return state;
+    }
+
+    public void setState(State<GoalNode<KeyData>> state) {
+        this.state = state;
+    }
+
+    public ASTNode getScriptstmt() {
+        return scriptstmt;
+    }
+
+    public void setScriptstmt(ASTNode scriptstmt) {
+        this.scriptstmt = scriptstmt;
+    }
+
+    public boolean hasState() {
+        return state != null;
+    }
+
+    public String toString() {
+        StringBuilder sb = new StringBuilder();
+        sb.append("Node {");
+        if (scriptstmt != null) {
+            sb.append(scriptstmt.toString());
+        } else {
+            sb.append("No Stmt");
+        }
+        sb.append("}");
+        return sb.toString();
+    }
+
+
+}

src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java

+package edu.kit.formal.interpreter;
+
+import com.google.common.graph.MutableValueGraph;
+import com.google.common.graph.ValueGraphBuilder;
+import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
+import edu.kit.formal.proofscriptparser.ast.AssignmentStatement;
+import edu.kit.formal.proofscriptparser.ast.ProofScript;
+import edu.kit.formal.proofscriptparser.ast.Statement;
+import edu.kit.formal.proofscriptparser.ast.Statements;
+
+/**
+ * Visitor to create ProgramFlowGraph
+ */
+public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
+
+    private PTreeNode lastNode;
+    private MutableValueGraph<PTreeNode, EdgeTypes> graph = ValueGraphBuilder.directed().build();
+
+    public MutableValueGraph<PTreeNode, EdgeTypes> getGraph() {
+        return graph;
+    }
+
+    @Override
+    public Void visit(ProofScript proofScript) {
+        PTreeNode scriptNode = new PTreeNode(proofScript);
+        lastNode = scriptNode;
+        return this.visit(proofScript.getBody());
+    }
+
+    @Override
+    public Void visit(AssignmentStatement assignment) {
+        PTreeNode node = new PTreeNode(assignment);
+        graph.addNode(node);
+        lastNode = node;
+        return null;
+    }
+
+    @Override
+    public Void visit(Statements statements) {
+        PTreeNode curLastNode = lastNode;
+        for (Statement stmnt : statements) {
+            stmnt.accept(this);
+            graph.putEdgeValue(curLastNode, lastNode, EdgeTypes.STEP_OVER);
+            graph.putEdgeValue(lastNode, curLastNode, EdgeTypes.STEP_BACK);
+            curLastNode = lastNode;
+        }
+        lastNode = curLastNode;
+        return null;
+    }
+}

src/main/java/edu/kit/formal/interpreter/ProofTreeController.java

+package edu.kit.formal.interpreter;
+
+import com.google.common.graph.MutableValueGraph;
+import edu.kit.formal.proofscriptparser.ast.ProofScript;
+
+/**
+ * Class controlling proof tree structure for debugger
+ *
+ * @author S. Grebing
+ */
+public class ProofTreeController {
+
+    private MutableValueGraph<PTreeNode, EdgeTypes> graph;
+
+    private Interpreter currentInterpreter;
+
+
+    private PTreeNode statePointer;
+
+    public ProofTreeController(Interpreter inter, ProofScript mainScript) {
+        this.currentInterpreter = inter;
+        buildEmptyGraph(mainScript);
+
+
+    }
+
+    private void buildEmptyGraph(ProofScript mainScript) {
+        ProgramFlowVisitor visitor = new ProgramFlowVisitor();
+
+        mainScript.accept(visitor);
+        System.out.println(visitor.getGraph());
+
+    }
+
+
+    public PTreeNode stepOver() {
+        return null;
+    }
+
+    public PTreeNode stepBack() {
+        return null;
+    }
+
+    public PTreeNode stepInto() {
+        return null;
+    }
+
+    public PTreeNode stepReturn() {
+        return null;
+    }
+
+
+}

src/main/resources/DebuggerMain.fxml

@@ -69,7 +69,7 @@
                                     </tooltip>
                                 </Button>
 
-                                <Button onAction="#stepOver"
+                                <Button onAction="#stepBack"
                                         disable="${! controller.debugMode}">
                                     <graphic>
                                         <MaterialDesignIconView glyphName="DEBUG_STEP_OVER" size="24.0" scaleX="-1"/>

src/test/resources/edu/kit/formal/interpreter/contraposition/test.kps

+script t(i:int, j:int){
+    i:= 0;
+    j:= 0;
+}
\ No newline at end of file