Commit 7e12bf82 authored by Lulu Luong's avatar Lulu Luong
Browse files

added ScriptTree statistics (accessible via Contextmenu) +

cleaned code + bug fixes
parent 24e7bad0
Pipeline #33839 passed with stages
in 2 minutes and 21 seconds
...@@ -1338,14 +1338,17 @@ public class DebuggerMain implements Initializable { ...@@ -1338,14 +1338,17 @@ public class DebuggerMain implements Initializable {
* refreshes the view on the scripttree * refreshes the view on the scripttree
*/ */
private void refreshScriptTreeView() { private void refreshScriptTreeView() {
scriptTreeGraph = new ScriptTreeGraph(); //refresh only if ScriptTreeView is visible
PTreeNode startnode = null; if (scriptTreeDock.isDocked() || scriptTreeDock.isFloating()) {
if (model.getDebuggerFramework() != null && model.getDebuggerFramework().getPtreeManager() != null) { scriptTreeGraph = new ScriptTreeGraph();
startnode = model.getDebuggerFramework().getPtreeManager().getStartNode(); PTreeNode startnode = null;
if (model.getDebuggerFramework() != null && model.getDebuggerFramework().getPtreeManager() != null) {
startnode = model.getDebuggerFramework().getPtreeManager().getStartNode();
}
scriptTreeGraph.createGraph(startnode, FACADE.getProof().root());
scriptTreeView.setStg(scriptTreeGraph);
scriptTreeView.toView();
} }
scriptTreeGraph.createGraph(startnode, FACADE.getProof().root());
scriptTreeView.setStg(scriptTreeGraph);
scriptTreeView.toView();
} }
@FXML @FXML
......
...@@ -113,8 +113,6 @@ public class ScriptController { ...@@ -113,8 +113,6 @@ public class ScriptController {
.filter(a -> a.getForce().equals(SavePoint.ForceOption.NO)) .filter(a -> a.getForce().equals(SavePoint.ForceOption.NO))
.collect(Collectors.toList()); .collect(Collectors.toList());
noForceSp.forEach(e -> getMainScript().getScriptArea().setAlertMarker(e.getLineNumber())); noForceSp.forEach(e -> getMainScript().getScriptArea().setAlertMarker(e.getLineNumber()));
loggerConsole.info("Found savepoints: " + list);
} }
} catch (Exception e) { } catch (Exception e) {
......
...@@ -16,13 +16,16 @@ import lombok.Setter; ...@@ -16,13 +16,16 @@ import lombok.Setter;
import java.util.function.Consumer; import java.util.function.Consumer;
/**
* Contextmenu for the ScriptTreevView
*
* @author An.Luong
*/
public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu { public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu {
MenuItem copyBranchLabel = new MenuItem("Branch Label"); MenuItem copyBranchLabel = new MenuItem("Branch Label");
MenuItem copyProgramLines = new MenuItem("Program Lines");
MenuItem createCases = new MenuItem("Created Case for Open Goals");
MenuItem showSequent = new MenuItem("Show Sequent"); MenuItem showSequent = new MenuItem("Show Sequent");
MenuItem showGoal = new MenuItem("Show in Goal List"); MenuItem showStatistics = new MenuItem("Show Statistics");
MenuItem expandAllNodes = new MenuItem("Expand Tree from here"); MenuItem expandAllNodes = new MenuItem("Expand Tree from here");
MenuItem collapseAllNodes = new MenuItem("Collapse Tree from here"); MenuItem collapseAllNodes = new MenuItem("Collapse Tree from here");
...@@ -53,30 +56,40 @@ public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu { ...@@ -53,30 +56,40 @@ public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu {
LabelFactory.getBranchingLabel(((AbstractTreeNode) n.getValue()).getNode())); LabelFactory.getBranchingLabel(((AbstractTreeNode) n.getValue()).getNode()));
}, "Copied!")); }, "Copied!"));
getItems().setAll(expandAllNodes, collapseAllNodes, new SeparatorMenuItem(), showSequent, createCases); //, new SeparatorMenuItem(), createCases, showSequent, showGoal); showStatistics.setOnAction(evt -> Events.fire(
new Events.PublishMessage("[ScriptTree statistics] open goals: " + scriptTreeView.getStg().getOpenGoals() + ", closed goals: " +
scriptTreeView.getStg().getClosedGoals(), 1)));
getItems().setAll(expandAllNodes, collapseAllNodes, new SeparatorMenuItem(), showSequent, showStatistics);
setAutoFix(true); setAutoFix(true);
setAutoHide(true); setAutoHide(true);
} }
/**
* Expand all subTreeItems from selected Treeitem
* @param candidate selected Treeitem
*/
static void expandNodeToLeaves(TreeItem candidate) { static void expandNodeToLeaves(TreeItem candidate) {
if (candidate != null) { if (candidate != null) {
if (!candidate.isLeaf()) { if (!candidate.isLeaf()) {
candidate.setExpanded(true); candidate.setExpanded(true);
ObservableList<TreeItem> children = candidate.getChildren(); ObservableList<TreeItem> children = candidate.getChildren();
children.forEach(treeItem -> expandNodeToLeaves(treeItem)); children.forEach(treeItem -> expandNodeToLeaves(treeItem));
} }
} }
} }
/**
* Collapse all subTreeItems from selected Treeitem
* @param candidate selected Treeitem
*/
static void collapseNodeToLeaves(TreeItem candidate) { static void collapseNodeToLeaves(TreeItem candidate) {
if (candidate != null) { if (candidate != null) {
if (!candidate.isLeaf()) { if (!candidate.isLeaf()) {
candidate.setExpanded(false); candidate.setExpanded(false);
ObservableList<TreeItem> children = candidate.getChildren(); ObservableList<TreeItem> children = candidate.getChildren();
children.forEach(treeItem -> expandNodeToLeaves(treeItem)); children.forEach(treeItem -> expandNodeToLeaves(treeItem));
} }
} }
} }
......
...@@ -4,6 +4,7 @@ import com.google.common.collect.Lists; ...@@ -4,6 +4,7 @@ import com.google.common.collect.Lists;
import com.google.common.graph.GraphBuilder; import com.google.common.graph.GraphBuilder;
import com.google.common.graph.MutableGraph; import com.google.common.graph.MutableGraph;
import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.gui.controller.Events;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.*; import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.*;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
...@@ -45,14 +46,21 @@ public class ScriptTreeGraph { ...@@ -45,14 +46,21 @@ public class ScriptTreeGraph {
private List<PlaceholderNode> placeholderNodes; private List<PlaceholderNode> placeholderNodes;
/**
* contains last node of a ForeachStatement
*/
private HashMap<Node, PTreeNode> foreachNodes; private HashMap<Node, PTreeNode> foreachNodes;
/**
* contains last node of RepeatStatement
*/
private HashMap<Node, PTreeNode> repeatNodes; private HashMap<Node, PTreeNode> repeatNodes;
/** /**
* statistic of scripttree * statistics of scripttree
*/ */
@Getter
private int openGoals = 0; private int openGoals = 0;
@Getter
private int closedGoals = 0; private int closedGoals = 0;
...@@ -85,8 +93,6 @@ public class ScriptTreeGraph { ...@@ -85,8 +93,6 @@ public class ScriptTreeGraph {
computeList(); computeList();
compute(); compute();
addGoals(); addGoals();
System.out.println("openGoals = " + openGoals);
System.out.println("closedGoals = " + closedGoals);
} }
...@@ -190,7 +196,6 @@ public class ScriptTreeGraph { ...@@ -190,7 +196,6 @@ public class ScriptTreeGraph {
} }
mapping.size(); mapping.size();
// mapping.forEach((node, abstractTreeNode) -> System.out.println("node.serialNr() = " + node.serialNr() + " " + abstractTreeNode.toTreeNode().label));
} }
/* /*
...@@ -284,10 +289,6 @@ public class ScriptTreeGraph { ...@@ -284,10 +289,6 @@ public class ScriptTreeGraph {
List<BranchLabelNode> branchlabel = getBranchLabels(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode(), gn); List<BranchLabelNode> branchlabel = getBranchLabels(nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode(), gn);
if(branchlabel.size() != 0) { if(branchlabel.size() != 0) {
Lists.reverse(branchlabel).forEach(k ->
System.out.println(k.getNode().serialNr() + " " + k.getLabelName()));
insertBranchLabels(callnode, branchlabel); insertBranchLabels(callnode, branchlabel);
addPlaceholder(branchlabel.get(0), gn.getData().getNode()); addPlaceholder(branchlabel.get(0), gn.getData().getNode());
...@@ -341,6 +342,8 @@ public class ScriptTreeGraph { ...@@ -341,6 +342,8 @@ public class ScriptTreeGraph {
@Override @Override
public Void visit(DefaultCaseStatement caseStatement) { public Void visit(DefaultCaseStatement caseStatement) {
PTreeNode<KeyData> nextintoptn = nextPtreeNode.getStepInto(); PTreeNode<KeyData> nextintoptn = nextPtreeNode.getStepInto();
//TODO: QS throws a Nullpointer at same point, eventhough cript has no Defaultstatement
ScriptTreeNode match = new ScriptTreeNode(nextPtreeNode.getStepInto().getStateBeforeStmt().getSelectedGoalNode().getData().getNode(),nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber()); ScriptTreeNode match = new ScriptTreeNode(nextPtreeNode.getStepInto().getStateBeforeStmt().getSelectedGoalNode().getData().getNode(),nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
match.setMatchEx(true); match.setMatchEx(true);
match.setSucc(true); match.setSucc(true);
...@@ -407,6 +410,7 @@ public class ScriptTreeGraph { ...@@ -407,6 +410,7 @@ public class ScriptTreeGraph {
} }
} }
private void addPlaceholder(AbstractTreeNode parent, Node current) { private void addPlaceholder(AbstractTreeNode parent, Node current) {
PlaceholderNode phn = new PlaceholderNode(current); PlaceholderNode phn = new PlaceholderNode(current);
phn.setParent(parent); phn.setParent(parent);
...@@ -417,7 +421,6 @@ public class ScriptTreeGraph { ...@@ -417,7 +421,6 @@ public class ScriptTreeGraph {
addToSubChildren(parent.getNode(), phn); addToSubChildren(parent.getNode(), phn);
} }
placeholderNodes.add(phn); placeholderNodes.add(phn);
} }
...@@ -628,13 +631,25 @@ public class ScriptTreeGraph { ...@@ -628,13 +631,25 @@ public class ScriptTreeGraph {
return -1; return -1;
} }
private void addGoals() { private void addGoals() {
//No script has been executed yet
if (rootNode instanceof DummyGoalNode) {
//fill statitics
if (rootNode.getNode().isClosed()) {
closedGoals++;
} else {
openGoals++;
}
return;
}
//after script execution
if (front == null) { if (front == null) {
return; return;
} }
front.forEach(k -> { front.forEach(k -> {
replacePlaceholder(k, new DummyGoalNode(k, k.isClosed())); replacePlaceholder(k, new DummyGoalNode(k, k.isClosed()));
//fill statistics //fill statistics
if(k.isClosed()) { if(k.isClosed()) {
closedGoals++; closedGoals++;
......
...@@ -20,6 +20,7 @@ import javafx.scene.layout.BackgroundFill; ...@@ -20,6 +20,7 @@ import javafx.scene.layout.BackgroundFill;
import javafx.scene.layout.BorderPane; import javafx.scene.layout.BorderPane;
import javafx.scene.layout.CornerRadii; import javafx.scene.layout.CornerRadii;
import javafx.util.StringConverter; import javafx.util.StringConverter;
import lombok.Getter;
import lombok.Setter; import lombok.Setter;
import java.awt.*; import java.awt.*;
...@@ -30,16 +31,17 @@ import java.util.Map; ...@@ -30,16 +31,17 @@ import java.util.Map;
import java.util.function.Consumer; import java.util.function.Consumer;
/** /**
* Displays a Treeview of the ScriptTree, which represents state of proof using only * Displays a Treeview of the ScriptTree, which represents state of proof with
* statements in the script * - statements in the script
* Branching Labels * - branching labels
* DummyGoalNodes * - goal nodes
* *
* @author luong * @author An.Luong
*/ */
public class ScriptTreeView extends BorderPane { public class ScriptTreeView extends BorderPane {
@Setter @Setter
@Getter
private ScriptTreeGraph stg; private ScriptTreeGraph stg;
private ScriptTreeContextMenu contextMenu; private ScriptTreeContextMenu contextMenu;
......
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