Merge remote-tracking branch 'remotes/origin/luonng_variableAssignment' into...

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

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

@@ -148,8 +148,6 @@ public class KeyInterpreter extends Interpreter<KeyData> {
     }
 
 
-
-
     @Override
     public Object visit(LetStatement let) {
         enterScope(let);

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

@@ -122,6 +122,9 @@ public class KeyData {
         return programStatementsLabel;
     }
 
+    public void getVarAssignment() {
+
+    }
 
     public Goal getGoal() {
         return goal;

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

@@ -148,6 +148,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         Variable var = assignmentStatement.getLhs();
         Expression expr = assignmentStatement.getRhs();
         if (t != null) {
+            System.out.println("t = " + t+ var);
             node.declareVariable(var, t);
         }
 
@@ -160,6 +161,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
                 if (fireVariableAssignmentHook(node, var.getIdentifier(), v)) {
                     node.setVariableValue(var, v);
                 }
+                System.out.println("v = " + v);
                 node.setVariableValue(var, v);
             }
         }

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

@@ -58,8 +58,8 @@ public class GoalNode<T> {
         this.id = id;
     }
 
-    private GoalNode(int id, GoalNode<T> parent, VariableAssignment ass, T data, boolean isClosed) {
-        this(parent, ass, data, isClosed);
+    private GoalNode(int id, GoalNode<T> parent, VariableAssignment varas, T data, boolean isClosed) {
+        this(parent, varas, data, isClosed);
         this.id = id;
     }
 
@@ -68,6 +68,12 @@ public class GoalNode<T> {
         this.isClosed = isClosed;
         this.id = id;
     }
+    private GoalNode(int id, VariableAssignment ass, T data, boolean isClosed) {
+        this(data);
+        this.assignments = ass;
+        this.isClosed = isClosed;
+        this.id = id;
+    }
 
     /**
      * @param varname
@@ -137,11 +143,13 @@ public class GoalNode<T> {
      * @return
      */
     public GoalNode<T> deepCopy() {
+        VariableAssignment deepCopy = assignments.deepCopy();
+
         if (parent != null) {
-            VariableAssignment deepCopy = parent.assignments.deepCopy();
             return new GoalNode<T>(id, parent.deepCopy(), deepCopy, data, isClosed);
         } else {
-            return new GoalNode<T>(id, data, isClosed);
+
+            return new GoalNode<T>(id, deepCopy, data, isClosed);
         }
     }
 

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

@@ -186,6 +186,7 @@ public class InteractiveModeController {
 
     public void stop() {
         Events.unregister(this);
+        //TODO: casesstatement visiten
         String c = getCasesAsString();
         scriptController.getDockNode(scriptArea).undock();
 

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

@@ -2,14 +2,18 @@ package edu.kit.iti.formal.psdbg.gui.controls;
 
 import com.google.common.collect.BiMap;
 import com.google.common.collect.HashBiMap;
+import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
+import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import javafx.beans.property.ObjectProperty;
 import javafx.beans.property.SimpleObjectProperty;
+import javafx.event.ActionEvent;
+import javafx.event.EventHandler;
 import javafx.fxml.FXML;
-import javafx.scene.control.ContextMenu;
-import javafx.scene.control.RadioMenuItem;
-import javafx.scene.control.Toggle;
-import javafx.scene.control.ToggleGroup;
+import javafx.scene.Scene;
+import javafx.scene.control.*;
+import javafx.stage.Stage;
+import lombok.Setter;
 
 import java.util.function.Function;
 
@@ -20,10 +24,17 @@ public class GoalOptionsMenu extends ContextMenu {
     @FXML
     private RadioMenuItem rmiShowSequent, rmiCFL, rmiCFS, rmiBranchLabels, rmiNodeNames, rmiRuleNames;
 
+    @FXML
+    private MenuItem showVarAssignment;
+
+    @Setter
+    private InspectionModel model;
+
     private ObjectProperty<ViewOption> selectedViewOption = new SimpleObjectProperty<>();
 
     private BiMap<Toggle, ViewOption> optionMap = HashBiMap.create(6);
 
+
     public GoalOptionsMenu() {
         Utils.createWithFXML(this);
 
@@ -44,6 +55,27 @@ public class GoalOptionsMenu extends ContextMenu {
         });
 
         selectedViewOption.setValue(ViewOption.SEQUENT);
+
+        showVarAssignment.setOnAction(new EventHandler<ActionEvent>() {
+            @Override
+            public void handle(ActionEvent event) {
+
+                if(model == null || model.getSelectedGoalNodeToShow() == null) {
+                    Utils.showInfoDialog("Select a goal", "Select a goal", "Please select a goal first.");
+                    return;
+                }
+                VariableAssignment var_assignm = model.getSelectedGoalNodeToShow().getAssignments();
+
+                Stage stage = new Stage();
+                stage.setTitle("Variable Assignment");
+                VariableAssignmentWindow vaw = new VariableAssignmentWindow(var_assignm);
+
+                Scene scene = new Scene(vaw);
+                stage.setScene(scene);
+
+                stage.show();
+            }
+        });
     }
 
 
@@ -55,9 +87,6 @@ public class GoalOptionsMenu extends ContextMenu {
         return selectedViewOption;
     }
 
-    public void setSelectedViewOption(ViewOption selectedViewOption) {
-        this.selectedViewOption.set(selectedViewOption);
-    }
 
     public enum ViewOption {
         BRANCHING(KeyData::getBranchingLabel),
@@ -67,6 +96,7 @@ public class GoalOptionsMenu extends ContextMenu {
         NAME(KeyData::getNameLabel),
         SEQUENT(item -> item.getNode().sequent().toString());
 
+
         private final Function<KeyData, String> projection;
 
         ViewOption(Function<KeyData, String> toString) {
@@ -77,4 +107,6 @@ public class GoalOptionsMenu extends ContextMenu {
             return projection.apply(item);
         }
     }
+
+
 }
\ No newline at end of file

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

@@ -138,6 +138,8 @@ public class InspectionView extends BorderPane {
         Utils.addDebugListener(model.get().currentInterpreterGoalProperty());
         Utils.addDebugListener(model.get().highlightedJavaLinesProperty());
 
+        goalOptionsMenu.setModel(model.get());
+
         /*TODO redefine CSS bases on selected mode
         mode.addListener(o -> {
             getStyleClass().removeAll(

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

@@ -25,6 +25,7 @@ import javafx.scene.control.ListView;
 import javafx.scene.control.TextArea;
 import javafx.scene.input.MouseEvent;
 import javafx.scene.layout.BorderPane;
+import lombok.Getter;
 import org.controlsfx.control.StatusBar;
 
 import java.util.HashMap;
@@ -40,6 +41,8 @@ public class SequentMatcher extends BorderPane {
     private final ListProperty<Map<String, MatchPath>> results = new SimpleListProperty<>(this, "results", FXCollections.observableArrayList());
     //sicht user selected
     private final ObjectProperty<GoalNode<KeyData>> selectedGoalNodeToShow = new SimpleObjectProperty<>(this, "selectedGoalNodeToShow");
+
+    @Getter
     public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
     @FXML
     private SequentViewForMatcher sequentView;
@@ -97,6 +100,7 @@ public class SequentMatcher extends BorderPane {
 
             }
         });
+
     }
 
     private void calculateLookupTable() {

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

@@ -2,6 +2,7 @@ package edu.kit.iti.formal.psdbg.gui.controls;
 
 import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
+import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import javafx.event.ActionEvent;
 import javafx.event.EventHandler;
 import javafx.fxml.FXML;
@@ -18,6 +19,8 @@ public class SequentOptionsMenu extends ContextMenu {
     private MenuItem openSequentMatcher;
 
 
+
+
     public SequentOptionsMenu(InspectionModel model) {
         Utils.createWithFXML(this);
         this.model = model;
@@ -31,6 +34,9 @@ public class SequentOptionsMenu extends ContextMenu {
 
                     KeyData data = (KeyData) model.getSelectedGoalNodeToShow().getData();
                     SequentMatcher root1 = new SequentMatcher(data.getProof().getServices());
+
+                    root1.getGoalOptionsMenu().setModel(model);
+
                     root1.setGoals(model.getGoals());
                     root1.setSelectedGoalNodeToShow(model.getSelectedGoalNodeToShow());
                     root1.getStyleClass().add("sequent-view");
@@ -58,6 +64,8 @@ public class SequentOptionsMenu extends ContextMenu {
             }
         });
 
+
+
     }
 
 

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

+package edu.kit.iti.formal.psdbg.gui.controls;
+
+import alice.tuprolog.Var;
+import edu.kit.iti.formal.psdbg.gui.controls.Utils;
+import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
+import edu.kit.iti.formal.psdbg.interpreter.assignhook.DefaultAssignmentHook;
+import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
+import edu.kit.iti.formal.psdbg.parser.ast.Variable;
+import edu.kit.iti.formal.psdbg.parser.types.Type;
+import javafx.beans.Observable;
+import javafx.beans.property.SimpleStringProperty;
+import javafx.collections.FXCollections;
+import javafx.collections.ObservableList;
+import javafx.fxml.FXML;
+import javafx.scene.control.TabPane;
+import javafx.scene.control.TableColumn;
+import javafx.scene.control.TableView;
+import javafx.scene.control.cell.PropertyValueFactory;
+import javafx.scene.layout.BorderPane;
+import lombok.Getter;
+import lombok.Setter;
+
+import java.util.Collection;
+import java.util.Collections;
+import java.util.Map;
+
+
+public class VariableAssignmentWindow extends TabPane {
+    @FXML
+    TableView declarative_tableView;
+
+    @FXML
+    TableView special_tableView;
+
+
+    /** Non special Variables that don't start with __ **/
+    private ObservableList<VariableModel> declarativeModel;
+
+    /** Variables that start with __ **/
+    private ObservableList<VariableModel> specialModel;
+
+    public VariableAssignmentWindow(VariableAssignment assignment) {
+
+        Utils.createWithFXML(this);
+
+        if (assignment != null) {
+            fillInVariableModelsLists(assignment);
+        }
+
+        declarative_tableView.setEditable(false);
+        special_tableView.setEditable(false);
+
+        //Table Colums for declarative_tableView
+        TableColumn decl_varCol = new TableColumn("Variable");
+        TableColumn decl_typeCol = new TableColumn("Type");
+        TableColumn decl_valCol = new TableColumn("Value");
+
+        //Set Colums width proportional to windows with
+        decl_varCol.prefWidthProperty().bind(declarative_tableView.widthProperty().divide(3));
+        decl_typeCol.prefWidthProperty().bind(declarative_tableView.widthProperty().divide(3));
+        decl_valCol.prefWidthProperty().bind(declarative_tableView.widthProperty().divide(3));
+
+        decl_varCol.setCellValueFactory(
+                new PropertyValueFactory<VariableModel,String>("varname")
+        );
+        decl_typeCol.setCellValueFactory(
+                new PropertyValueFactory<VariableModel,String>("vartype")
+        );
+        decl_valCol.setCellValueFactory(
+                new PropertyValueFactory<VariableModel,String>("varval")
+        );
+
+        declarative_tableView.setItems(declarativeModel);
+        declarative_tableView.getColumns().addAll(decl_varCol, decl_typeCol, decl_valCol);
+
+        //Table Colums for special_tableView
+        TableColumn spec_varCol = new TableColumn("Variable");
+        TableColumn spec_typeCol = new TableColumn("Type");
+        TableColumn spec_valCol = new TableColumn("Value");
+
+        //Set Colums width proportional to windows with
+        spec_varCol.prefWidthProperty().bind(special_tableView.widthProperty().divide(3));
+        spec_typeCol.prefWidthProperty().bind(special_tableView.widthProperty().divide(3));
+        spec_valCol.prefWidthProperty().bind(special_tableView.widthProperty().divide(3));
+
+        spec_varCol.setCellValueFactory(
+                new PropertyValueFactory<VariableModel,String>("varname")
+        );
+        spec_typeCol.setCellValueFactory(
+                new PropertyValueFactory<VariableModel,String>("vartype")
+        );
+        spec_valCol.setCellValueFactory(
+                new PropertyValueFactory<VariableModel,String>("varval")
+        );
+
+        special_tableView.setItems(specialModel);
+        special_tableView.getColumns().addAll(spec_varCol, spec_typeCol, spec_valCol);
+
+        // TODO: set css for TableView
+
+        //declarative_tableView.getStyleClass().add("table_view");
+
+
+}
+
+    /**
+     * Combine all previous Variableassignments and return it
+     * @param assignment
+     */
+    private void fillInVariableModelsLists(VariableAssignment assignment) {
+        ObservableList<VariableModel> varmodel = FXCollections.observableArrayList();
+        ObservableList<VariableModel> special_varmodel = FXCollections.observableArrayList();
+        VariableAssignment current = assignment;
+
+
+        while (current != null) {
+
+            final VariableAssignment currentcopy = current;
+            //iterate over types map
+            currentcopy.getTypes().forEach((k, v) -> {
+                VariableModel variableModel = new VariableModel(k.getIdentifier(), v.symbol(), currentcopy.getValue(k).getData().toString());
+
+                if (variableModel.getVarname().startsWith("__")) {
+                    if (!special_varmodel.contains(variableModel)) {
+                        special_varmodel.add(variableModel);
+                    }
+                } else if (!varmodel.contains(variableModel)) {
+                    varmodel.add(variableModel);
+                }
+            });
+            current = current.getParent();
+        }
+        declarativeModel = varmodel;
+        specialModel = special_varmodel;
+    }
+
+    public static class VariableModel {
+        @Getter
+        private final String varname;
+        @Getter
+        private final String vartype;
+        @Getter
+        private final String varval;
+
+        private VariableModel(String varname, String vartype, String varval) {
+            this.varname = varname;
+            this.vartype = vartype;
+            this.varval = varval;
+        }
+    }
+}

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

@@ -66,4 +66,32 @@ cases{
         impRight;
     }
     auto;
+}
+
+script varDecl1(){
+    var1 : INT :=  1;
+    var2 : INT :=  2;
+    var3 : INT :=  3;
+}
+
+script varDecl2(){
+  var1 : INT :=  1;
+  impRight;
+  impRight;
+  impLeft;
+  cases {
+	case match `!q ==> p`:
+		notLeft;
+		var2 : INT :=  2;
+		notRight;
+
+
+
+	case match `q==>!p`:
+		notLeft;
+		var3 : INT :=  3;
+   }
+
+
+
 }
\ No newline at end of file

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/GoalOptionsMenu.fxml

@@ -15,6 +15,8 @@
         <RadioMenuItem fx:id="rmiNodeNames" text="Show _Node Names " toggleGroup="$toggleProjection"/>
         <RadioMenuItem fx:id="rmiRuleNames" text="Show _Rule Names " toggleGroup="$toggleProjection"/>
 
+        <MenuItem fx:id="showVarAssignment" text="Show _Variable Assignment" />
+
         <Menu fx:id="a" text="Filter by...">
             <MenuItem fx:id="removeFilter" text="Remove Filters"/>
             <SeparatorMenuItem/>

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/VariableAssignmentWindow.fxml

+<?xml version="1.0" encoding="UTF-8"?>
+
+
+<?import javafx.scene.control.*?>
+
+<fx:root xmlns="http://javafx.com/javafx"
+         xmlns:fx="http://javafx.com/fxml"
+         type="edu.kit.iti.formal.psdbg.gui.controls.VariableAssignmentWindow"
+         prefHeight="400.0" prefWidth="600.0">
+    <tabs>
+        <Tab text="Script Variables">
+            <TableView fx:id="declarative_tableView" ></TableView>
+        </Tab>
+        <Tab text="KeY Control Variables">
+            <TableView fx:id="special_tableView"></TableView>
+        </Tab>
+    </tabs>
+
+</fx:root>

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

@@ -412,4 +412,13 @@
   -fx-background-color: antiquewhite;
   -fx-stroke: navy;
 }
+/**********************************************************************************************************************/
+.table-view {
+.table-row-cell:empty {
+   -fx-background-color: white;
+}
 
+.table-row-cell:empty .table-cell {
+    -fx-border-width: 0px;
+}
+}