Commit c7ec5de9 authored by Alexander Weigl's avatar Alexander Weigl

Merge remote-tracking branch 'origin/extendedState' into weigl-sync

# Conflicts:
#	rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/ControlFlowVisitor.java
#	rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
#	rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
#	ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
parents bc93a6d2 704840d3
......@@ -25,6 +25,7 @@ package edu.kit.iti.formal.psdbg.parser.ast;
import edu.kit.iti.formal.psdbg.parser.Visitable;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.EqualsAndHashCode;
import lombok.Getter;
import lombok.Setter;
import org.antlr.v4.runtime.ParserRuleContext;
......@@ -35,6 +36,7 @@ import javax.annotation.Nullable;
* @author Alexander Weigl
* @version 1 (27.04.17)
*/
@EqualsAndHashCode
public abstract class ASTNode<T extends ParserRuleContext>
implements Visitable, Copyable<ASTNode<T>> {
/**
......
......@@ -36,11 +36,13 @@ import lombok.*;
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
@Data
@ToString(includeFieldNames = true)
@NoArgsConstructor
@RequiredArgsConstructor()
@AllArgsConstructor
@Getter
@Setter
public class AssignmentStatement
extends Statement<ScriptLanguageParser.AssignmentContext> {
@NonNull
......
......@@ -34,7 +34,8 @@ import lombok.*;
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
@Data
@Getter
@Setter
@NoArgsConstructor
@RequiredArgsConstructor
@AllArgsConstructor
......
......@@ -23,19 +23,20 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.AllArgsConstructor;
import lombok.Data;
import lombok.NoArgsConstructor;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import lombok.Setter;
/**
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
@Data
@NoArgsConstructor
@Getter
@Setter
@RequiredArgsConstructor
@AllArgsConstructor
public class CaseStatement extends Statement<ScriptLanguageParser.CasesListContext> {
public boolean isClosedStmt;
......
......@@ -23,11 +23,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.Data;
import lombok.Getter;
import lombok.NonNull;
import lombok.RequiredArgsConstructor;
import lombok.Setter;
import java.util.ArrayList;
import java.util.List;
......@@ -36,7 +37,9 @@ import java.util.List;
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
@Data
@Setter
@Getter
@RequiredArgsConstructor
public class CasesStatement extends Statement<ScriptLanguageParser.CasesStmtContext> {
@NonNull private final List<CaseStatement> cases = new ArrayList<>();
// @NonNull private Statements defaultCase = new Statements();
......
......@@ -2,9 +2,11 @@ package edu.kit.iti.formal.psdbg.parser.ast;
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.Data;
import lombok.Getter;
import lombok.Setter;
@Data
@Getter
@Setter
public class DefaultCaseStatement extends Statement<ScriptLanguageParser.StmtListContext> {
protected Statements body;
......
......@@ -23,16 +23,17 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.Data;
import lombok.Getter;
import lombok.Setter;
/**
* @author Alexander Weigl
* @version 1 (29.04.17)
*/
@Data
@Getter
@Setter
public class ForeachStatement extends GoalSelector<ScriptLanguageParser.ForEachStmtContext> {
public ForeachStatement() {
}
......
......@@ -31,7 +31,13 @@ import org.antlr.v4.runtime.ParserRuleContext;
* @author Alexander Weigl
* @version 1 (29.04.17)
*/
@Data @AllArgsConstructor @NoArgsConstructor public abstract class GoalSelector<T extends ParserRuleContext>
@Getter
@Setter
@AllArgsConstructor
@NoArgsConstructor
public abstract class GoalSelector<T extends ParserRuleContext>
extends Statement<T> {
@Getter
@Setter
@NonNull private Statements body = new Statements();
}
......@@ -23,16 +23,17 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.Data;
import lombok.Getter;
import lombok.Setter;
/**
* @author Alexander Weigl
* @version 1 (29.04.17)
*/
@Data
@Getter
@Setter
public class RepeatStatement extends GoalSelector<ScriptLanguageParser.RepeatStmtContext> {
public RepeatStatement() {
}
......
......@@ -23,11 +23,9 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitable;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.EqualsAndHashCode;
import lombok.ToString;
import java.util.*;
......@@ -40,7 +38,6 @@ import java.util.stream.Stream;
* @author Alexander Weigl
* @version 1 (27.04.17)
*/
@EqualsAndHashCode
@ToString
public class Statements extends ASTNode<ScriptLanguageParser.StmtListContext>
implements Visitable, Iterable<Statement> {
......@@ -182,4 +179,5 @@ public class Statements extends ASTNode<ScriptLanguageParser.StmtListContext>
s.setRuleContext(this.getRuleContext());
return s;
}
}
......@@ -23,16 +23,17 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.Data;
import lombok.Getter;
import lombok.Setter;
/**
* @author Alexander Weigl
* @version 1 (29.04.17)
*/
@Data
@Getter
@Setter
public class TheOnlyStatement extends GoalSelector<ScriptLanguageParser.TheOnlyStmtContext> {
public TheOnlyStatement() {
}
......
......@@ -7,6 +7,7 @@ import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.ProofScriptHandler;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.util.Pair;
import java.util.*;
......@@ -31,7 +32,7 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
/**
* Control Flow Graph
*/
private MutableValueGraph<ControlFlowNode, ControlFlowTypes> graph = ValueGraphBuilder.directed().allowsSelfLoops(true).build();
private MutableValueGraph<ControlFlowNode, EdgeTypes> graph = ValueGraphBuilder.directed().allowsSelfLoops(true).build();
/**
* Call context
......@@ -44,6 +45,12 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
mappingOfNodes = new HashMap<>();
}
/**
* Return all nodes that have the parameter node as target in the graph
*
* @param node
* @return
*/
public Set<EndpointPair<ControlFlowNode>> getAllEdgesForNodeAsTarget(ASTNode node) {
......@@ -55,9 +62,9 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
if (e.target().equals(assocNode)) {
edges.add(e);
System.out.println(e.target());
System.out.println(e.source());
System.out.println(graph.edgeValue(e.target(), e.source()));
//System.out.println(e.target());
//System.out.println(e.source());
//System.out.println(graph.edgeValue(e.target(), e.source()));
}
});
return edges;
......@@ -66,9 +73,58 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
}
}
public Collection<Pair<ControlFlowNode, EdgeTypes>> getPredecessorsAndTheirEdges(ASTNode node) {
ControlFlowNode assocNode = getCorrespondingNode(node);
List<Pair<ControlFlowNode, EdgeTypes>> allPreds = new LinkedList<>();
if (assocNode != null) {
graph.edges().forEach(edge -> {
if (edge.target().equals(assocNode)) {
allPreds.add(new Pair(edge.source(), graph.edgeValue(edge.source(), edge.target())));
}
});
return allPreds;
} else {
return Collections.EMPTY_LIST;
}
}
public ControlFlowNode getCorrespondingNode(ASTNode node) {
ControlFlowNode ctrl = null;
for (ASTNode astNode : mappingOfNodes.keySet()) {
if (astNode.getStartPosition().equals(node.getStartPosition())
&& astNode.getEndPosition().equals(node.getEndPosition())) {
ctrl = mappingOfNodes.get(astNode);
break;
}
}
return ctrl;
}
public Collection<Pair<ControlFlowNode, EdgeTypes>> getPredecessorsAsTarget(ASTNode node) {
ControlFlowNode assocNode = getCorrespondingNode(node);
List<Pair<ControlFlowNode, EdgeTypes>> allPreds = new LinkedList<>();
if (assocNode != null) {
graph.edges().forEach(edge -> {
if (edge.source().equals(assocNode)) {
allPreds.add(new Pair(edge.target(), graph.edgeValue(edge.source(), edge.target())));
}
});
return allPreds;
} else {
return Collections.EMPTY_LIST;
}
}
@Override
public Void visit(ProofScript proofScript) {
ControlFlowNode scriptNode = new ControlFlowNode(proofScript);
context.add(proofScript);
mappingOfNodes.put(proofScript, scriptNode);
......@@ -93,8 +149,8 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
//ControlFlowNode curLastNode = lastNode;
for (Statement stmnt : statements) {
stmnt.accept(this);
//graph.putEdgeValue(curLastNode, lastNode, ControlFlowTypes.STEP_OVER);
//graph.putEdgeValue(lastNode, curLastNode, ControlFlowTypes.STEP_BACK);
//graph.putEdgeValue(curLastNode, lastNode, EdgeTypes.STEP_OVER);
//graph.putEdgeValue(lastNode, curLastNode, EdgeTypes.STEP_BACK);
//curLastNode = lastNode;
}
//lastNode = curLastNode;
......@@ -106,12 +162,13 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
public Void visit(CallStatement call) {
ControlFlowNode currentNode = new ControlFlowNode(call);
if (!context.isEmpty()) {
currentNode.setCallCtx((ASTNode[]) context.toArray());
currentNode.setCallCtx(context);
}
mappingOfNodes.put(call, currentNode);
graph.addNode(currentNode);
graph.putEdgeValue(lastNode, currentNode, ControlFlowTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, ControlFlowTypes.STEP_BACK);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
lastNode = currentNode;
boolean atomic = functionLookup.isAtomic(call);
......@@ -129,8 +186,8 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
psh.getScript(call.getCommand()).getBody().accept(this);
//verbinde letzten knoten aus auruf mit step return zu aktuellem knoten
graph.putEdgeValue(lastNode, currentNode, ControlFlowTypes.STEP_RETURN);
graph.putEdgeValue(currentNode, lastNode, ControlFlowTypes.STEP_INTO);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_INTO);
context.removeLast();
//check if context is restored properly
......@@ -149,11 +206,11 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
mappingOfNodes.put(foreach, currentNode);
graph.addNode(currentNode);
//System.out.println("\n" + currentNode + "\n");
graph.putEdgeValue(lastNode, currentNode, ControlFlowTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, ControlFlowTypes.STEP_BACK);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
lastNode = currentNode;
foreach.getBody().accept(this);
graph.putEdgeValue(lastNode, currentNode, ControlFlowTypes.STEP_RETURN);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
//lastNode = currentNode; ??
return null;
}
......@@ -164,11 +221,11 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
mappingOfNodes.put(theOnly, currentNode);
graph.addNode(currentNode);
//System.out.println("\n" + currentNode + "\n");
graph.putEdgeValue(lastNode, currentNode, ControlFlowTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, ControlFlowTypes.STEP_BACK);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
lastNode = currentNode;
theOnly.getBody().accept(this);
graph.putEdgeValue(lastNode, currentNode, ControlFlowTypes.STEP_RETURN);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
//lastNode = currentNode; ??
return null;
......@@ -179,11 +236,11 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
ControlFlowNode currentNode = new ControlFlowNode(repeatStatement);
mappingOfNodes.put(repeatStatement, currentNode);
graph.addNode(currentNode);
graph.putEdgeValue(lastNode, currentNode, ControlFlowTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, ControlFlowTypes.STEP_BACK);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
lastNode = currentNode;
repeatStatement.getBody().accept(this);
graph.putEdgeValue(lastNode, currentNode, ControlFlowTypes.STEP_OVER);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
lastNode = currentNode;
return null;
}
......@@ -194,23 +251,23 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
mappingOfNodes.put(casesStatement, casesNode);
graph.addNode(casesNode);
//System.out.println("\n" + casesNode + "\n");
graph.putEdgeValue(lastNode, casesNode, ControlFlowTypes.STEP_OVER);
graph.putEdgeValue(casesNode, lastNode, ControlFlowTypes.STEP_BACK);
graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_OVER);
graph.putEdgeValue(casesNode, lastNode, EdgeTypes.STEP_BACK);
List<CaseStatement> cases = casesStatement.getCases();
for (CaseStatement aCase : cases) {
// if (aCase.isClosedStmt) {
// } else {
ControlFlowNode caseNode = new ControlFlowNode(aCase);
mappingOfNodes.put(aCase, caseNode);
graph.addNode(caseNode);
ControlFlowNode caseNode = new ControlFlowNode(aCase);
mappingOfNodes.put(aCase, caseNode);
graph.addNode(caseNode);
//TODO rethink
graph.putEdgeValue(casesNode, caseNode, ControlFlowTypes.STEP_INTO); //??is this right?
graph.putEdgeValue(caseNode, casesNode, ControlFlowTypes.STEP_BACK);
lastNode = caseNode;
aCase.getBody().accept(this);
graph.putEdgeValue(lastNode, casesNode, ControlFlowTypes.STEP_RETURN);
graph.putEdgeValue(casesNode, caseNode, EdgeTypes.STEP_INTO); //??is this right?
graph.putEdgeValue(caseNode, casesNode, EdgeTypes.STEP_BACK);
lastNode = caseNode;
aCase.getBody().accept(this);
graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_RETURN);
// }
}
//casesStatement.getDefaultCase()
......@@ -220,22 +277,22 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
mappingOfNodes.put(defCase, caseNode);
graph.addNode(caseNode);
//TODO rethink
graph.putEdgeValue(casesNode, caseNode, ControlFlowTypes.STEP_INTO); //??is this right?
graph.putEdgeValue(caseNode, casesNode, ControlFlowTypes.STEP_BACK);
graph.putEdgeValue(casesNode, caseNode, EdgeTypes.STEP_INTO); //??is this right?
graph.putEdgeValue(caseNode, casesNode, EdgeTypes.STEP_BACK);
lastNode = caseNode;
defCase.getBody().accept(this);
graph.putEdgeValue(lastNode, casesNode, ControlFlowTypes.STEP_RETURN);
graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_RETURN);
/*Statements defaultCase = defCase.getBody();
ControlFlowNode caseNode = new ControlFlowNode(defaultCase);
mappingOfNodes.put(defaultCase, caseNode);
graph.addNode(caseNode);
//System.out.println("\n" + caseNode + "\n");
graph.putEdgeValue(casesNode, caseNode, ControlFlowTypes.STEP_OVER); //??is this right?
graph.putEdgeValue(caseNode, casesNode, ControlFlowTypes.STEP_BACK);
graph.putEdgeValue(casesNode, caseNode, EdgeTypes.STEP_OVER); //??is this right?
graph.putEdgeValue(caseNode, casesNode, EdgeTypes.STEP_BACK);
lastNode = caseNode;
defaultCase.accept(this);
graph.putEdgeValue(lastNode, casesNode, ControlFlowTypes.STEP_RETURN);*/
graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_RETURN);*/
}
lastNode = casesNode;
return null;
......@@ -268,8 +325,10 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
return sb.toString();
}
public MutableValueGraph<ControlFlowNode, ControlFlowTypes> getGraph() {
public MutableValueGraph<ControlFlowNode, EdgeTypes> getGraph() {
return graph;
}
}
package edu.kit.iti.formal.psdbg.interpreter.graphs;
import edu.kit.iti.formal.psdbg.interpreter.data.InterpreterExtendedState;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import lombok.Data;
import lombok.Getter;
import lombok.Setter;
import java.util.Stack;
/**
* Inner class representing nodes in the stategraph graph
* A node contains a reference to the ASTNode and a reference to the corresponding interpreter state if this state is already interpreted, null otherwise.
*/
@Data
public class PTreeNode<T> {
/**
* State after statement
*/
//private State<T> state;
private InterpreterExtendedState<T> extendedState = new InterpreterExtendedState<>(null);
/**
* Statement
*/
private ASTNode scriptStmt;
/**
* Call context
*/
@Getter
@Setter
private Stack<ASTNode> context = new Stack<>();
private boolean root;
PTreeNode(ASTNode node) {
this.setScriptStmt(node);
}
public void setExtendedState(InterpreterExtendedState<T> extendedState) {
this.extendedState = extendedState;
}
public String toString() {
StringBuilder sb = new StringBuilder();
sb.append("Node {");
if (scriptStmt != null) {
sb.append(scriptStmt.getNodeName() + "\n");
} else {
sb.append("Root Node");
}
/* if (hasState()) {
sb.append("\nState " + state.getGoals() + "\n");
} else {
sb.append("No State yet");
}*/
if (extendedState != null) {
sb.append(extendedStateToString());
} else {
sb.append("No extended State yet");
}
sb.append("}");
return sb.toString();
}
public String extendedStateToString() {
return this.extendedState.toString();
}
}
package edu.kit.iti.formal.psdbg.interpreter.graphs;
import com.google.common.graph.MutableValueGraph;
import com.google.common.graph.ValueGraphBuilder;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.NodeAddedEvent;
import edu.kit.iti.formal.psdbg.interpreter.StateAddedEvent;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.InterpreterExtendedState;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.StateGraphException;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.application.Platform;
import javafx.beans.property.SimpleObjectProperty;
import lombok.Getter;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import java.io.IOException;
import java.nio.charset.StandardCharsets;
import java.nio.file.Path;
import java.nio.file.Paths;
import java.util.*;
/**
* State graph that is computed on the fly while stepping through script
* A Node in the graph is a PTreeNode {@link PTreeNode}
* Edges are computed on the fly while
*/
public class StateGraphWrapper<T> {
private static final Logger LOGGER = LogManager.getLogger(StateGraphWrapper.class);
/**
* Listeners getting informed when new node added to state graph
*/
@Getter
private List<GraphChangedListener> changeListeners = new ArrayList<>();
/**
* Interpreter
*/
private Interpreter<T> currentInterpreter;
/**
* Graph that is computed on the fly in order to allow stepping
*/
private MutableValueGraph<PTreeNode<T>, EdgeTypes> stateGraph;
/**
* Root of state graph
*/
private SimpleObjectProperty<PTreeNode<T>> root = new SimpleObjectProperty<>();
/**
* last added node
*/
private PTreeNode<T> lastNode;
/**
* Mapping ASTNode to PTreeNode for lookup
*/
private HashMap<ASTNode, PTreeNode<T>> addedNodes = new LinkedHashMap<>();
/**
* Visitor for control flow graph
*/
private ControlFlowVisitor cfgVisitor;
private EntryListener entryListener = new EntryListener();
private ExitListener exitListener = new ExitListener();
private ProofScript mainScript;
/**
* Creates a new state graph and adds the root node with the root state
* @param inter
* @param mainScript
* @param cfgVisitor
*
*/
public StateGraphWrapper(Interpreter<T> inter, ProofScript mainScript, ControlFlowVisitor cfgVisitor) {
stateGraph = ValueGraphBuilder.directed().build();
this.currentInterpreter = inter;
this.cfgVisitor = cfgVisitor;
this.mainScript = mainScript;
createRootNode(this.mainScript);