interim

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

@@ -26,6 +26,8 @@ import edu.kit.iti.formal.psdbg.parser.types.Type;
 import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade;
 import edu.kit.iti.formal.psdbg.termmatcher.Matchings;
 import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
 import org.key_project.util.collection.ImmutableList;
 
 import java.util.*;
@@ -39,6 +41,8 @@ import java.util.regex.Pattern;
  * @author S. Grebing
  */
 public class KeYMatcher implements MatcherApi<KeyData> {
+    private static final Logger LOGGER = LogManager.getLogger(KeYMatcher.class);
+
     private static final Name CUT_TACLET_NAME = new Name("cut");
     private ScriptApi scrapi;
     private KeyInterpreter interpreter;
@@ -244,6 +248,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
         Matchings m = MatcherFacade.matches(data, currentState.getData().getNode().sequent());
 
         if (m.isEmpty()) {
+            LOGGER.error("currentState has no match= " + currentState.getData().getNode().sequent());
             return Collections.emptyList();
         } else {
             Map<String, MatchPath> firstMatch = m.first();
@@ -260,11 +265,11 @@ public class KeYMatcher implements MatcherApi<KeyData> {
                     Value<String> value = toValueTerm(currentState.getData(), matched);
                     va.declare(s, value.getType());
                     va.assign(s, value);
-                    System.out.println("Variable " + s + " : " + value);
+                    LOGGER.error("Variables to match " + s + " : " + value);
                 }
             }
             List<VariableAssignment> retList = new LinkedList();
-            System.out.println("Matched Variables " + va.toString());
+            LOGGER.error("Matched Variables " + va.toString());
             retList.add(va);
             return retList;
         }

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/KeyData.java

 package edu.kit.iti.formal.psdbg.interpreter.data;
 
 import de.uka.ilkd.key.control.KeYEnvironment;
-import de.uka.ilkd.key.java.Label;
 import de.uka.ilkd.key.java.SourceElement;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
@@ -11,7 +10,6 @@ import lombok.*;
 
 import java.util.HashSet;
 import java.util.Set;
-import java.util.function.Function;
 
 /**
  * @author Alexander Weigl
@@ -52,6 +50,7 @@ public class KeyData {
         env = environment;
         this.proof = proof;
         closedNode = proof.closed();
+
     }
 
     public KeyData(Node root, KeYEnvironment environment, Proof proof) {

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

@@ -84,6 +84,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
      * starting point is a statement list
      */
     public void interpret(ProofScript script) {
+        enterScope(script);
         if (stateStack.empty()) {
             throw new InterpreterRuntimeException("no state on stack. call newState before interpret");
         }
@@ -96,6 +97,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         }
 
         script.accept(this);
+        exitScope(script);
     }
 
     /**

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

@@ -32,7 +32,6 @@ public abstract class Blocker {
 
         @Override
         public boolean test(ASTNode node) {
-            Evaluator<T> evaluator = new Evaluator<>(interpreter.getSelectedNode().getAssignments(), interpreter.getSelectedNode());
             for (Breakpoint brkpt : getBreakpoints()) {
                 // check file name
                 if (brkpt.getSourceName().equals(node.getOrigin())) {
@@ -42,6 +41,7 @@ public abstract class Blocker {
                         if (brkpt.getConditionAst() == null) {
                             return true; // no condition ==> trigger
                         } else { // if there is a condition, we check:
+                            Evaluator<T> evaluator = new Evaluator<>(interpreter.getSelectedNode().getAssignments(), interpreter.getSelectedNode());
                             val v = evaluator.eval(brkpt.getConditionAst());
                             if (v.getType() != SimpleType.BOOL)
                                 throw new InterpreterRuntimeException(

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

@@ -134,6 +134,7 @@ public class DebuggerFramework<T> {
     private void run() {
         try {
             interpreter.interpret(mainScript);
+            //dummyproofnode
             succeedListener.accept(this);
         } catch (Exception e) {
             error = e;

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

@@ -36,6 +36,10 @@ public class PTreeNode<T> {
 
     private boolean atomic;
 
+    private boolean isFirstNode = false;
+
+    private boolean isLastNode = false;
+
     @Nullable
     private PTreeNode<T> stepInto;
 

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

@@ -43,6 +43,9 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
     private Consumer<PTreeNode<T>> emitNode = (n) -> {
     };
 
+    @Getter
+    private ProofScript root;
+
     @Nullable
     private PTreeNode<T> lastNode;
 
@@ -74,6 +77,7 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
     }
 
     public void createRoot(ProofScript node) {
+        this.root = node;
         emitNode.accept(createNode(node));
     }
 
@@ -81,6 +85,12 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
         emitNode.accept(createNode(node));
     }
 
+    public void createSentinel() {
+        PTreeNode<T> node = createNode(getRoot());
+        node.setLastNode(true);
+        emitNode.accept(node);
+    }
+
 
     public State<T> getInterpreterStateCopy() {
         return interpreter.getCurrentState().copy();
@@ -145,6 +155,16 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
             return null;
         }
 
+        @Override
+        public Void visit(ProofScript proofScript) {
+            LOGGER.error("exit {}", proofScript.accept(new ShortCommandPrinter()));
+
+            if (proofScript.equals(root)) {
+                createSentinel();
+            }
+            return null;
+        }
+
         @Override
         public Void visit(Statements statements) {
             return null;

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

@@ -971,15 +971,19 @@ public class DebuggerMain implements Initializable {
             ptree.setRoot(pnode);
             ptree.setDeactivateRefresh(true);
 
+
             Set<Node> sentinels = proof.getSubtreeGoals(pnode)
                     .stream()
                     .map(Goal::node)
                     .collect(Collectors.toSet());
             ptree.getSentinels().addAll(sentinels);
+            ptree.expandRootToLeaves();
+            //TODO set coloring of starting and end node
             DockNode node = new DockNode(ptree, "Proof Tree for Step Into: " +
                     original.getStatement().accept(new ShortCommandPrinter())
             );
-            node.dock(dockStation, DockPos.CENTER, getActiveInspectorDock());
+
+            node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea()));
         }
     }
 //endregion

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java

@@ -170,7 +170,7 @@ public class InspectionView extends BorderPane {
 
     public void activate(PTreeNode<KeyData> node, State<KeyData> lastState) {
         InspectionModel im = model.get();
-        im.getGoals().setAll(lastState.getGoals());
+        im.getGoals().setAll(lastState.getGoals()); //TODO nullcheck
         im.setSelectedGoalNodeToShow(lastState.getSelectedGoalNode());
 
         //Experimental

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java

@@ -47,6 +47,8 @@ public class ProofTree extends BorderPane {
     @FXML
     private TreeView<TreeNode> treeProof;
 
+    public void addNodeColor() {
+    }
     private ContextMenu contextMenu;
 
     @Getter @Setter
@@ -123,6 +125,10 @@ public class ProofTree extends BorderPane {
         init();
     }
 
+    public void expandRootToLeaves() {
+        expandRootToLeaves(getTreeProof().getRoot());
+    }
+
     /**
      * From https://www.programcreek.com/java-api-examples/index.php?api=javafx.scene.control.TreeItem
      *
@@ -137,6 +143,9 @@ public class ProofTree extends BorderPane {
         }
     }
 
+    public TreeView<TreeNode> getTreeProof() {
+        return treeProof;
+    }
     private static void expandRootToLeaves(TreeItem candidate) {
         if (candidate != null) {
             if (!candidate.isLeaf()) {
@@ -266,8 +275,7 @@ public class ProofTree extends BorderPane {
             });
 
             MenuItem expandAllNodes = new MenuItem("Expand Tree");
-            expandAllNodes.setOnAction(event -> {
-
+            expandAllNodes.setOnAction((event) -> {
                 expandRootToLeaves(treeProof.getRoot());
             });
 

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps

-script t(){
+script t1(){
     symbex;
-    foreach{
-       simp_heap;
+    cases{
+       case match `?X >= 0,?X > 0  ==>`:
+           cut `?X = 0`[?X \ X];
+           auto;
 
     }
+    //foreach{
+    //    auto;
+    //}
 
 }
 
-script t(){
-    symbex;
-    cases{
-       case match `?X = 0 ==>`:
-            eqSymm on=`?X=0`[];
-
-    }
 
-}
 
-script t1(){
+script t2(){
     symbex;
     cases{
        case match '.*x.*':
@@ -31,3 +28,11 @@ script t1(){
 }
 
 
+script t(){
+    symbex;
+    foreach{
+       simp_heap;
+
+    }
+
+}

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less

@@ -34,7 +34,8 @@
   -fx-background-color: @basenavy;
   -fx-font-family: "Inconsolata", monospace;
   //-fx-font-family: "Fira Code Medium", monospace;
-  -fx-font-size: 12pt;
+  //-fx-font-size: 12pt;
+  -fx-font-size: 18pt;
   -fx-fill: @base00;
 
   .lineno {
@@ -130,7 +131,8 @@
 .breakpoint-menu {
   -fx-skin: "com.sun.javafx.scene.control.skin.ContextMenuSkin";
   -fx-font-family: sans-serif;
-  -fx-font-size: 9pt;
+  //was 9
+  -fx-font-size: 14pt;
 }
 
 
@@ -138,7 +140,8 @@
   -fx-background-color: @basenavy;
   //  -fx-background-color: @base3;
   -fx-font-family: "Inconsolata", monospace;
-  -fx-font-size: 12pt;
+  //-fx-font-size: 12pt;
+  -fx-font-size: 18pt;
   -fx-fill: @base01;
 
 
@@ -233,7 +236,8 @@
 }
 
 .sequent-view {
-  -fx-font-size: 14pt;
+  //-fx-font-size: 14pt;
+  -fx-font-size: 18pt;
   -fx-background-color: @basenavy;
   -fx-fill: black;
 
@@ -244,7 +248,8 @@
 }
 
 .closed-sequent-view {
-  -fx-font-size: 14pt;
+  -fx-font-size: 18pt;
+  //-fx-font-size: 14pt;
   -fx-background-color: @green;
 
   .sequent-highlight {
@@ -256,6 +261,7 @@
 .section-pane {
   .title {
     -fx-font-weight: bold;
+
     -fx-font-size: 14pt;
   }
 
@@ -305,5 +311,6 @@
 .context-menu {
   -fx-skin: "com.sun.javafx.scene.control.skin.ContextMenuSkin";
   -fx-font-family: sans-serif;
-  -fx-font-size: 9pt;
+  -fx-font-size: 12pt;
+  //-fx-font-size: 9pt;
 }