Commit 5fa9b68a authored by Sarah Grebing's avatar Sarah Grebing
Browse files

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

parents 5b801d08 a41d9894
......@@ -140,6 +140,22 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
}
} catch (ScriptException e) {
//TODO: adding UserinteractionWindow
/*TODO: possible cases not applicable, because
command not recognized
command multiple matches -> need more specification with on + formula
command not complete -> missig parameters
solution:
if(e.getMessage().equals("Not a unique \\assumes instantiation")) {
//TODO: open UserinteractionWindow
//TODO: apply completed TacletApp
//TODO: insert into script
}
*/
if (interpreter.isStrictMode()) {
throw new ScriptCommandNotApplicableException(e, c, map);
} else {
......
package edu.kit.iti.formal.psdbg.examples.applyEq;
import edu.kit.iti.formal.psdbg.examples.Example;
public class ApplyEqExample extends Example {
public ApplyEqExample() {
setName("ApplyEq");
defaultInit(getClass());
}
}
......@@ -20,6 +20,7 @@ import edu.kit.iti.formal.psdbg.examples.Examples;
import edu.kit.iti.formal.psdbg.fmt.DefaultFormatter;
import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger;
import edu.kit.iti.formal.psdbg.gui.controls.*;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.AbstractTreeNode;
import edu.kit.iti.formal.psdbg.gui.graph.Graph;
import edu.kit.iti.formal.psdbg.gui.graph.GraphView;
import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel;
......@@ -35,6 +36,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
import edu.kit.iti.formal.psdbg.parser.ASTDiff;
import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import edu.kit.iti.formal.psdbg.storage.KeyPersistentFacade;
......@@ -50,12 +52,14 @@ import javafx.event.EventHandler;
import javafx.fxml.FXML;
import javafx.fxml.FXMLLoader;
import javafx.fxml.Initializable;
import javafx.scene.Scene;
import javafx.scene.control.*;
import javafx.scene.layout.BorderPane;
import javafx.scene.web.WebEngine;
import javafx.scene.web.WebView;
import javafx.stage.FileChooser;
import javafx.stage.Modality;
import javafx.stage.Stage;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import org.apache.commons.io.FileUtils;
......@@ -1325,14 +1329,29 @@ public class DebuggerMain implements Initializable {
if(startnode == null) return;
stg.createGraph(startnode, FACADE.getProof().root());
TreeItem<TreeNode> item = (stg.toView());
scriptTreeView.setModel(model);
scriptTreeView.setFACADE(FACADE);
scriptTreeView.setTree(item);
scriptTreeView.setStg(stg);
scriptTreeView.toView();
/*TreeItem<AbstractTreeNode> item = (stg.toView());
scriptTreeView.setTree(item);
*/
}
@FXML
public void showUserInteractionW(ActionEvent actionEvent) {
Stage stage = new Stage();
stage.setTitle("Userinteraction");
Scene scene = new Scene(new UserinteractionWindow());
stage.setScene(scene);
stage.show();
}
public DockNode getJavaAreaDock() {
return javaAreaDock;
......@@ -1405,7 +1424,7 @@ public class DebuggerMain implements Initializable {
keyWindow.makePrettyView();
keyWindow.setVisible(true);
} catch (SecurityException e) {
e.printStackTrace();
// e.printStackTrace();
}
......@@ -1565,7 +1584,7 @@ public class DebuggerMain implements Initializable {
private class KeYSecurityManager extends SecurityManager {
@Override public void checkExit(int status) {
throw new SecurityException();
throw new SecurityException("KeY window closed");
}
@Override public void checkPermission(Permission perm) {
......
......@@ -325,6 +325,14 @@ public class InteractiveModeController {
model.setSelectedGoalNodeToShow(last);
} catch (Exception e) {
if (e.getClass().equals(ScriptException.class)) {
if (e.getMessage().equals("Not a unique \\assumes instantiation")) {
//TODO: open UserinteractionWindow
//TODO: apply completed TacletApp
//TODO: insert into script
}
System.out.println("e.getMessage() = " + e.getMessage());
throw new ScriptCommandNotApplicableException(e, c, map);
......
......@@ -24,9 +24,7 @@ public class ProofTreeContextMenu extends javafx.scene.control.ContextMenu {
MenuItem showSequent = new MenuItem("Show Sequent");
MenuItem showGoal = new MenuItem("Show in Goal List");
MenuItem expandAllNodes = new MenuItem("Expand Tree");
MenuItem showScriptTree = new MenuItem("Show ScriptTree");
//TODO: zum Testen
private ProofTree proofTree;
......@@ -88,8 +86,7 @@ public class ProofTreeContextMenu extends javafx.scene.control.ContextMenu {
proofTree.expandRootToLeaves(proofTree.getTreeProof().getRoot());
});
//TODO SCRIPTTREE ACTION
//showScriptTree.setOnAction(event -> proofTree.getTreeScriptCreation().showScriptTree());
getItems().setAll(refresh, expandAllNodes, new SeparatorMenuItem(), copy, createCases, showSequent, showGoal, showScriptTree);
getItems().setAll(refresh, expandAllNodes, new SeparatorMenuItem(), copy, createCases, showSequent, showGoal);
setAutoFix(true);
setAutoHide(true);
}
......
......@@ -29,7 +29,7 @@ public class AbstractTreeNode {
}
public TreeNode toTreeNode() {
return new TreeNode("no to string method yet", null);
return new TreeNode("Proof", null);
}
}
package edu.kit.iti.formal.psdbg.gui.controls.ScriptTree;
import de.uka.ilkd.key.proof.Node;
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;
/**
* This calss represents a node in the script tree, whcih can be of different kinds.
* The scriptTreeNodes is the model calls for TreeNodes
*/
public class RepeatTreeNode extends AbstractTreeNode {
@Getter
private final PTreeNode<KeyData> scriptState;
@Getter @Setter
private final int linenr;
private final boolean repeatstart;
public RepeatTreeNode(Node node, PTreeNode<KeyData> scriptState, int linenr, boolean repeatstart) {
super(node);
this.scriptState = scriptState;
this.linenr = linenr;
this.repeatstart = repeatstart;
}
@Override
public String toString(){
return scriptState.getStatement().toString()+" with ID "+scriptState.getId();
}
@Override
public TreeNode toTreeNode() {
String label= (repeatstart)? "repeat in line " + linenr + " START": "repeat in line " + linenr + " END";
return new TreeNode(label, getNode());
}
}
\ No newline at end of file
package edu.kit.iti.formal.psdbg.gui.controls;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
import de.uka.ilkd.key.pp.LogicPrinter;
import edu.kit.iti.formal.psdbg.LabelFactory;
import edu.kit.iti.formal.psdbg.gui.controller.Events;
import javafx.collections.ObservableList;
import javafx.scene.control.Menu;
import javafx.scene.control.MenuItem;
import javafx.scene.control.SeparatorMenuItem;
import javafx.scene.control.TreeItem;
public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu {
MenuItem copyBranchLabel = new MenuItem("Branch Label");
MenuItem copyProgramLines = new MenuItem("Program Lines");
MenuItem createCases = new MenuItem("Created Case for Open Goals");
MenuItem refresh = new MenuItem("Refresh (TOFIX)");
MenuItem showSequent = new MenuItem("Show Sequent");
MenuItem showGoal = new MenuItem("Show in Goal List");
MenuItem expandAllNodes = new MenuItem("Expand Tree");
private ScriptTreeView scriptTreeView;
public ScriptTreeContextMenu(ScriptTreeView scriptTreeView) {
this.scriptTreeView = scriptTreeView;
refresh.setOnAction(event -> scriptTreeView.setTree(scriptTreeView.toView()));
refresh.setGraphic(new MaterialDesignIconView(MaterialDesignIcon.REFRESH));
expandAllNodes.setOnAction((event) -> {
expandRootToLeaves(scriptTreeView.treeView.getRoot());
});
getItems().setAll(refresh, expandAllNodes); //, new SeparatorMenuItem(), createCases, showSequent, showGoal);
setAutoFix(true);
setAutoHide(true);
/*
copyBranchLabel.setOnAction(evt -> proofTree.consumeNode(n -> Utils.intoClipboard(
LabelFactory.getBranchingLabel(n)), "Copied!"));
copyProgramLines.setOnAction(evt -> {
proofTree.consumeNode(n -> {
Utils.intoClipboard(
LabelFactory.getProgramLines(n));
}, "Copied!");
});
MenuItem copySequent = new MenuItem("Sequent");
copySequent.setOnAction(evt -> {
proofTree.consumeNode(n -> {
assert proofTree.getServices() != null : "set KeY services!";
String s = LogicPrinter.quickPrintSequent(n.sequent(), proofTree.getServices());
Utils.intoClipboard(s);
}, "Copied!");
});
MenuItem copyRulesLabel = new MenuItem("Rule labels");
copyRulesLabel.setOnAction(evt -> {
proofTree.consumeNode(n -> {
Utils.intoClipboard(
LabelFactory.getRuleLabel(n));
}, "Copied!");
});
MenuItem copyProgramStatements = new MenuItem("Statements");
copyProgramStatements.setOnAction(event -> {
proofTree.consumeNode(n -> {
Utils.intoClipboard(
LabelFactory.getProgramStatmentLabel(n));
}, "Copied!");
});
Menu copy = new Menu("Copy", new MaterialDesignIconView(MaterialDesignIcon.CONTENT_COPY),
copyBranchLabel, copyProgramLines,
copyProgramStatements, copyRulesLabel,
copySequent);
createCases.setOnAction(this::onCreateCases);
showSequent.setOnAction((evt) ->
proofTree.consumeNode(n -> Events.fire(new Events.ShowSequent(n)), ""));
showGoal.setOnAction((evt) -> proofTree.consumeNode(n -> Events.fire(new Events.SelectNodeInGoalList(n)), "Found!"));
//TODO SCRIPTTREE ACTION
getItems().setAll(refresh, expandAllNodes, new SeparatorMenuItem(), copy, createCases, showSequent, showGoal);
setAutoFix(true);
setAutoHide(true);
*/
}
static void expandRootToLeaves(TreeItem candidate) {
if (candidate != null) {
if (!candidate.isLeaf()) {
candidate.setExpanded(true);
ObservableList<TreeItem> children = candidate.getChildren();
children.forEach(treeItem -> expandRootToLeaves(treeItem));
}
}
}
}
......@@ -43,11 +43,15 @@ public class ScriptTreeGraph {
private List<PlaceholderNode> placeholderNodes;
private HashMap<Node, PTreeNode> foreachNodes;
private HashMap<Node, PTreeNode> repeatNodes;
/**
* Contains color of nodes
* statistic of scripttree
*/
private MapProperty<Node, String> colorOfNodes = new SimpleMapProperty<Node, String>(FXCollections.observableHashMap());
private int openGoals = 0;
private int closedGoals = 0;
public void createGraph(PTreeNode<KeyData> rootPTreeNode, Node root) {
......@@ -57,6 +61,7 @@ public class ScriptTreeGraph {
ScriptTreeNode rootNode = new ScriptTreeNode(root, rootPTreeNode, rootPTreeNode.getStatement().getStartPosition().getLineNumber());
mapping = new HashMap<>();
foreachNodes = new HashMap<>();
repeatNodes = new HashMap<>();
placeholderNodes = new ArrayList<>();
front = new ArrayList<>();
sortedList = new ArrayList<>();
......@@ -73,7 +78,8 @@ public class ScriptTreeGraph {
computeList();
compute();
addGoals();
System.out.println("openGoals = " + openGoals);
System.out.println("closedGoals = " + closedGoals);
}
......@@ -174,30 +180,27 @@ public class ScriptTreeGraph {
}
mapping.size();
mapping.forEach((node, abstractTreeNode) -> System.out.println("node.serialNr() = " + node.serialNr() + " " + abstractTreeNode.toTreeNode().label));
// mapping.forEach((node, abstractTreeNode) -> System.out.println("node.serialNr() = " + node.serialNr() + " " + abstractTreeNode.toTreeNode().label));
}
/**
* returns treeItem that represents current Script tree
* @return
*/
public TreeItem<TreeNode> toView () {
TreeItem<TreeNode> treeItem;
/*
public TreeItem<AbstractTreeNode> toView () {
TreeItem<AbstractTreeNode> treeItem;
if(rootNode == null) {
treeItem = new TreeItem<>(new TreeNode("Proof", null));
treeItem = new TreeItem<>(new AbstractTreeNode(null));
DummyGoalNode dummy = new DummyGoalNode(null, false);
treeItem.getChildren().add(new TreeItem<>(dummy.toTreeNode()));
treeItem.getChildren().add(new TreeItem<>(dummy));
return treeItem;
}
treeItem = new TreeItem<>(new TreeNode("Proof", rootNode.getNode()));
treeItem = new TreeItem<>(new AbstractTreeNode(null));
List<AbstractTreeNode> children = mapping.get(rootNode.getNode()).getChildren();
if (children == null) return treeItem;
treeItem.getChildren().add(new TreeItem<>(mapping.get(rootNode.getNode()).toTreeNode()));
treeItem.getChildren().add(new TreeItem<>(mapping.get(rootNode.getNode())));
while (children.size() == 1) {
treeItem.getChildren().add(new TreeItem<>(children.get(0).toTreeNode()));
treeItem.getChildren().add(new TreeItem<>(children.get(0)));
children = children.get(0).getChildren();
if(children == null) return treeItem;
}
......@@ -209,15 +212,15 @@ public class ScriptTreeGraph {
return treeItem;
}
private TreeItem<TreeNode> rekursiveToView (AbstractTreeNode current){
TreeItem<TreeNode> treeItem = new TreeItem<>(current.toTreeNode()); //
private TreeItem<AbstractTreeNode> rekursiveToView (AbstractTreeNode current){
TreeItem<AbstractTreeNode> treeItem = new TreeItem<>(current); //
List<AbstractTreeNode> children = current.getChildren();
while (children != null && children.size() == 1) {
if(children.get(0) == null) return treeItem;
treeItem.getChildren().add(new TreeItem<>(children.get(0).toTreeNode()));
treeItem.getChildren().add(new TreeItem<>(children.get(0)));
children = children.get(0).getChildren();
}
if (children == null) {
......@@ -229,6 +232,7 @@ public class ScriptTreeGraph {
}
return treeItem;
}
*/
private class ScriptVisitor extends DefaultASTVisitor<Void> {
......@@ -240,7 +244,7 @@ public class ScriptTreeGraph {
Node callnode = nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
ScriptTreeNode sn = new ScriptTreeNode(callnode, nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
//check if statement was applicable
if (nextPtreeNode.getStateBeforeStmt() == nextPtreeNode.getStateAfterStmt()) {
if (nextPtreeNode.getStateAfterStmt().getGoals().equals(nextPtreeNode.getStateBeforeStmt().getGoals())) {
sn.setSucc(false);
}
......@@ -255,6 +259,7 @@ public class ScriptTreeGraph {
switch (children.size()) {
case 0:
putIntoFront(callnode);
checkIfRepeatEnd(callnode);
checkIfForeachEnd(callnode);
addPlaceholder(sn, sn.getNode());
break;
......@@ -296,7 +301,10 @@ public class ScriptTreeGraph {
}
if(children.size() > 0) {
children.forEach(k -> checkIfForeachEnd(k.getData().getNode()));
children.forEach(k -> {
checkIfRepeatEnd(k.getData().getNode());
checkIfForeachEnd(k.getData().getNode());
});
}
return null;
......@@ -361,6 +369,34 @@ public class ScriptTreeGraph {
aftergoals.forEach(k -> foreachNodes.put(k.getData().getNode(), nextPtreeNode));
return null;
}
@Override
public Void visit(RepeatStatement repeat){
List<GoalNode<KeyData>> goals = nextPtreeNode.getStateBeforeStmt().getGoals();
if (goals.size() == 0) return null;
goals.forEach(k -> {
RepeatTreeNode ftn = new RepeatTreeNode(
k.getData().getNode(),
nextPtreeNode,
nextPtreeNode.getStatement().getStartPosition().getLineNumber(),
true);
replacePlaceholder(
searchParentInMapping(k.getData().getNode()), ftn);
addPlaceholder(ftn, k.getData().getNode());
});
// add to repeat list -> so the end of a repeat can be catched
List<GoalNode<KeyData>> aftergoals = (nextPtreeNode.getStateAfterStmt() != null)? nextPtreeNode.getStateAfterStmt().getGoals()
: (nextPtreeNode.getStepOver() != null && nextPtreeNode.getStepOver().getStateBeforeStmt() != null) ? nextPtreeNode.getStepOver().getStateBeforeStmt().getGoals()
: new ArrayList<>();
aftergoals.forEach(k -> repeatNodes.put(k.getData().getNode(), nextPtreeNode));
return null;
}
}
......@@ -466,6 +502,25 @@ public class ScriptTreeGraph {
}
}
/*
checks if given node is the end of a repeat-statement
*/
private void checkIfRepeatEnd(Node n) {
if(repeatNodes.containsKey(n)) {
PTreeNode ptn = repeatNodes.get(n);
RepeatTreeNode ftn = new RepeatTreeNode(
n,
ptn,
ptn.getStatement().getStartPosition().getLineNumber(),
false);
replacePlaceholder(n, ftn);
addPlaceholder(ftn, n);
repeatNodes.remove(n);
}
}
/**
* Get all Branchlabels from child to parent GoalNode
* Order of Branchlabels is from bottom to top
......@@ -497,17 +552,6 @@ public class ScriptTreeGraph {
return branchlabels;
}
private boolean sameBranchlabelBefore(List<BranchLabelNode> branchlabels, Node node) {
if(branchlabels.size() == 0) return false;
return branchlabels.get(branchlabels.size()-1).getNode().serialNr() == node.serialNr();
}
private boolean isBranchLabel(String label) {
if (label.contains("rule") || label.contains("rules") || label.equals("Normal Execution")) return false;
return true;
}
/**
* Inserts given node after Branchlabelnodes
* @param node
......@@ -557,6 +601,7 @@ public class ScriptTreeGraph {
}
}
}
......@@ -577,57 +622,21 @@ public class ScriptTreeGraph {
}
private void addGoals() {
front.forEach(k -> replacePlaceholder(k, new DummyGoalNode(k, k.isClosed())));
}
private TreeCell<TreeNode> cellFactory(TreeView<TreeNode> nodeTreeView) {
TextFieldTreeCell<TreeNode> tftc = new TextFieldTreeCell<>();
StringConverter<TreeNode> stringConverter = new StringConverter<TreeNode>() {
@Override
public String toString(TreeNode object) {
return object.label;
}
@Override
public TreeNode fromString(String string) {
return null;
front.forEach(k -> {
replacePlaceholder(k, new DummyGoalNode(k, k.isClosed()));
//fill statistics
if(k.isClosed()) {
closedGoals++;
} else {
openGoals ++;
}
};
tftc.setConverter(stringConverter);
tftc.itemProperty().addListener((p, o, n) -> {
if (n != null)
repaint(tftc);
});
//colorOfNodes.addListener((InvalidationListener) o -> repaint(tftc));
return tftc;
}
private void repaint(TextFieldTreeCell<TreeNode> tftc) {
TreeNode item = tftc.getItem();
Node n = item.node;
tftc.setStyle("");
if (n != null) {