Commit 6ceb7b2c authored by Sarah Grebing's avatar Sarah Grebing

supporting structures for treegraph interim state

parent b3fa15c9
Pipeline #23408 failed with stages
......@@ -131,4 +131,26 @@ public class PTreeNode<T> {
return stateAfterStmt.getGoals().stream().filter(gn -> gn.getParent().equals(incoming)).collect(Collectors.toList());
}
public <T> PTreeNode<T> getNextPtreeNode(PTreeNode<T> current) {
return (current.getStepInto() != null)? current.getStepInto() :
current.getStepOver();
}
public <T> PTreeNode<T> computeNextPtreeNode(PTreeNode<T> current) {
if(current == null){
return current;
}
if(getNextPtreeNode(current) != null){
return getNextPtreeNode(current);
}
if(current.getStepReturn() != null){
return current.getStepReturn();
} else {
while(current.getStepInvInto() != null){
current = current.getStepInvInto();
}
return getNextPtreeNode(current);
}
}
}
\ No newline at end of file
......@@ -8,6 +8,6 @@ import lombok.RequiredArgsConstructor;
public class DummyGoalNode extends AbstractTreeNode {
@Getter
private boolean closedGoal;
private final boolean closedGoal;
}
......@@ -16,7 +16,7 @@ import lombok.Setter;
public class ScriptTreeNode extends AbstractTreeNode {
@Getter
private final PTreeNode<KeyData> scriptState;
@Getter @Setter
private Node keyNode;
@Getter
private final Node keyNode;
}
......@@ -2,27 +2,64 @@ package edu.kit.iti.formal.psdbg.gui.controls;
import com.google.common.graph.Graph;
import com.google.common.graph.GraphBuilder;
import com.google.common.graph.MutableGraph;
import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.AbstractTreeNode;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.DummyGoalNode;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.ScriptTreeNode;
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.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import java.util.Collections;
public class ScriptTreeGraph {
private ScriptTreeNode rootNode;
private final Graph<AbstractTreeNode> graph =
private final MutableGraph<AbstractTreeNode> graph =
GraphBuilder.directed().allowsSelfLoops(false).build();
public void createGraph(PTreeNode<KeyData> rootPTreeNode, Node root) {
ScriptTreeNode rootNode = new ScriptTreeNode(rootPTreeNode);
rootNode.setKeyNode(root);
graph.nodes().add(rootNode);
ScriptTreeNode rootNode = new ScriptTreeNode(rootPTreeNode, root);
// rootNode.setKeyNode(root);
// graph.addNode(rootNode);
this.rootNode = rootNode;
computeOuterGraph();
}
public void computeOuterGraph(){
//Am Anfang: rootNode
ScriptTreeNode currentScriptNode = rootNode;
PTreeNode<KeyData> currentNode = rootNode.getScriptState();
while(currentNode.getStateAfterStmt() != null) {
if (currentNode.getStateAfterStmt() != null) {
if (currentNode.getStateAfterStmt().getGoals().size() == 1) {
PTreeNode<KeyData> nextPTreeNode = currentNode.computeNextPtreeNode(currentNode);
ScriptTreeNode newNode = new ScriptTreeNode(nextPTreeNode, currentNode.getStateAfterStmt().getGoals().get(0).getData().getNode());
//set parent and children relation
newNode.setParent(currentScriptNode);
currentScriptNode.setChildren(Collections.singletonList(newNode));
//reset Pointer for next round
currentNode = nextPTreeNode;
currentScriptNode = newNode;
} else {
if (currentNode.getStateAfterStmt().getGoals().size() < 1) {
}
}
} else {
break;
}
}
}
}
......@@ -45,7 +45,13 @@ public class ProofTreeTest {
interpreter = ib.build();
DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, scripts.get(0));
interpreter.interpret(scripts.get(0));
ScriptTreeTransformation treeScriptCreation = new ScriptTreeTransformation(df.getPtreeManager());
ScriptTreeGraph stg = new ScriptTreeGraph();
stg.createGraph(df.getPtreeManager().getStartNode(), facade.getProof().root());
System.out.println("stg = " + stg);
/* ScriptTreeTransformation treeScriptCreation = new ScriptTreeTransformation(df.getPtreeManager());
treeScriptCreation.create(facade.getProof());
PTreeNode startNode = df.getPtreeManager().getStartNode();
if (startNode != null) {
......@@ -54,9 +60,10 @@ public class ProofTreeTest {
}
TreeItem<TreeNode> rootItem = treeScriptCreation.create(ib.getProof());
printTree(rootItem, 0);
printTree(rootItem, 0);*/
}
}
\ 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