Commit 2566cd6e authored by Sarah Grebing's avatar Sarah Grebing

minor details, still getting null pointer if end of script is reached

parent b59c8a8e
Pipeline #23167 passed with stages
in 3 minutes and 6 seconds
...@@ -112,7 +112,7 @@ public class ProofTree extends BorderPane { ...@@ -112,7 +112,7 @@ public class ProofTree extends BorderPane {
Utils.createWithFXML(this); Utils.createWithFXML(this);
//TODO remove this hack for a better solution //TODO remove this hack for a better solution
main.getModel().debuggerFrameworkProperty().addListener((p, n, m) -> { main.getModel().debuggerFrameworkProperty().addListener((p, n, m) -> {
treeScriptCreation = new ScriptTreeTransformation(m.getPtreeManager(), proof.get(), root.get()); treeScriptCreation = new ScriptTreeTransformation(m.getPtreeManager());
}); });
treeCreation = new KeyProofTreeTransformation(sentinels); treeCreation = new KeyProofTreeTransformation(sentinels);
...@@ -330,7 +330,7 @@ public class ProofTree extends BorderPane { ...@@ -330,7 +330,7 @@ public class ProofTree extends BorderPane {
if(manager != null) { if(manager != null) {
PTreeNode startNode = manager.getStartNode(); PTreeNode startNode = manager.getStartNode();
if (startNode != null) { if (startNode != null) {
treeScript.setRoot(treeScriptCreation.buildScriptTree(startNode)); treeScript.setRoot(treeScriptCreation.buildScriptTree(startNode, proof.get()));
} }
} }
} }
......
...@@ -24,10 +24,6 @@ import java.util.*; ...@@ -24,10 +24,6 @@ import java.util.*;
@RequiredArgsConstructor @RequiredArgsConstructor
public class ScriptTreeTransformation extends KeyProofTreeTransformation { public class ScriptTreeTransformation extends KeyProofTreeTransformation {
final ProofTreeManager<KeyData> manager; final ProofTreeManager<KeyData> manager;
@Getter
private final Proof proof;
@Getter
private final Node root;
private PTreeNode<KeyData> currentPointer; private PTreeNode<KeyData> currentPointer;
...@@ -119,7 +115,7 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation { ...@@ -119,7 +115,7 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
} }
//TODO: Reverse ArrayList in the end or nah? /*//TODO: Reverse ArrayList in the end or nah?
@Deprecated @Deprecated
public ArrayList<String> getBranchLabels(TreeNode node) { public ArrayList<String> getBranchLabels(TreeNode node) {
TreeItem<TreeNode> proofTree = create(proof); TreeItem<TreeNode> proofTree = create(proof);
...@@ -156,10 +152,10 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation { ...@@ -156,10 +152,10 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
return branchlabels; return branchlabels;
} }
*/
public TreeItem<TreeNode> buildScriptTree(PTreeNode<KeyData> node, Proof proof) {
public TreeItem<TreeNode> buildScriptTree(PTreeNode<KeyData> node) {
TreeItem<TreeNode> tree = create(proof); TreeItem<TreeNode> tree = create(proof);
PTreeNode<KeyData> nextNode = node; PTreeNode<KeyData> nextNode = node;
...@@ -172,7 +168,8 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation { ...@@ -172,7 +168,8 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
Node root = rootGoalNode.getData().getNode(); Node root = rootGoalNode.getData().getNode();
TreeItem<TreeNode> currentItem = new TreeItem<>(new TreeNode("Proof", nextNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode())); TreeItem<TreeNode> currentItem = new TreeItem<>(new TreeNode("Proof", nextNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode()));
//build the first node after the root //build the first node after the root
currentItem.getChildren().add(new TreeItem<>(createTreeNode(nextNode))); TreeNode t = createTreeNode(nextNode);
if (t != null) currentItem.getChildren().add(new TreeItem<>());
return buildScriptSubTree(currentItem, nextNode, nextNode.getStateAfterStmt().getSelectedGoalNode()); return buildScriptSubTree(currentItem, nextNode, nextNode.getStateAfterStmt().getSelectedGoalNode());
...@@ -201,17 +198,24 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation { ...@@ -201,17 +198,24 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
}*/ }*/
//if we have reached a state where we do not need a selector //if we have reached a state where we do not need a selector
if(currentNode == null && nextNode.getStateAfterStmt().getGoals().size() < 2){ if(currentNode == null && nextNode.getStateAfterStmt().getGoals().size() < 2){
currentItem.getChildren().add(new TreeItem<>(createTreeNode(nextNode))); TreeNode t = createTreeNode(nextNode);
if (t!=null) {
currentItem.getChildren().add(new TreeItem<>(t));
}
return currentItem; return currentItem;
} }
if (getNextPtreeNode(nextNode) == null) { //End of Script if (getNextPtreeNode(nextNode) == null || getNextPtreeNode(nextNode).isLastNode()) { //End of Script
System.out.println("nextNode = " + nextNode.getStatement());
return currentItem; return currentItem;
} }
//if we arrive at a cases statement we skip this statement //if we arrive at a cases statement we skip this statement
if(nextNode.getStateAfterStmt() != null && nextNode.getStateAfterStmt().getGoals().size() > 1){ if(nextNode.getStateAfterStmt() != null && nextNode.getStateAfterStmt().getGoals().size() > 1){
//we arrived at a branching statement, add it to the tree and add the branches as new children //we arrived at a branching statement, add it to the tree and add the branches as new children
currentItem.getChildren().add(new TreeItem<>(createTreeNode(nextNode))); TreeNode t = createTreeNode(nextNode);
if(t != null) {
currentItem.getChildren().add(new TreeItem<>(t));
}
List<GoalNode<KeyData>> goals = nextNode.getStateAfterStmt().getGoals(); List<GoalNode<KeyData>> goals = nextNode.getStateAfterStmt().getGoals();
int size = goals.size(); int size = goals.size();
for (int i = 0; i < size; i++) { for (int i = 0; i < size; i++) {
...@@ -221,14 +225,16 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation { ...@@ -221,14 +225,16 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
Pair<TreeItem<TreeNode>, PTreeNode<KeyData>> treeItemPTreeNodePair = buildScriptTreeHelper(nextNode, goals.get(i)); Pair<TreeItem<TreeNode>, PTreeNode<KeyData>> treeItemPTreeNodePair = buildScriptTreeHelper(nextNode, goals.get(i));
child.getChildren().add(treeItemPTreeNodePair.getKey()); child.getChildren().add(treeItemPTreeNodePair.getKey());
currentItem.getChildren().add(child); currentItem.getChildren().add(child);
nextNode = computeNextPtreeNode(treeItemPTreeNodePair.getValue()); nextNode = computeNextPtreeNode(treeItemPTreeNodePair.getValue());
setPointer(nextNode); setPointer(nextNode);
} }
return currentItem; return currentItem;
} else { } else {
currentItem.getChildren().add(new TreeItem<>(createTreeNode(nextNode))); TreeNode t = createTreeNode(nextNode);
if (t != null) {
currentItem.getChildren().add(new TreeItem<>(t));
}
} }
...@@ -243,9 +249,16 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation { ...@@ -243,9 +249,16 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
private Pair<TreeItem<TreeNode>, PTreeNode<KeyData>> buildScriptTreeHelper(PTreeNode<KeyData> node, GoalNode<KeyData> keyDataGoalNode) { private Pair<TreeItem<TreeNode>, PTreeNode<KeyData>> buildScriptTreeHelper(PTreeNode<KeyData> node, GoalNode<KeyData> keyDataGoalNode) {
assert node.getStateBeforeStmt().getGoals().get(0).getData() != null; assert node.getStateBeforeStmt().getGoals().get(0).getData() != null;
PTreeNode<KeyData> nextNode;
TreeItem<TreeNode> currentItem = null; TreeItem<TreeNode> currentItem = null;
PTreeNode<KeyData> nextNode = getNextPtreeNode(node);
setPointer(nextNode); if(getNextPtreeNode(node) != null){
nextNode = getNextPtreeNode(node);
setPointer(nextNode);
} else {
nextNode = node;
setPointer(nextNode);
}
while(currentItem == null){ while(currentItem == null){
...@@ -276,15 +289,22 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation { ...@@ -276,15 +289,22 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
//handle if we reach other statements //handle if we reach other statements
if(nextNode.getStateBeforeStmt() == null || if(nextNode.getStateBeforeStmt() == null ||
nextNode.getStateBeforeStmt().getGoals() == null){ nextNode.getStateBeforeStmt().getGoals() == null
//||
//nextNode.getStatement().getStartPosition().getLineNumber() < 1
){
continue; continue;
} else { } else {
assert nextNode.getStateBeforeStmt().getSelectedGoalNode().equals(keyDataGoalNode); assert nextNode.getStateBeforeStmt().getSelectedGoalNode().equals(keyDataGoalNode);
Node node1 = keyDataGoalNode.getData().getNode();
ASTNode statement= nextNode.getStatement();
ASTNode astNode = mutatedBy.get(node1);
boolean bool = mutatedBy.get(keyDataGoalNode.getData().getNode()).equals(nextNode.getStatement()); if(astNode == null || astNode.equals(statement)) {
if(bool) {
currentItem = new TreeItem<>(new TreeNode(((CallStatement) nextNode.getStatement()).getCommand() + currentItem = new TreeItem<>(new TreeNode(((CallStatement) nextNode.getStatement()).getCommand() +
" (line " + nextNode.getStatement().getStartPosition().getLineNumber() + " (line " + nextNode.getStatement().getStartPosition().getLineNumber() +
")", keyDataGoalNode.getData().getNode())); ")", keyDataGoalNode.getData().getNode()));
...@@ -315,7 +335,7 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation { ...@@ -315,7 +335,7 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
public TreeNode createTreeNode(PTreeNode<KeyData> node) { public TreeNode createTreeNode(PTreeNode<KeyData> node) {
try { try {
if(node == null){ if(node == null){
System.out.println("Node is null"); return null;
} }
if(node.getStatement() instanceof CallStatement) { if(node.getStatement() instanceof CallStatement) {
...@@ -323,7 +343,7 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation { ...@@ -323,7 +343,7 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
int lineNumber = node.getStatement().getStartPosition().getLineNumber(); int lineNumber = node.getStatement().getStartPosition().getLineNumber();
if(lineNumber == -1 || command.equals("")){ if(lineNumber == -1 || command.equals("")){
System.out.println(node.getStatement().getNodeName());
return new TreeNode("TempEnd", node.getStateBeforeStmt().getGoals().get(0).getData().getNode()); return new TreeNode("TempEnd", node.getStateBeforeStmt().getGoals().get(0).getData().getNode());
} }
Node node1 = node.getStateBeforeStmt().getSelectedGoalNode().getData().getNode(); Node node1 = node.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
...@@ -331,8 +351,8 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation { ...@@ -331,8 +351,8 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
" (line " + lineNumber + " (line " + lineNumber +
")", node1); ")", node1);
} else { } else {
System.out.println(node.getStatement().getNodeName()); return null;
return new TreeNode(node.getStatement().getNodeName(), node.getStateBeforeStmt().getGoals().get(0).getData().getNode()); // return new TreeNode(node.getStatement().getNodeName(), node.getStateBeforeStmt().getGoals().get(0).getData().getNode());
} }
} catch (Exception e) { } catch (Exception e) {
e.printStackTrace(); e.printStackTrace();
......
...@@ -24,7 +24,7 @@ public class ProofTreeTest { ...@@ -24,7 +24,7 @@ public class ProofTreeTest {
private List<ProofScript> scripts; private List<ProofScript> scripts;
private Interpreter<KeyData> interpreter; private Interpreter<KeyData> interpreter;
private static void printTree(TreeItem<ProofTree.TreeNode> rootItem, int level) { private static void printTree(TreeItem<TreeNode> rootItem, int level) {
System.out.format("%s* %s%n", Strings.repeat(" ", level * 4), rootItem.getValue().label); System.out.format("%s* %s%n", Strings.repeat(" ", level * 4), rootItem.getValue().label);
rootItem.getChildren().forEach(item -> { rootItem.getChildren().forEach(item -> {
printTree(item, level+1); printTree(item, level+1);
...@@ -45,15 +45,15 @@ public class ProofTreeTest { ...@@ -45,15 +45,15 @@ public class ProofTreeTest {
interpreter = ib.build(); interpreter = ib.build();
DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, scripts.get(0)); DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, scripts.get(0));
interpreter.interpret(scripts.get(0)); interpreter.interpret(scripts.get(0));
ScriptTreeTransformation treeScriptCreation = new ScriptTreeTransformation(df.getPtreeManager(), facade.getProof(), facade.getProof().root()); ScriptTreeTransformation treeScriptCreation = new ScriptTreeTransformation(df.getPtreeManager());
treeScriptCreation.create(facade.getProof()); treeScriptCreation.create(facade.getProof());
PTreeNode startNode = df.getPtreeManager().getStartNode(); PTreeNode startNode = df.getPtreeManager().getStartNode();
if (startNode != null) { if (startNode != null) {
TreeItem<TreeNode> treeItem = treeScriptCreation.buildScriptTree(startNode); TreeItem<TreeNode> treeItem = treeScriptCreation.buildScriptTree(startNode, facade.getProof());
System.out.println("treeItem = " + treeItem);
} }
TreeItem<ProofTree.TreeNode> rootItem = treeScriptCreation.create(ib.getProof()); TreeItem<TreeNode> rootItem = treeScriptCreation.create(ib.getProof());
printTree(rootItem, 0); printTree(rootItem, 0);
} }
......
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