Initial Tab for scriptArea

src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java

@@ -7,12 +7,10 @@ package edu.kit.formal.gui;
  */
 
 import de.uka.ilkd.key.util.KeYConstants;
-import edu.kit.formal.gui.controller.DebuggerMainWindowController;
 import javafx.application.Application;
 import javafx.fxml.FXMLLoader;
 import javafx.scene.Parent;
 import javafx.scene.Scene;
-import javafx.scene.SceneBuilder;
 import javafx.stage.Stage;
 
 import java.io.IOException;

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

@@ -10,7 +10,9 @@ import javafx.scene.layout.VBox;
 import lombok.Getter;
 
 /**
- * WozardPane to dosplay all available contracts
+ * WizardPane to display all available contracts
+ * @author S. Grebing
+ * @author A. Weigl
  */
 public class ContractChooser extends Dialog<Contract> {
     @Getter
@@ -52,14 +54,14 @@ public class ContractChooser extends Dialog<Contract> {
         return items.get();
     }
 
-    public ObjectProperty<ObservableList<Contract>> itemsProperty() {
-        return items;
-    }
-
     public void setItems(ObservableList<Contract> items) {
         this.items.set(items);
     }
 
+    public ObjectProperty<ObservableList<Contract>> itemsProperty() {
+        return items;
+    }
+
     private class ContractListCell extends ListCell<Contract> {
         ContractListCell(ListView<Contract> contractListView) {
             itemProperty().addListener((observable, oldValue, newValue) -> render());

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

@@ -18,6 +18,7 @@ import edu.kit.formal.interpreter.data.State;
 import edu.kit.formal.proofscriptparser.Facade;
 import edu.kit.formal.proofscriptparser.ast.ProofScript;
 import javafx.beans.Observable;
+import javafx.beans.binding.StringBinding;
 import javafx.beans.property.SimpleBooleanProperty;
 import javafx.beans.property.SimpleObjectProperty;
 import javafx.beans.value.ObservableBooleanValue;
@@ -55,23 +56,23 @@ import java.util.concurrent.Executors;
  * @author Alexander Weigl
  */
 public class DebuggerMainWindowController implements Initializable {
+    private final PuppetMaster blocker = new PuppetMaster();
     private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false);
-
     private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
-
-
     @FXML
     private Pane rootPane;
     @FXML
     private SplitPane splitPane;
-
     /***********************************************************************************************************
      *      Code Area
      * **********************************************************************************************************/
-    @FXML
-    private ScrollPane scrollPaneCode;
+
     @FXML
     private ScriptArea scriptArea;
+    @FXML
+    private TabPane tabPane;
+    @FXML
+    private Tab startTab;
     /***********************************************************************************************************
      *      MenuBar
      * **********************************************************************************************************/
@@ -98,22 +99,17 @@ public class DebuggerMainWindowController implements Initializable {
     private ExecutorService executorService = Executors.newFixedThreadPool(2);
     private KeYProofFacade facade = new KeYProofFacade();
     private ContractLoaderService contractLoaderService = new ContractLoaderService();
-
     /**
      * Model for the DebuggerController containing the neccessary
      * references to objects needed for controlling backend through UI
      */
     private RootModel model = new RootModel();
-
     @FXML
     private Label lblStatusMessage;
     @FXML
     private Label lblCurrentNodes;
     @FXML
     private Label lblFilename;
-
-    private final PuppetMaster blocker = new PuppetMaster();
-
     private File initialDirectory;
 
     @FXML
@@ -126,6 +122,35 @@ public class DebuggerMainWindowController implements Initializable {
 
     private ObservableBooleanValue executeNotPossible = interpreterService.runningProperty().or(facade.readyToExecuteProperty().not());
 
+    public static void showExceptionDialog(String title, String headerText, String contentText, Throwable ex) {
+        Alert alert = new Alert(Alert.AlertType.ERROR);
+        alert.setTitle(title);
+        alert.setHeaderText(headerText);
+        alert.setContentText(contentText);
+        StringWriter sw = new StringWriter();
+        PrintWriter pw = new PrintWriter(sw);
+        ex.printStackTrace(pw);
+        String exceptionText = sw.toString();
+
+        Label label = new Label("The exception stacktrace was:");
+        TextArea textArea = new TextArea(exceptionText);
+        textArea.setEditable(false);
+        textArea.setWrapText(true);
+
+        textArea.setMaxWidth(Double.MAX_VALUE);
+        textArea.setMaxHeight(Double.MAX_VALUE);
+        GridPane.setVgrow(textArea, Priority.ALWAYS);
+        GridPane.setHgrow(textArea, Priority.ALWAYS);
+
+        GridPane expContent = new GridPane();
+        expContent.setMaxWidth(Double.MAX_VALUE);
+        expContent.add(label, 0, 0);
+        expContent.add(textArea, 0, 1);
+
+        alert.getDialogPane().setExpandableContent(expContent);
+
+        alert.showAndWait();
+    }
 
     /**
      * @param location
@@ -185,8 +210,25 @@ public class DebuggerMainWindowController implements Initializable {
         });
 
         goalView.setCellFactory(GoalNodeListCell::new);
-    }
 
+        startTab.textProperty().bind(new StringBinding() {
+            {
+                super.bind(model.scriptFileProperty());
+            }
+
+            @Override
+            protected String computeValue() {
+                if (model.scriptFileProperty().getValue() != null) {
+                    System.out.println(model.scriptFileProperty());
+                    return model.scriptFileProperty().get().getName();
+                } else {
+                    return "Untitled";
+                }
+            }
+
+        });
+
+    }
 
     //region Actions: Execution
     @FXML
@@ -213,6 +255,7 @@ public class DebuggerMainWindowController implements Initializable {
     public void executeInDebugMode() {
         executeScript(facade.buildInterpreter(), true);
     }
+    //endregion
 
     private void executeScript(InterpreterBuilder ib, boolean debugMode) {
         this.debugMode.set(debugMode);
@@ -235,7 +278,6 @@ public class DebuggerMainWindowController implements Initializable {
             showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
         }
     }
-    //endregion
 
     //region Actions: Menu
     @FXML
@@ -322,7 +364,9 @@ public class DebuggerMainWindowController implements Initializable {
     public void saveProof(ActionEvent actionEvent) {
 
     }
+    //endregion
 
+    //region Santa's Little Helper
 
     @FXML
     protected void loadJavaFile() {
@@ -332,9 +376,6 @@ public class DebuggerMainWindowController implements Initializable {
             contractLoaderService.start();
         }
     }
-    //endregion
-
-    //region Santa's Little Helper
 
     /**
      * Creates a filechooser dialog
@@ -382,6 +423,32 @@ public class DebuggerMainWindowController implements Initializable {
         goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY());
     }
 
+    public KeYProofFacade getFacade() {
+        return facade;
+    }
+
+    //region Property
+    public boolean isDebugMode() {
+        return debugMode.get();
+    }
+    //endregion
+
+    public void setDebugMode(boolean debugMode) {
+        this.debugMode.set(debugMode);
+    }
+
+    public SimpleBooleanProperty debugModeProperty() {
+        return debugMode;
+    }
+
+    public Boolean getExecuteNotPossible() {
+        return executeNotPossible.get();
+    }
+
+    public ObservableBooleanValue executeNotPossibleProperty() {
+        return executeNotPossible;
+    }
+
     public class ContractLoaderService extends Service<List<Contract>> {
         @Override
         protected Task<List<Contract>> createTask() {
@@ -397,7 +464,7 @@ public class DebuggerMainWindowController implements Initializable {
         protected void succeeded() {
             lblStatusMessage.setText("Contract loaded");
             model.getLoadedContracts().setAll(getValue());
-            //FIXME
+            //FIXME model braucht contracts nicht
             ContractChooser cc = new ContractChooser(facade.getService(), model.loadedContractsProperty());
 
             cc.showAndWait().ifPresent(result -> {
@@ -412,54 +479,6 @@ public class DebuggerMainWindowController implements Initializable {
         }
     }
 
-    public KeYProofFacade getFacade() {
-        return facade;
-    }
-
-    public static void showExceptionDialog(String title, String headerText, String contentText, Throwable ex) {
-        Alert alert = new Alert(Alert.AlertType.ERROR);
-        alert.setTitle(title);
-        alert.setHeaderText(headerText);
-        alert.setContentText(contentText);
-        StringWriter sw = new StringWriter();
-        PrintWriter pw = new PrintWriter(sw);
-        ex.printStackTrace(pw);
-        String exceptionText = sw.toString();
-
-        Label label = new Label("The exception stacktrace was:");
-        TextArea textArea = new TextArea(exceptionText);
-        textArea.setEditable(false);
-        textArea.setWrapText(true);
-
-        textArea.setMaxWidth(Double.MAX_VALUE);
-        textArea.setMaxHeight(Double.MAX_VALUE);
-        GridPane.setVgrow(textArea, Priority.ALWAYS);
-        GridPane.setHgrow(textArea, Priority.ALWAYS);
-
-        GridPane expContent = new GridPane();
-        expContent.setMaxWidth(Double.MAX_VALUE);
-        expContent.add(label, 0, 0);
-        expContent.add(textArea, 0, 1);
-
-        alert.getDialogPane().setExpandableContent(expContent);
-
-        alert.showAndWait();
-    }
-    //endregion
-
-    //region Property
-    public boolean isDebugMode() {
-        return debugMode.get();
-    }
-
-    public SimpleBooleanProperty debugModeProperty() {
-        return debugMode;
-    }
-
-    public void setDebugMode(boolean debugMode) {
-        this.debugMode.set(debugMode);
-    }
-
     private class GoalNodeListCell extends ListCell<GoalNode<KeyData>> {
 
         public GoalNodeListCell(ListView<GoalNode<KeyData>> goalNodeListView) {
@@ -481,14 +500,6 @@ public class DebuggerMainWindowController implements Initializable {
         }
     }
 
-    public Boolean getExecuteNotPossible() {
-        return executeNotPossible.get();
-    }
-
-    public ObservableBooleanValue executeNotPossibleProperty() {
-        return executeNotPossible;
-    }
-
     private class InterpretingService extends Service<State<KeyData>> {
         private final SimpleObjectProperty<Interpreter<KeyData>> interpreter = new SimpleObjectProperty<>();
         private final SimpleObjectProperty<ProofScript> mainScript = new SimpleObjectProperty<>();
@@ -511,6 +522,10 @@ public class DebuggerMainWindowController implements Initializable {
         }
 
         private void updateView() {
+            //check proof
+            // check state for empty/error goal nodes leer
+            //currentGoals.set(state.getGoals());
+            //currentSelectedGoal.set(state.getSelectedGoalNode());
             blocker.publishState();
         }
 

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

@@ -10,6 +10,7 @@ import edu.kit.formal.proofscriptparser.ast.*;
 import javafx.application.Platform;
 import javafx.beans.property.SimpleObjectProperty;
 
+import java.util.Collections;
 import java.util.List;
 import java.util.Set;
 import java.util.concurrent.ConcurrentSkipListSet;
@@ -22,17 +23,13 @@ import java.util.concurrent.locks.ReentrantLock;
  * Created by weigl on 21.05.2017.
  */
 public class PuppetMaster {
-    private Interpreter<KeyData> puppet;
-
-    private AtomicInteger stepUntilBlock = new AtomicInteger(-1);
-    private Set<Integer> brkpnts = new ConcurrentSkipListSet<>();
     private final Lock lock = new ReentrantLock();
     private final Condition block = lock.newCondition();
-
     private final SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoals = new SimpleObjectProperty<>();
     private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoal = new SimpleObjectProperty<>();
-
-
+    private Interpreter<KeyData> puppet;
+    private AtomicInteger stepUntilBlock = new AtomicInteger(-1);
+    private Set<Integer> brkpnts = new ConcurrentSkipListSet<>();
     private Visitor<Void> entryListener = new EntryListener();
     private Visitor<Void> exitListener = new ExitListener();
 
@@ -58,6 +55,8 @@ public class PuppetMaster {
     }
 
     public Void checkForHalt(ASTNode node) {
+        System.out.println("node = [" + node + "]");
+        //<0 run
         if (stepUntilBlock.get() > 0)
             stepUntilBlock.decrementAndGet();
 
@@ -76,11 +75,25 @@ public class PuppetMaster {
 
     public void publishState() {
         System.out.println("PuppetMaster.publishState");
-        final State<KeyData> state = puppet.getCurrentState().copy();
-        Platform.runLater(() -> {
-            currentGoals.set(state.getGoals());
-            currentSelectedGoal.set(state.getSelectedGoalNode());
-        });
+        //puppet is null if sucessful interprter state and publish state
+        if (puppet != null) {
+
+            final State<KeyData> state = puppet.getCurrentState().copy();
+            System.out.println(state);
+            Platform.runLater(() -> {
+                currentGoals.set(state.getGoals());
+                currentSelectedGoal.set(state.getSelectedGoalNode());
+            });
+        } else {
+            //if puppet is null an empty state may be reached therefore state get goals etc returns null
+
+            Platform.runLater(() -> {
+                currentGoals.set(Collections.emptyList());
+                currentSelectedGoal.set(null);
+            });
+
+        }
+
     }
 
     /**
@@ -115,26 +128,26 @@ public class PuppetMaster {
         return currentSelectedGoal.get();
     }
 
-    public SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoalProperty() {
-        return currentSelectedGoal;
-    }
-
     public void setCurrentSelectedGoal(GoalNode<KeyData> currentSelectedGoal) {
         this.currentSelectedGoal.set(currentSelectedGoal);
     }
 
-    public List<GoalNode<KeyData>> getCurrentGoals() {
-        return currentGoals.get();
+    public SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoalProperty() {
+        return currentSelectedGoal;
     }
 
-    public SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoalsProperty() {
-        return currentGoals;
+    public List<GoalNode<KeyData>> getCurrentGoals() {
+        return currentGoals.get();
     }
 
     public void setCurrentGoals(List<GoalNode<KeyData>> currentGoals) {
         this.currentGoals.set(currentGoals);
     }
 
+    public SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoalsProperty() {
+        return currentGoals;
+    }
+
     public Set<Integer> getBreakpoints() {
         return brkpnts;
     }

src/main/java/edu/kit/formal/gui/model/RootModel.java

@@ -4,7 +4,6 @@ package edu.kit.formal.gui.model;
 import de.uka.ilkd.key.speclang.Contract;
 import edu.kit.formal.interpreter.data.GoalNode;
 import edu.kit.formal.interpreter.data.KeyData;
-import edu.kit.formal.interpreter.data.State;
 import javafx.beans.property.ListProperty;
 import javafx.beans.property.SimpleListProperty;
 import javafx.beans.property.SimpleObjectProperty;
@@ -19,11 +18,13 @@ import java.io.File;
  * @author S. Grebing
  */
 public class RootModel {
+
     /**
      * Property: current loaded ScriptFile
      */
     private final SimpleObjectProperty<File> scriptFile = new SimpleObjectProperty<>();
 
+
     /**
      * Property: current loaded javaFile
      */
@@ -54,6 +55,7 @@ public class RootModel {
     private final SimpleObjectProperty<Contract> chosenContract = new SimpleObjectProperty<>();
 
     public RootModel() {
+
     }
 
 
@@ -136,12 +138,13 @@ public class RootModel {
         return chosenContract.get();
     }
 
+    public void setChosenContract(Contract chosenContract) {
+        this.chosenContract.set(chosenContract);
+    }
+
     public SimpleObjectProperty<Contract> chosenContractProperty() {
         return chosenContract;
     }
 
-    public void setChosenContract(Contract chosenContract) {
-        this.chosenContract.set(chosenContract);
-    }
 
 }

src/main/java/edu/kit/formal/interpreter/data/State.java

@@ -14,6 +14,8 @@ import java.util.List;
  */
 
 public class State<T> {
+
+
     /**
      * All goalnodes in this state
      */
@@ -31,12 +33,14 @@ public class State<T> {
     @Getter
     private boolean errorState;
 
+
     public State(Collection<GoalNode<T>> goals, GoalNode selected) {
         this.goals = new ArrayList<>(goals);
         this.selectedGoalNode = selected;
         assert selected == null || goals.contains(selected);
     }
 
+
     public State(List<GoalNode<T>> goals, int n) {
         this(goals, goals.get(n));
     }

src/main/resources/DebuggerMain.fxml

@@ -52,6 +52,9 @@
                                     <graphic>
                                         <MaterialDesignIconView glyphName="DEBUG_STEP_INTO" size="24.0"/>
                                     </graphic>
+                                    <tooltip>
+                                        <Tooltip text="Step Into"/>
+                                    </tooltip>
                                 </Button>
 
                                 <Button onAction="#stepOver"
@@ -59,36 +62,54 @@
                                     <graphic>
                                         <MaterialDesignIconView glyphName="DEBUG_STEP_OVER" size="24.0"/>
                                     </graphic>
+                                    <tooltip>
+                                        <Tooltip text="Step Over"/>
+                                    </tooltip>
                                 </Button>
 
+                                <Button onAction="#stepOver"
+                                        disable="${! controller.debugMode}">
+                                    <graphic>
+                                        <MaterialDesignIconView glyphName="DEBUG_STEP_OVER" size="24.0" scaleX="-1"/>
+                                    </graphic>
+                                    <tooltip>
+                                        <Tooltip text="Step Back"/>
+                                    </tooltip>
+                                </Button>
+
+
                                 <Button disable="${! controller.debugMode}">
                                     <graphic>
                                         <MaterialDesignIconView glyphName="DEBUG_STEP_OUT" size="24.0"/>
                                     </graphic>
+                                    <tooltip>
+                                        <Tooltip text="Step Out"/>
+                                    </tooltip>
                                 </Button>
 
                                 <Button disable="${! controller.debugMode}">
                                     <graphic>
                                         <MaterialDesignIconView glyphName="STOP" size="24.0"/>
                                     </graphic>
+                                    <tooltip>
+                                        <Tooltip text="Stop"/>
+                                    </tooltip>
                                 </Button>
                             </items>
                         </ToolBar>
                         <TabPane fx:id="tabPane" side="left"
                                  tabClosingPolicy="SELECTED_TAB" VBox.vgrow="ALWAYS">
                             <tabs>
-                                <Tab text="Script">
+                                <Tab fx:id="startTab" text="Untitled">
                                     <content>
                                         <AnchorPane VBox.vgrow="ALWAYS">
                                             <ScrollPane AnchorPane.rightAnchor="0.0" AnchorPane.bottomAnchor="0.0"
                                                         AnchorPane.leftAnchor="0.0" AnchorPane.topAnchor="0.0"
                                                         fitToWidth="true" fitToHeight="true" hbarPolicy="AS_NEEDED"
-                                                        vbarPolicy="AS_NEEDED">
+                                                        vbarPolicy="ALWAYS">
                                                 <ScriptArea fx:id="scriptArea" VBox.vgrow="ALWAYS"/>
                                             </ScrollPane>
                                         </AnchorPane>
-
-
                                     </content>
                                 </Tab>
                             </tabs>

src/test/resources/edu/kit/formal/proofscriptparser/badexpr.txt

@@ -7,13 +7,10 @@ not (match `d5'` using [ pi:int, isLess :bool, khar:term] -> false | k < b3o ) -
 case p:=true :{x:=x+1;}case p=false :{x:=x-1;}
 case q=(r&s) :{   y:=2*x-d;}case q!=(r&s) {   y:=3*x+d;}
 case p=(q|b) :b:=p<=>q;	s:=true;case p=not(q|b) :{   b:=r<=>d;    s:=false;}
-// q := t this should raise a syntax error because ; is missing
 repeat{   k:=k+1; auto;
 repeat{   theonly{   puD:int := ie4+41-iZ;}cmd1;} //linter?
 case{   cases a>gh :{   repeat{   a := a*b+1;df:= 5*fd-df;}}default :{   cf:=a>df;}}
-//2pF:int //should raise a syntax error, ids are not allowed to start with a number
 cases{   case dl=true:{   ft:=true;}case dl=false:{   ft:=sp&rd; }};
-//symbex //; is missing
 call sCmd5;;
 script test(aX:int; aY:int){}
 ;