Commit 8d4f4cc3 authored by Sarah Grebing's avatar Sarah Grebing

INterim State for ScriptTree, structure is build up, now cornercases such as...

INterim State for ScriptTree, structure is build up, now cornercases such as macthing expressions need to be added
parent 969b79ad
Pipeline #23666 passed with stages
in 2 minutes and 55 seconds
...@@ -12,6 +12,7 @@ import lombok.Setter; ...@@ -12,6 +12,7 @@ import lombok.Setter;
import javax.annotation.Nullable; import javax.annotation.Nullable;
import java.util.*; import java.util.*;
import java.util.concurrent.atomic.AtomicInteger;
import java.util.stream.Collectors; import java.util.stream.Collectors;
/** /**
...@@ -26,6 +27,9 @@ import java.util.stream.Collectors; ...@@ -26,6 +27,9 @@ import java.util.stream.Collectors;
@Setter @Setter
@RequiredArgsConstructor @RequiredArgsConstructor
public class PTreeNode<T> { public class PTreeNode<T> {
private final int id;
private final ASTNode statement; private final ASTNode statement;
private Map<CaseStatement, List<GoalNode<T>>> mappingOfCaseToStates = new HashMap<>(); private Map<CaseStatement, List<GoalNode<T>>> mappingOfCaseToStates = new HashMap<>();
......
...@@ -18,6 +18,7 @@ import javax.annotation.Nonnull; ...@@ -18,6 +18,7 @@ import javax.annotation.Nonnull;
import javax.annotation.Nullable; import javax.annotation.Nullable;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.List; import java.util.List;
import java.util.concurrent.atomic.AtomicInteger;
import java.util.function.Consumer; import java.util.function.Consumer;
/** /**
...@@ -27,6 +28,7 @@ import java.util.function.Consumer; ...@@ -27,6 +28,7 @@ import java.util.function.Consumer;
public class StateWrapper<T> implements InterpreterObserver<T> { public class StateWrapper<T> implements InterpreterObserver<T> {
private static final Logger LOGGER = LogManager.getLogger(StateWrapper.class); private static final Logger LOGGER = LogManager.getLogger(StateWrapper.class);
private AtomicInteger id;
@Getter @Setter @Getter @Setter
private Interpreter<T> interpreter; private Interpreter<T> interpreter;
...@@ -51,7 +53,7 @@ public class StateWrapper<T> implements InterpreterObserver<T> { ...@@ -51,7 +53,7 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
public StateWrapper(Interpreter<T> interpreter) { public StateWrapper(Interpreter<T> interpreter) {
install(interpreter); id = new AtomicInteger(0); install(interpreter);
} }
public ASTNode[] getContextCopy() { public ASTNode[] getContextCopy() {
...@@ -64,7 +66,8 @@ public class StateWrapper<T> implements InterpreterObserver<T> { ...@@ -64,7 +66,8 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
public PTreeNode<T> createNode(ASTNode node) { public PTreeNode<T> createNode(ASTNode node) {
LOGGER.info("Creating Root for State graph with statement {}@{}", LOGGER.info("Creating Root for State graph with statement {}@{}",
node.getNodeName(), node.getStartPosition()); node.getNodeName(), node.getStartPosition());
lastNode = new PTreeNode<>(node);
lastNode = new PTreeNode<T>(id.incrementAndGet(), node);
lastNode.setContext(getContextCopy()); lastNode.setContext(getContextCopy());
contextStack.add(node); contextStack.add(node);
State<T> currentInterpreterStateCopy = getInterpreterStateCopy(); State<T> currentInterpreterStateCopy = getInterpreterStateCopy();
......
...@@ -19,4 +19,9 @@ public class ScriptTreeNode extends AbstractTreeNode { ...@@ -19,4 +19,9 @@ public class ScriptTreeNode extends AbstractTreeNode {
@Getter @Getter
private final Node keyNode; private final Node keyNode;
@Override
public String toString(){
return scriptState.getStatement().toString()+" with ID "+scriptState.getId();
}
} }
package edu.kit.iti.formal.psdbg.gui.controls; 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.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.controls.ScriptTree.AbstractTreeNode; 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.gui.controls.ScriptTree.ScriptTreeNode;
import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
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;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode; import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; 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.CaseStatement;
import java.util.Collections; import java.util.*;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.List;
public class ScriptTreeGraph { public class ScriptTreeGraph {
private ScriptTreeNode rootNode; private ScriptTreeNode rootNode;
private Map<Node, AbstractTreeNode> mapping;
private List<Node> front;
private PTreeNode<KeyData> currentNode;
private List<PTreeNode<KeyData>> sortedList;
private final MutableGraph<AbstractTreeNode> graph = private final MutableGraph<AbstractTreeNode> graph =
GraphBuilder.directed().allowsSelfLoops(false).build(); GraphBuilder.directed().allowsSelfLoops(false).build();
public void createGraph(PTreeNode<KeyData> rootPTreeNode, Node root) { public void createGraph(PTreeNode<KeyData> rootPTreeNode, Node root) {
this.currentNode = rootPTreeNode;
ScriptTreeNode rootNode = new ScriptTreeNode(rootPTreeNode, root); ScriptTreeNode rootNode = new ScriptTreeNode(rootPTreeNode, root);
// rootNode.setKeyNode(root); mapping = new HashMap<Node, AbstractTreeNode>();
// graph.addNode(rootNode); front = new ArrayList<>();
sortedList = new ArrayList<>();
mapping.put(root, rootNode);
State<KeyData> stateAfterStmt = rootPTreeNode.getStateAfterStmt();
if (stateAfterStmt != null) {
for (GoalNode<KeyData> g : stateAfterStmt.getGoals()) {
mapping.put(g.getData().getNode(), null);
front.add(g.getData().getNode());
}
}
this.rootNode = rootNode; this.rootNode = rootNode;
computeOuterGraph(); computeList();
compute();
} addParents();
mapping.size();
public void computeOuterGraph(){
//Am Anfang: rootNode
ScriptTreeNode currentScriptNode = rootNode;
PTreeNode<KeyData> currentNode = rootNode.getScriptState();
while (currentNode.getStateAfterStmt() != null) { }
List<GoalNode<KeyData>> goalsAfterStmt = currentNode.getStateAfterStmt().getGoals();
if (goalsAfterStmt.size() == 1) {
PTreeNode<KeyData> nextPTreeNode = currentNode.computeNextPtreeNode(currentNode);
ScriptTreeNode newNode = new ScriptTreeNode(nextPTreeNode, goalsAfterStmt.get(0).getData().getNode());
//set parent and children relation private void addParents() {
newNode.setParent(currentScriptNode); Node current = rootNode.getKeyNode();
currentScriptNode.setChildren(Collections.singletonList(newNode)); AbstractTreeNode currentParent = mapping.get(current);
Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0);
while(iter.hasNext()){
PTreeNode<KeyData> next = iter.next();
if (next.getStateAfterStmt() != null) {
for (GoalNode<KeyData> gn: next.getStateAfterStmt().getGoals()) {
mapping.get(gn.getData().getNode()).setParent(currentParent);
}
}
if(next.getStateBeforeStmt().getSelectedGoalNode() != null) {
current = next.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
currentParent = mapping.get(current);
}
}
//reset Pointer for next round mapping.size();
currentNode = nextPTreeNode; }
currentScriptNode = newNode;
} else if (goalsAfterStmt.size() > 1) {
} else { private void computeList() {
while (currentNode != null) {
sortedList.add(currentNode);
currentNode = currentNode.getNextPtreeNode(currentNode);
}
}
public void compute() {
Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0);
//Node current = rootNode.getKeyNode();
while (iter.hasNext()) {
PTreeNode<KeyData> nextPtreeNode = iter.next();
ASTNode statement = nextPtreeNode.getStatement();
//check for selected node and find the node in map
if (nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode() != null) {
if (statement instanceof CallStatement) {
Node n = nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
ScriptTreeNode sn = new ScriptTreeNode(nextPtreeNode, n);
// sn.setParent(mapping.get(current));
mapping.replace(n, sn);
front.remove(n);
// current = n;
for (GoalNode<KeyData> gn : nextPtreeNode.getStateAfterStmt().getGoals()) {
mapping.put(gn.getData().getNode(), null);
front.add(gn.getData().getNode());
}
}
if(statement instanceof CaseStatement){
}
} }
} }
mapping.size();
mapping.forEach((node, abstractTreeNode) -> System.out.println("node.serialNr() = " + node.serialNr() + " " + abstractTreeNode.toString()));
} }
} }
...@@ -34,7 +34,7 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation { ...@@ -34,7 +34,7 @@ public class ScriptTreeTransformation extends KeyProofTreeTransformation {
currentPointer = p; currentPointer = p;
} }
/** /**
* maps a node to its siblings, that were created by an mutator call. * maps a node to its siblings, that were created by a mutator call.
*/ */
Multimap<Node, Node> entryExitMap = HashMultimap.create(); Multimap<Node, Node> entryExitMap = HashMultimap.create();
......
script full(){
impRight;
impRight;
impLeft;
cases {
case match `!q ==> p`:
notLeft;
notRight;
closeAntec;
case match `q==>!p`:
notLeft;
closeAntec;
}
}
script full1(){ script full1(){
impRight; impRight;
impRight; impRight;
...@@ -11,7 +29,7 @@ script full1(){ ...@@ -11,7 +29,7 @@ script full1(){
script full(){ script full2(){
impRight; impRight;
impRight; impRight;
impLeft; impLeft;
......
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