Commit afe30047 authored by Lulu Luong's avatar Lulu Luong

Bug fixed:

Dummygoalsnodes are visible
no script executed -> no nullpointer
symbex leads to infinity loop
remove scriptpanel in prooftree
matchexpression shown

TODO:
foreach start shown but still missing end
icon for scripttree needs to be included
parent c5fd7c63
Pipeline #25696 passed with stages
in 2 minutes and 51 seconds
......@@ -45,9 +45,6 @@ public class ProofTree extends BorderPane {
@FXML
private TreeView<TreeNode> treeProof;
//TODO: added for testing
@FXML
private TreeView<TreeNode> treeScript;
private ContextMenu contextMenu;
......@@ -118,7 +115,6 @@ public class ProofTree extends BorderPane {
treeCreation = new KeyProofTreeTransformation(sentinels);
treeProof.setCellFactory(this::cellFactory);
treeScript.setCellFactory(this::cellFactory);
root.addListener(o -> init());
proof.addListener((prop, old, n) -> {
......@@ -327,16 +323,9 @@ public class ProofTree extends BorderPane {
treeProof.setRoot(item);
ProofTreeManager<KeyData> manager = treeScriptCreation.manager;
if(manager != null) {
PTreeNode startNode = manager.getStartNode();
if (startNode != null) {
treeScript.setRoot(treeScriptCreation.buildScriptTree(startNode, proof.get()));
}
}
}
treeProof.refresh();
treeScript.refresh();
}
......
......@@ -5,6 +5,9 @@ import edu.kit.iti.formal.psdbg.gui.controls.TreeNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.GuardedCaseStatement;
import edu.kit.iti.formal.psdbg.parser.ast.MatchExpression;
import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import lombok.Setter;
......@@ -36,9 +39,13 @@ public class ScriptTreeNode extends AbstractTreeNode {
public TreeNode toTreeNode() {
String label;
if (isMatchEx()) {
label = "match in line " + linenr;
String matchexpression = ((TermLiteral) ((MatchExpression) ((GuardedCaseStatement) scriptState.getStatement()).getGuard()).getPattern()).getContent();
label = "match ("+ matchexpression +") in line " + linenr;
} else {
label = ((CallStatement) scriptState.getStatement()).getCommand() + " (line " + linenr + ")";
label = (scriptState.getStatement() instanceof CallStatement)?
((CallStatement)scriptState.getStatement()).getCommand() + " (line " + linenr + ")"
: "foreach in line " + linenr + " START";
}
if (!isSucc()) {
......
......@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg.gui.controls;
import com.google.common.graph.GraphBuilder;
import com.google.common.graph.MutableGraph;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.rule.BlockContractBuilders;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.AbstractTreeNode;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.BranchLabelNode;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.DummyGoalNode;
......@@ -14,6 +15,7 @@ import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.ForeachStatement;
import edu.kit.iti.formal.psdbg.parser.ast.GuardedCaseStatement;
import javafx.scene.control.TreeItem;
import sun.reflect.generics.tree.Tree;
......@@ -133,7 +135,8 @@ public class ScriptTreeGraph {
* @param atn
*/
private void addToSubChildren(Node node, AbstractTreeNode atn) {
if(mapping.get(node) == atn) return;
if(atn == null) return;
if(mapping.get(node) == atn) return;
if (mapping.get(node).getChildren() == null) {
List<AbstractTreeNode> childlist = new ArrayList<>();
childlist.add(atn);
......@@ -143,7 +146,7 @@ public class ScriptTreeGraph {
List<AbstractTreeNode> childlist = mapping.get(node).getChildren();
if(childlist.contains(atn)) return;
while (childlist.get(0).getChildren() != null) {
while (childlist.get(0) != null && childlist.get(0).getChildren() != null) {
if(childlist.contains(atn)) return;
childlist = childlist.get(0).getChildren();
......@@ -183,10 +186,9 @@ public class ScriptTreeGraph {
while (iter.hasNext()) {
nextPtreeNode = iter.next();
statement = nextPtreeNode.getStatement();
//check for selected node and find the node in map
if (nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode() != null) {
//if (nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode() != null) {
statement.accept(visitor);
}
//}
}
mapping.size();
......@@ -202,7 +204,7 @@ public class ScriptTreeGraph {
if(rootNode == null) {
treeItem = new TreeItem<>(new TreeNode("Proof", null));
DummyGoalNode dummy = new DummyGoalNode(null, false);
treeItem.getChildren().add(new TreeItem<TreeNode>(dummy.toTreeNode()));
treeItem.getChildren().add(new TreeItem<>(dummy.toTreeNode()));
return treeItem;
}
treeItem = new TreeItem<>(new TreeNode("Proof", rootNode.getNode()));
......@@ -225,7 +227,7 @@ public class ScriptTreeGraph {
}
private TreeItem<TreeNode> rekursiveToView (AbstractTreeNode current){
TreeItem<TreeNode> treeItem = new TreeItem<>(current.toTreeNode()); //TODO: sollte eig immer ein Branchlabel sein
TreeItem<TreeNode> treeItem = new TreeItem<>(current.toTreeNode()); //
List<AbstractTreeNode> children = current.getChildren();
......@@ -249,6 +251,7 @@ public class ScriptTreeGraph {
@Override
public Void visit(CallStatement call) {
if (nextPtreeNode.toString().equals("End of Script")) return null;
Node n = nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
ScriptTreeNode sn = new ScriptTreeNode(n, nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
// sn.setParent(mapping.get(current));
......@@ -304,7 +307,6 @@ public class ScriptTreeGraph {
if (nextintoptn == null) {
match.setSucc(false);
//TODO: add stuff
return null;
}
Node n = nextintoptn.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
......@@ -313,7 +315,13 @@ public class ScriptTreeGraph {
return null;
}
@Override
public Void visit(ForeachStatement foreachStatement){
List<GoalNode<KeyData>> goals = nextPtreeNode.getStateBeforeStmt().getGoals();
if(goals.size() == 0) return null;
goals.forEach(k -> putIntoMapping(k.getData().getNode(), new ScriptTreeNode(k.getData().getNode(), nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber())));return null;}
//TODO: add end foreach
}
/**
......
......@@ -9,6 +9,7 @@
<?import javafx.scene.layout.Pane?>
<?import javafx.scene.layout.VBox?>
<?import org.dockfx.DockPane?>
<?import javafx.scene.image.ImageView?>
<BorderPane xmlns:fx="http://javafx.com/fxml/1" fx:id="rootPane" xmlns="http://javafx.com/javafx/8.0.112"
fx:controller="edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain"
prefWidth="1024" prefHeight="640">
......@@ -182,50 +183,54 @@
</graphic>
</CheckMenuItem>
<CheckMenuItem fx:id="miScriptTree" onAction="#showScriptTree" text="Show Script Tree">
<graphic>
<MaterialDesignIconView glyphName="TREE" size="24.0"/>
</graphic>
</CheckMenuItem>
<CheckMenuItem fx:id="miCommandHelp" onAction="#showCommandHelp"
accelerator="F1"
text="Show Command Help">
<graphic>
<MaterialDesignIconView glyphName="STACKEXCHANGE" size="24.0"/>
</graphic>
</CheckMenuItem>
</items>
</Menu>
<Menu fx:id="examplesMenu" text="_Examples">
<items>
<MenuItem text="Examples not loaded" disable="true"/>
</items>
</Menu>
<Menu text="Help">
<items>
<MenuItem text="About" onAction="#showAbout"/>
</items>
</Menu>
</menus>
</MenuBar>
<ToolBar fx:id="toolbar">
<items>
<SplitMenuButton fx:id="buttonStartInterpreter" onAction="#executeScript"
disable="${controller.executeNotPossible}">
<graphic>
<MaterialDesignIconView glyphName="PLAY" size="24.0"/>
</graphic>
<tooltip>
<Tooltip text="Execute Script"/>
</tooltip>
<items>
<!-- <MenuItem text="Execute from Cursor"
onAction="#executeScriptFromCursor"
disable="${controller.executeNotPossible}">
<graphic>
<MaterialDesignIconView glyphName="CURSOR_TEXT" size="24.0"/>
</graphic>
</MenuItem> -->
<!--
<graphic>
<ImageView
image="resources\edu\kit\iti\formal\psdbg\gui\icon\treescript.jpg">
</ImageView>
</graphic>
-->
</CheckMenuItem>
<CheckMenuItem fx:id="miCommandHelp" onAction="#showCommandHelp"
accelerator="F1"
text="Show Command Help">
<graphic>
<MaterialDesignIconView glyphName="STACKEXCHANGE" size="24.0"/>
</graphic>
</CheckMenuItem>
</items>
</Menu>
<Menu fx:id="examplesMenu" text="_Examples">
<items>
<MenuItem text="Examples not loaded" disable="true"/>
</items>
</Menu>
<Menu text="Help">
<items>
<MenuItem text="About" onAction="#showAbout"/>
</items>
</Menu>
</menus>
</MenuBar>
<ToolBar fx:id="toolbar">
<items>
<SplitMenuButton fx:id="buttonStartInterpreter" onAction="#executeScript"
disable="${controller.executeNotPossible}">
<graphic>
<MaterialDesignIconView glyphName="PLAY" size="24.0"/>
</graphic>
<tooltip>
<Tooltip text="Execute Script"/>
</tooltip>
<items>
<!-- <MenuItem text="Execute from Cursor"
onAction="#executeScriptFromCursor"
disable="${controller.executeNotPossible}">
<graphic>
<MaterialDesignIconView glyphName="CURSOR_TEXT" size="24.0"/>
</graphic>
</MenuItem> -->
<MenuItem
text="Execute Script Stepwise From Start"
......@@ -390,6 +395,17 @@
<Tooltip text="Show Proof Tree"/>
</tooltip>
</ToggleButton>
<ToggleButton fx:id="togBtnScriptTree" onAction="#showScriptTree">
<graphic>
<!-- FILE-TREE-->
<MaterialDesignIconView glyphName="TREE" size="24.0"/>
</graphic>
<tooltip>
<Tooltip text="Show Script Tree"/>
</tooltip>
</ToggleButton>
<ToggleButton fx:id="togBtnCommandHelp" onAction="#showCommandHelp">
<graphic>
<MaterialDesignIconView glyphName="STACKEXCHANGE" size="24.0"/>
......
......@@ -3,14 +3,10 @@
<?import javafx.scene.control.TreeView?>
<?import javafx.scene.layout.BorderPane?>
<fx:root type="javafx.scene.layout.BorderPane" xmlns:fx="http://javafx.com/fxml/1" fx:id="rootPane" xmlns="http://javafx.com/javafx/8.0.112">
<left>
<center>
<TreeView fx:id="treeProof" editable="false">
</TreeView>
</left>
<right>
<TreeView fx:id="treeScript" editable="false">
</center>
</TreeView>
</right>
</fx:root>
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment