bug fix

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

@@ -236,7 +236,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         return null;
     }
 
-   /* @Override
+    @Override
     public Object visit(SimpleCaseStatement simpleCaseStatement) {
         Expression matchExpression = simpleCaseStatement.getGuard();
         State<T> currentStateToMatch = peekState();
@@ -250,7 +250,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         } else {
             return false;
         }
-    }*/
+    }
 
     @Override
     public Object visit(TryCase TryCase) {

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

@@ -58,21 +58,6 @@ public class State<T> {
         return goals;
     }
 
-    public GoalNode<T> getSelectedGoalNode() {
-        if (selectedGoalNode == null) {
-            throw new IllegalStateException("no selected node");
-        } else {
-            if (getGoals().size() == 1) {
-                selectedGoalNode = getGoals().get(0);
-            }
-            return selectedGoalNode;
-        }
-    }
-
-    public void setSelectedGoalNode(GoalNode<T> gn) {
-        this.selectedGoalNode = gn;
-    }
-
     /**
      * Deep Copy state
      *
@@ -81,17 +66,43 @@ public class State<T> {
     public State<T> copy() {
         List<GoalNode<T>> copiedGoals = new ArrayList<>();
         GoalNode<T> refToSelGoal = null;
-
-        for (GoalNode<T> goal : goals) {
-            GoalNode<T> deepcopy = goal.deepCopy();
+        if (goals.size() == 1) {
+            GoalNode<T> deepcopy = goals.get(0).deepCopy();
+            refToSelGoal = deepcopy;
             copiedGoals.add(deepcopy);
-            if (goal.equals(getSelectedGoalNode())) {
-                refToSelGoal = deepcopy;
+        } else {
+            for (GoalNode<T> goal : goals) {
+                GoalNode<T> deepcopy = goal.deepCopy();
+                copiedGoals.add(deepcopy);
+
+                if (selectedGoalNode != null && goal.equals(getSelectedGoalNode())) {
+                    refToSelGoal = deepcopy;
+                }
             }
         }
         return new State<T>(copiedGoals, refToSelGoal);
     }
 
+    public void setSelectedGoalNode(GoalNode<T> gn) {
+        this.selectedGoalNode = gn;
+    }
+
+    public GoalNode<T> getSelectedGoalNode() {
+     /*   if (selectedGoalNode == null) {
+            throw new IllegalStateException("no selected node");
+        } else {
+            if (getGoals().size() == 1) {
+                selectedGoalNode = getGoals().get(0);
+            }
+            return selectedGoalNode;
+        }*/
+
+        if (getGoals().size() == 1) {
+            selectedGoalNode = getGoals().get(0);
+        }
+        return selectedGoalNode;
+    }
+
     public String toString() {
         if (selectedGoalNode == null) {
             return "No Goal selected";

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

@@ -9,7 +9,6 @@ import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.interpreter.exceptions.StateGraphException;
 import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
-import edu.kit.iti.formal.psdbg.parser.Visitor;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
 import javafx.application.Platform;
 import javafx.beans.property.SimpleObjectProperty;
@@ -269,6 +268,7 @@ public class StateGraphWrapper<T> {
         changeListeners.forEach(list -> {
             Platform.runLater(() -> {
                 list.graphChanged(nodeAddedEvent);
+                System.out.println("New StateGraphChange " + this.asdot());
             });
         });
 
@@ -310,11 +310,11 @@ public class StateGraphWrapper<T> {
             return createNewNode(casesStatement);
         }
 
-        @Override
-        public Void visit(CaseStatement caseStatement) {
-            return createNewNode(caseStatement);
-        }
-
+        /* @Override
+         public Void visit(CaseStatement caseStatement) {
+             return createNewNode(caseStatement);
+         }
+         */
         @Override
         public Void visit(CallStatement call) {
             return createNewNode(call);
@@ -334,6 +334,21 @@ public class StateGraphWrapper<T> {
         public Void visit(RepeatStatement repeatStatement) {
             return createNewNode(repeatStatement);
         }
+
+        @Override
+        public Void visit(TryCase tryCase) {
+            return createNewNode(tryCase);
+        }
+
+        @Override
+        public Void visit(SimpleCaseStatement simpleCaseStatement) {
+            return createNewNode(simpleCaseStatement);
+        }
+
+        @Override
+        public Void visit(ClosesCase closesCase) {
+            return createNewNode(closesCase);
+        }
     }
 
     private class ExitListener extends DefaultASTVisitor<Void> {
@@ -347,10 +362,10 @@ public class StateGraphWrapper<T> {
             return addState(casesStatement);
         }
 
-        @Override
+        /*@Override
         public Void visit(CaseStatement caseStatement) {
             return addState(caseStatement);
-        }
+        }*/
 
         @Override
         public Void visit(CallStatement call) {
@@ -372,6 +387,20 @@ public class StateGraphWrapper<T> {
             return addState(repeatStatement);
         }
 
+        @Override
+        public Void visit(TryCase tryCase) {
+            return addState(tryCase);
+        }
+
+        @Override
+        public Void visit(SimpleCaseStatement simpleCaseStatement) {
+            return addState(simpleCaseStatement);
+        }
+
+        @Override
+        public Void visit(ClosesCase closesCase) {
+            return addState(closesCase);
+        }
        /* @Override
         public Void visit(ProofScript proofScript) {
             return addState(proofScript);

ui/src/main/java/edu/kit/iti/formal/psdbg/InterpretingService.java

@@ -69,7 +69,7 @@ public class InterpretingService extends Service<State<KeyData>> {
         //check state for empty/error goal nodes
         //currentGoals.set(state.getGoals());
         //currentSelectedGoal.set(state.getSelectedGoalNode());
-
+        System.out.println("Updating View");
         blocker.publishState();
     }
 

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/JavaExample.java

@@ -13,6 +13,12 @@ import java.nio.charset.Charset;
  * @author Alexander Weigl
  */
 public class JavaExample extends Example {
+
+
+    public void setJavaFile(URL javaFile) {
+        this.javaFile = javaFile;
+    }
+
     protected URL javaFile;
 
     @Override
@@ -23,9 +29,12 @@ public class JavaExample extends Example {
         try {
             File script = newTempFile(scriptFile, getName() + ".kps");
             debuggerMain.openScript(script);
-            File key = newTempFile(keyFile, "problem.key");
+
+            //File key = newTempFile(keyFile, "project.key");
             File java = newTempFile(javaFile, getName() + ".java");
-            debuggerMain.openKeyFile(key);
+            //System.out.println(java.getAbsolutePath());
+            //debuggerMain.openKeyFile(key);
+            debuggerMain.openJavaFile(java);
             if (helpText != null) {
                 String content = IOUtils.toString(helpText, Charset.defaultCharset());
                 debuggerMain.openNewHelpDock(getName() + " Example", content);

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/JavaSimpleExample.java

+package edu.kit.iti.formal.psdbg.examples.java;
+
+import edu.kit.iti.formal.psdbg.examples.JavaExample;
+
+public class JavaSimpleExample extends JavaExample {
+
+    public JavaSimpleExample() {
+        setName("Test");
+        setJavaFile(this.getClass().getResource("Test.java"));
+
+
+        defaultInit(getClass());
+
+        System.out.println(this);
+    }
+}

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

@@ -190,7 +190,7 @@ public class DebuggerMain implements Initializable {
             //System.out.println("Pos: "+newValue.getData().getNode().getNodeInfo().getActiveStatement().getPositionInfo());
         });
 
-        //TODO nullpointer
+
         proofTreeController.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> {
             if (newValue != null) {
                 scriptController.getDebugPositionHighlighter().highlight(newValue);
@@ -211,16 +211,7 @@ public class DebuggerMain implements Initializable {
     }
 
     public void marriageJavaCode() {
-        /*javaFileProperty().addListener((observable, oldValue, newValue) -> {
-            showCodeDock(null);
-            try {
-                String code = FileUtils.readFileToString(newValue, Charset.defaultCharset());
-                javaCode.set(code);
-            } catch (IOException e) {
-                e.printStackTrace();
-            }
-        });*/
-
+        //Listener on chosenContract from
         chosenContract.addListener(o -> {
             //javaCode.set(Utils.getJavaCode(chosenContract.get()));
             try {

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

@@ -129,7 +129,9 @@ public class ProofTreeController {
         //this.currentSelectedGoal.bindBidirectional(blocker.currentSelectedGoalProperty());
         blocker.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> {
             Platform.runLater(() -> {
-                this.setCurrentSelectedGoal(newValue);
+                if (newValue != null) {
+                    this.setCurrentSelectedGoal(newValue);
+                }
             });
         });
         blocker.currentGoalsProperty().addListener((observable, oldValue, newValue) -> {
@@ -156,7 +158,9 @@ public class ProofTreeController {
      */
     private void setNewState(State<KeyData> state) {
         setCurrentGoals(state == null ? null : state.getGoals());
-        setCurrentSelectedGoal(state == null ? null : state.getSelectedGoalNode());
+
+        setCurrentSelectedGoal(state == null ? null : (state.getSelectedGoalNode() == null ? null : state.getSelectedGoalNode()));
+
         setCurrentHighlightNode(statePointer.getScriptstmt());
         LOGGER.debug("New State from this command: {}@{}",
                 this.statePointer.getScriptstmt().getNodeName(),

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

@@ -100,8 +100,23 @@ public class PuppetMaster {
 
             Platform.runLater(() -> {
 
-                currentGoals.set(state.getGoals());
-                currentSelectedGoal.set(state.getSelectedGoalNode());
+
+                //filter whether all goals are closed
+                Object[] arr = state.getGoals().stream().filter(keyDataGoalNode -> !keyDataGoalNode.isClosed()).toArray();
+
+                if (state.getSelectedGoalNode() == null) {
+                    if (arr.length == 0) {
+                        currentGoals.set(Collections.emptyList());
+                        //currentSelectedGoal.set(state.getGoals().get(0));
+                        currentSelectedGoal.set(null);
+                    } else {
+                        currentGoals.set(state.getGoals());
+                        currentSelectedGoal.set(null);
+                    }
+                } else {
+                    currentGoals.set(state.getGoals());
+                    currentSelectedGoal.set(state.getSelectedGoalNode());
+                }
 
             });
         } else {

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

@@ -228,16 +228,6 @@ public class ScriptArea extends CodeArea {
         if (hasExecutionMarker()) {
             System.out.println("getExecutionMarkerPosition() = " + getExecutionMarkerPosition());
 
- /*           getStyleSpans(0, getExecutionMarkerPosition()).stream()
-                    .map(span -> {
-                        Collection<String> style = span.getStyle();
-                        if (style.isEmpty()) {
-                            Collections.singleton("NON_EXE_AREA");
-                        } else {
-                            style.add("NON_EXE_AREA");
-                        }
-                        return style;
-                    });*/
 
             UnaryOperator<Collection<String>> styleMapper = strings -> {
                 if (strings.isEmpty()) {
@@ -252,11 +242,11 @@ public class ScriptArea extends CodeArea {
             setStyleSpans(0, getStyleSpans(0, getExecutionMarkerPosition()).mapStyles(styleMapper));
 
 
+            //this results in a NotSupportedOperation Exception because the add to an immutable list is not allowed
            /* getStyleSpans(0, getExecutionMarkerPosition()).forEach(span -> {
                 Collection<String> style = span.getStyle();
                 if (style.isEmpty()) {
-                    style.add("NON_EXE_AREA");
-                    //setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA"));
+                    setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA"));
                 } else {
                     style.add("NON_EXE_AREA");
                 }

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

@@ -5,8 +5,6 @@ import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
 import javafx.event.ActionEvent;
 import javafx.scene.layout.AnchorPane;
 
-import java.io.File;
-
 /**
  * Welcome pane that allows for a more usable entry point
  * Created by weigl on 7/7/17.
@@ -40,11 +38,16 @@ public class WelcomePane extends AnchorPane {
     public void loadJavaTest(ActionEvent event) {
         proofScriptDebugger.getWelcomePaneDock().close();
         proofScriptDebugger.showActiveInspector(null);
-        proofScriptDebugger.openScript(
+        Examples.loadExamples().forEach(example -> {
+            if (example.getName().equals("Test"))
+                example.open(proofScriptDebugger);
+
+        });
+       /* proofScriptDebugger.openScript(
                 new File("src/test/resources/edu/kit/formal/psdb/interpreter/javaExample/test.kps")
         );
         proofScriptDebugger.openJavaFile(
-                new File("src/test/resources/edu/kit/formal/psdb/interpreter/javaExample/Test.java"));
+                new File("src/test/resources/edu/kit/formal/psdb/interpreter/javaExample/Test.java"));*/
     }
 
     public void loadHelpPage(ActionEvent event) {

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java

@@ -28,6 +28,7 @@ public class InspectionModel {
     private final BooleanProperty isInterpreterTab = new SimpleBooleanProperty();
     private ObjectProperty<Mode> mode = new SimpleObjectProperty<>();
 
+
     public GoalNode<KeyData> getCurrentInterpreterGoal() {
         return currentInterpreterGoal.get();
     }

ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example

 edu.kit.iti.formal.psdbg.examples.contraposition.ContrapositionExample
-edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample
\ No newline at end of file
+edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample
+edu.kit.iti.formal.psdbg.examples.java.JavaSimpleExample
\ No newline at end of file

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/Test.java

+public class Test{
+
+
+
+    /*@ public normal_behavior
+      @ requires x >= 0;
+      @ ensures \result >0;
+      @*/
+    public int foo(int x){
+        if(x > 0){
+            x--;
+        }else{
+            x++;
+        }
+        return x++;
+    }
+}
\ No newline at end of file

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/help.html

+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="UTF-8">
+    <title>Java Simple Test Example</title>
+    This is a simple Java example.
+</head>
+<body>
+
+</body>
+</html>
\ No newline at end of file

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/project.key

+
+
+\javaSource "";
+\chooseContract
\ No newline at end of file

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

+script t1(){
+    symbex;
+    cases{
+       case match '.*x.*':
+            auto;
+
+	   default:
+	       auto;
+
+    }
+
+}
+
+

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

@@ -7,13 +7,17 @@
 @base2: rgb(238, 232, 213);
 @base3: rgb(253, 246, 227);
 @yellow: rgb(181, 137, 0);
-@orange: rgb(203, 75, 22);
+@orange: rgb(203, 133, 91);
 @red: rgb(220, 50, 47);
 @magenta: rgb(211, 54, 130);
 @violet: rgb(108, 113, 196);
 @blue: rgb(38, 139, 210);
 @cyan: rgb(42, 161, 152);
-@green: rgb(133, 153, 0);
+@green: rgb(38, 187, 108);
+@basenavy: #f6f8ff;
+@keywordColor: #200080;
+@stringliteralColor: #6679aa;
+@integerLiteralColor: #008c00;
 
 .solarized-dark() {
   background-color: @base03;
@@ -26,8 +30,10 @@
 }
 
 .script-area {
-  -fx-background-color: @base3;
-  -fx-font-family: "Fira Code Medium", monospace;
+  //-fx-background-color: @base3;
+  -fx-background-color: @basenavy;
+  -fx-font-family: "Inconsolata", monospace;
+  //-fx-font-family: "Fira Code Medium", monospace;
   -fx-font-size: 12pt;
   -fx-fill: @base00;
 
@@ -53,7 +59,8 @@
   // Structures
   .FOREACH, .CASES, .CASE, .DEFAULT
   .THEONLY, .SCRIPT, .USING, .REPEAT {
-    -fx-fill: @blue;
+    // -fx-fill: @blue;
+    -fx-fill: @keywordColor;
     -fx-font-weight: bold;
   }
 
@@ -73,7 +80,8 @@
   }
 
   .DIGITS, .TRUE, .FALSE {
-    -fx-fill: @orange;
+    -fx-fill: @integerLiteralColor;
+    //-fx-fill: @orange;
   }
 
   .TERM_LITERAL {
@@ -81,7 +89,8 @@
   }
 
   .STRING_LITERAL {
-    -fx-fill: @violet;
+    -fx-fill: @stringliteralColor;
+    //-fx-fill: @violet;
   }
 
   .SINGLE_LINE_COMMENT, .MULTI_LINE_COMMENT {
@@ -103,7 +112,7 @@
   }
 
   .line-highlight-postmortem {
-    -rtfx-background-color: @blue;
+    -rtfx-background-color: @cyan;
   }
 
   .line-unhighlight {
@@ -126,8 +135,10 @@
 
 
 .java-area {
-  -fx-background-color: @base3;
-  -fx-font-family: "Fira Code Medium", monospace;
+  -fx-background-color: @basenavy;
+  //  -fx-background-color: @base3;
+  -fx-font-family: "Inconsolata", monospace;
+  //-fx-font-family: "Fira Code Medium", monospace;
   -fx-font-size: 12pt;
   -fx-fill: @base01;
 
@@ -138,7 +149,8 @@
   .INTERFACE, .LONG, .NATIVE, .NEW, .PACKAGE, .PRIVATE, .PROTECTED, .PUBLIC, .RETURN,
   .SHORT, .STATIC, .STRICTFP, .SUPER, .SWITCH, .SYNCHRONIZED, .THIS, .THROW, .THROWS,
   .TRANSIENT, .TRY, .VOID, .VOLATILE, .WHILE {
-    -fx-fill: darkgreen;
+    //-fx-fill: darkgreen;
+    -fx-fill: @keywordColor;
     -fx-font-weight: bold;
   }
 
@@ -157,17 +169,20 @@
   }
 
   .INTEGER_LITERAL {
-    -fx-fill: @blue;
+    -fx-fill: @integerLiteralColor;
+    //-fx-fill: @blue;
   }
 
   .StringLiteral, .CharacterLiteral {
-    -fx-fill: @green;
+    //-fx-fill: @green;
+    -fx-fill: @stringliteralColor;
     -fx-font-smoothing-type: lcd;
   }
 
   .LINE_COMMENT, .COMMENT {
     -fx-fill: @base01;
-    -fx-font-family: "Fira Code Light";
+    //-fx-font-family:  "Fira Code Light", monospace;
+    -fx-font-family: "Inconsolata", monospace;
   }
 
   .Identifier {
@@ -180,10 +195,10 @@
     -fx-underline: true;
   }
   .line-highlight {
-    -rtfx-background-color: @blue;
+    -rtfx-background-color: @cyan;
   }
     .line-un-highlight {
-      -rtfx-background-color: @base3;
+      -rtfx-background-color: @basenavy;
     }
 
 }
@@ -191,7 +206,7 @@
 /**********************************************************************************************************************/
 
 .problem-popup {
-  -fx-background-color: @base03;
+  -fx-background-color: @basenavy;
   -fx-text-fill: @base3;
   -fx-text-alignment: center;
   -fx-wrap-text: true;
@@ -222,7 +237,7 @@
 
 .sequent-view {
   -fx-font-size: 14pt;
-  -fx-background-color: @base2;
+  -fx-background-color: @basenavy;
   -fx-fill: black;
 
   .sequent-highlight {