Merge remote-tracking branch 'origin/grebing_luong_workbranch' into grebing_luong_workbranch

rt-key/src/main/java/edu/kit/iti/formal/psdbg/InteractiveCLIDebugger.java

@@ -60,7 +60,7 @@ public class InteractiveCLIDebugger {
         //ControlFlowVisitor cfgVistor = new ControlFlowVisitor(ib.getLookup());
         //MutableValueGraph<ControlFlowNode, ControlFlowTypes> cfg = cfgVistor.getGraph();
 
-        df = new DebuggerFramework<>(interpreter, scripts.get(0), null);
+        df = new DebuggerFramework<>(interpreter, scripts.get(0));
         df.getStatePointerListener().add(this::printNode);
         //df.getBeforeExecutionListener().add(this::printNode);
         //df.getAfterExecutionListener().add(this::end);

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java

 package edu.kit.iti.formal.psdbg.interpreter.dbg;
 
-import com.google.common.graph.MutableValueGraph;
 import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
-import edu.kit.iti.formal.psdbg.interpreter.graphs.ControlFlowNode;
-import edu.kit.iti.formal.psdbg.interpreter.graphs.ControlFlowTypes;
 import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
 import lombok.Getter;
@@ -103,15 +100,14 @@ public class DebuggerFramework<T> {
 
 
     public DebuggerFramework(@Nonnull Interpreter<T> interpreter,
-                             @Nonnull ProofScript main,
-                             MutableValueGraph<ControlFlowNode, ControlFlowTypes> cfg) {
+                             @Nonnull ProofScript main) {
         this.interpreter = interpreter;
         mainScript = main;
         blocker = new BlockListener<>(interpreter);
         breakpointBlocker = new Blocker.BreakpointLine<>(interpreter);
         blocker.getPredicates().add(breakpointBlocker);
         stateWrapper = new StateWrapper<>(interpreter);
-        ptreeManager = new ProofTreeManager<>(cfg);
+        ptreeManager = new ProofTreeManager<>();
         stateWrapper.setEmitNode(ptreeManager::receiveNode);
         interpreterThread = new Thread(this::run);
     }

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java

@@ -34,11 +34,6 @@ public class ProofTreeManager<T> {
             ValueGraphBuilder.directed().allowsSelfLoops(false).build();
     */
 
-    @Getter
-    @Setter
-    @Nullable
-    private final MutableValueGraph<ControlFlowNode, ControlFlowTypes> controlFlowGraph;
-
     @Getter
     private final Set<PTreeNode<T>> nodes = new HashSet<>();
 
@@ -59,8 +54,7 @@ public class ProofTreeManager<T> {
 
     private List<List<PTreeNode<T>>> context = new ArrayList<>(10);
 
-    public ProofTreeManager(MutableValueGraph<ControlFlowNode, ControlFlowTypes> controlFlowGraph) {
-        this.controlFlowGraph = controlFlowGraph;
+    public ProofTreeManager() {
         pushContext();
     }
 

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java

@@ -2,7 +2,6 @@ package edu.kit.iti.formal.psdbg.gui.controller;
 
 import alice.tuprolog.InvalidLibraryException;
 import alice.tuprolog.InvalidTheoryException;
-import antlr.collections.AST;
 import com.google.common.eventbus.Subscribe;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
@@ -36,9 +35,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
 import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
 import edu.kit.iti.formal.psdbg.parser.ASTDiff;
-import edu.kit.iti.formal.psdbg.parser.Facade;
 import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
-import edu.kit.iti.formal.psdbg.parser.ast.CaseStatement;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
 import edu.kit.iti.formal.psdbg.storage.KeyPersistentFacade;
 import javafx.application.Platform;
@@ -61,7 +58,6 @@ import javafx.stage.FileChooser;
 import javafx.stage.Modality;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
-import lombok.val;
 import org.apache.commons.io.FileUtils;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
@@ -75,11 +71,6 @@ import org.reactfx.util.Timer;
 import javax.annotation.Nullable;
 import javax.swing.*;
 import javax.xml.bind.JAXBException;
-import java.awt.event.WindowAdapter;
-import java.awt.event.WindowEvent;
-import java.awt.event.WindowListener;
-import java.awt.event.WindowStateListener;
-import java.awt.im.InputContext;
 import java.io.*;
 import java.net.URL;
 import java.nio.charset.Charset;
@@ -89,8 +80,6 @@ import java.util.*;
 import java.util.concurrent.*;
 import java.util.stream.Collectors;
 
-import org.reactfx.util.Timer;
-
 
 /**
  * Controller for the Debugger MainWindow
@@ -742,7 +731,7 @@ public class DebuggerMain implements Initializable {
 
 
     public void createDebuggerFramework(Collection<? extends Breakpoint> breakpoints, ProofScript ms, boolean addInitBreakpoint, KeyInterpreter interpreter) {
-        DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, ms, null);
+        DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, ms);
         df.setSucceedListener(this::onInterpreterSucceed);
         df.setErrorListener(this::onInterpreterError);
         if (addInitBreakpoint) {

ui/src/test/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTreeTest.java

 package edu.kit.iti.formal.psdbg.gui.controls;
 
+import com.google.common.base.Strings;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
 import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
 import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
-
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
@@ -12,27 +12,28 @@ import edu.kit.iti.formal.psdbg.parser.Facade;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
 import javafx.scene.control.TreeItem;
 import org.antlr.v4.runtime.CharStreams;
-
 import org.junit.Before;
 import org.junit.Test;
 
 import java.io.File;
 import java.io.IOException;
-
 import java.util.List;
 
 public class ProofTreeTest {
-    KeYProofFacade facade;
-    List<ProofScript> scripts;
-    Interpreter<KeyData> i;
-
-
+    private KeYProofFacade facade;
+    private List<ProofScript> scripts;
+    private Interpreter<KeyData> interpreter;
+
+    private static void printTree(TreeItem<ProofTree.TreeNode> rootItem, int level) {
+        System.out.format("%s* %s%n", Strings.repeat(" ", level * 4), rootItem.getValue().label);
+        rootItem.getChildren().forEach(item -> {
+            printTree(item, level+1);
+        });
+    }
 
     @Before
     public void setUp() throws Exception {
-       facade = new KeYProofFacade();
-
-
+        facade = new KeYProofFacade();
     }
 
     @Test
@@ -41,18 +42,19 @@ public class ProofTreeTest {
         facade.loadKeyFileSync(keyProblem);
         scripts = Facade.getAST(CharStreams.fromStream(getClass().getResourceAsStream("proofTreeScript.kps")));
         InterpreterBuilder ib = facade.buildInterpreter();
-        i = ib.build();
-        DebuggerFramework<KeyData> df = new DebuggerFramework<>(i, scripts.get(0), null);
-        i.interpret(scripts.get(0));
+        interpreter = ib.build();
+        DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, scripts.get(0));
+        interpreter.interpret(scripts.get(0));
         ScriptTreeTransformation treeScriptCreation = new ScriptTreeTransformation(df.getPtreeManager(), facade.getProof(), facade.getProof().root());
         treeScriptCreation.create(facade.getProof());
         PTreeNode startNode = df.getPtreeManager().getStartNode();
         if (startNode != null) {
             TreeItem<TreeNode> treeItem = treeScriptCreation.buildScriptTree(startNode);
             System.out.println("treeItem = " + treeItem);
-
         }
 
+        TreeItem<ProofTree.TreeNode> rootItem = treeScriptCreation.create(ib.getProof());
+        printTree(rootItem, 0);
 
     }