Skip to content

GitLab

P
ProofScriptParser
Commit 22c5c2ac authored by Sarah Grebing's avatar Sarah Grebing
Browse files
Options

Big Bugfix

parent 6019bbae
Pipeline #14592 failed with stage
    in 2 minutes and 52 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 254 additions and 98 deletions
    rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java
    View file @ 22c5c2ac
    ......@@ -100,9 +100,10 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
    */
    @Override
    public Object visit(ProofScript proofScript) {
    enterScope(proofScript);
    //add vars
    visit(proofScript.getSignature());
    enterScope(proofScript);
    proofScript.getBody().accept(this);
    exitScope(proofScript);
    return null;
    ......@@ -519,6 +520,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
    @Override
    public Object visit(CallStatement call) {
    enterScope(call);
    // System.out.println(stateStack.peek().hashCode());
    //neuer VarScope
    //enter new variable scope
    VariableAssignment params = evaluateParameters(call.getParameters());
    ......@@ -535,6 +537,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
    //pushState(newErrorState);
    }
    g.exitScope();
    // System.out.println(stateStack.peek().hashCode());
    exitScope(call);
    return null;
    }
    ......@@ -614,11 +617,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
    @Override
    public Object visit(Signature signature) {
    exitScope(signature);
    // enterScope(signature);
    GoalNode<T> node = getSelectedNode();
    node.enterScope();
    signature.forEach(node::declareVariable);
    enterScope(signature);
    // exitScope(signature);
    return null;
    }
    ......
    rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java
    View file @ 22c5c2ac
    ......@@ -112,4 +112,6 @@ public class GoalNode<T> {
    assignments = assignments.push(va);
    return assignments;
    }
    }
    rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/InterpreterExtendedState.java
    View file @ 22c5c2ac
    package edu.kit.iti.formal.psdbg.interpreter.data;
    import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
    import edu.kit.iti.formal.psdbg.parser.ast.CaseStatement;
    import lombok.Data;
    import lombok.Getter;
    import lombok.RequiredArgsConstructor;
    import lombok.Setter;
    import java.util.*;
    import java.util.stream.Collectors;
    import java.util.Collections;
    import java.util.HashMap;
    import java.util.List;
    import java.util.Map;
    @RequiredArgsConstructor
    @Data
    public class InterpreterExtendedState<T> {
    public class InterpreterExtendedState<T> extends State<T> {
    @Getter
    @Setter
    private Map<CaseStatement, List<GoalNode<T>>> mappingOfCaseToStates = new HashMap<>();
    public InterpreterExtendedState(Collection<GoalNode<T>> goals, GoalNode selected) {
    super(goals, selected);
    }
    /**
    * State before the statement;
    */
    @Getter
    @Setter
    private State<T> stateBeforeStmt;
    /**
    * State after execution of statement
    */
    @Getter
    @Setter
    private State<T> stateAfterStmt;
    /**
    * Statement
    */
    @Getter
    @Setter
    private ASTNode stmt;
    /**
    * Null if root
    */
    @Getter
    @Setter
    private InterpreterExtendedState<T> predecessor;
    public InterpreterExtendedState(Collection<GoalNode<T>> goals, GoalNode selected, Map<CaseStatement, List<GoalNode<T>>> casesMapping) {
    super(goals, selected);
    this.mappingOfCaseToStates = casesMapping;
    }
    public Map<CaseStatement, List<GoalNode<T>>> getMappingOfCaseToStates() {
    return mappingOfCaseToStates;
    public InterpreterExtendedState(InterpreterExtendedState<T> pred) {
    if (pred == null) {
    this.predecessor = null;
    } else {
    this.predecessor = pred;
    }
    }
    public void setMappingOfCaseToStates(Map<CaseStatement, List<GoalNode<T>>> mappingOfCaseToStates) {
    this.mappingOfCaseToStates = mappingOfCaseToStates;
    public InterpreterExtendedState copy() {
    InterpreterExtendedState ext = new InterpreterExtendedState();
    if (this.predecessor != null) {
    ext.setPredecessor(this.predecessor.copy());
    } else {
    ext.predecessor = null;
    }
    ext.setStmt(stmt.copy());
    if (stateAfterStmt != null) {
    ext.setStateAfterStmt(this.stateAfterStmt.copy());
    } else {
    ext.setStateAfterStmt(null);
    }
    if (stateBeforeStmt != null) {
    ext.setStateBeforeStmt(this.stateBeforeStmt.copy());
    } else {
    ext.setStateBeforeStmt(null);
    }
    return ext;
    }
    /*
    public List<GoalNode<T>> getClosedNodes() {
    return super.getGoals().stream().filter(nodes -> nodes.isClosed()).collect(Collectors.toList());
    }
    public List<GoalNode<T>> getopenNodes() {
    public List<GoalNode<T>> getOpenNodes() {
    return super.getGoals().stream().filter(nodes -> !nodes.isClosed()).collect(Collectors.toList());
    }
    }*/
    public List<GoalNode<T>> getActiveGoalsForCase(CaseStatement caseStmt) {
    return mappingOfCaseToStates.getOrDefault(caseStmt, Collections.emptyList());
    }
    @Override
    public String toString() {
    StringBuilder sb = new StringBuilder("\n%%%%%%%%%%%%%%%%%%%%%\nExtended State ");
    if (getStmt() != null) {
    sb.append(getStmt().getNodeName() + ": \n");
    }
    sb.append("State before Statement: \n");
    if (stateBeforeStmt != null) {
    stateBeforeStmt.getGoals().stream().map(tGoalNode -> tGoalNode.getData()).forEach(sb::append);
    } else {
    sb.append("Before is Empty");
    }
    sb.append("\nAfter Statement:\n");
    if (stateAfterStmt != null) {
    stateAfterStmt.getGoals().stream().map(tGoalNode -> tGoalNode.getData()).forEach(sb::append);
    } else {
    sb.append("After is empty");
    }
    sb.append("\n%%%%%%%%%%%%%%%%%%%%\n");
    return sb.toString();
    // this.stateBeforeStmt.toString()+"\n"+this.stateAfterStmt.toString();
    }
    //getuserSelected/
    //verfuegbar im case
    //map<case, listgoal>
    ......
    rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/GraphChangedListener.java
    View file @ 22c5c2ac
    ......@@ -10,4 +10,5 @@ public interface GraphChangedListener {
    abstract void graphChanged(NodeAddedEvent nodeAddedEvent);
    }
    rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
    View file @ 22c5c2ac
    ......@@ -3,7 +3,6 @@ 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 edu.kit.iti.formal.psdbg.parser.ast.CaseStatement;
    import java.util.LinkedList;
    ......@@ -66,11 +65,8 @@ public class PTreeNode<T> {
    return extendedState;
    }
    public void setExtendedState(State<T> state) {
    this.extendedState = new InterpreterExtendedState<>(state.getGoals(), state.getSelectedGoalNode());
    if (getScriptstmt() instanceof CaseStatement) {
    }
    public void setExtendedState(InterpreterExtendedState<T> extendedState) {
    this.extendedState = extendedState;
    }
    public String toString() {
    ......@@ -95,6 +91,7 @@ public class PTreeNode<T> {
    }
    public String extendedStateToString() {
    return this.extendedState.toString();
    }
    }
    rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
    View file @ 22c5c2ac
    ......@@ -6,6 +6,7 @@ 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.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;
    ......@@ -13,16 +14,18 @@ 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.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
    ......@@ -53,7 +56,7 @@ public class StateGraphWrapper<T> {
    private PTreeNode<T> lastNode;
    /**
    * Mapping ASTNode to PTreeNode
    * Mapping ASTNode to PTreeNode for lookup
    */
    private HashMap<ASTNode, PTreeNode> addedNodes = new LinkedHashMap<>();
    ......@@ -75,7 +78,7 @@ public class StateGraphWrapper<T> {
    this.mainScript = mainScript;
    createRootNode(this.mainScript);
    // createRootNode(this.mainScript);
    }
    ......@@ -91,15 +94,29 @@ public class StateGraphWrapper<T> {
    public void createRootNode(ASTNode node) {
    LOGGER.info("Creating Root for State graph");
    PTreeNode newStateNode = new PTreeNode(node);
    newStateNode.setState(currentInterpreter.getCurrentState().copy());
    State<T> currentInterpreterStateCopy = currentInterpreter.getCurrentState().copy();
    //copy current state before executing statement
    newStateNode.setState(currentInterpreterStateCopy);
    //create extended State
    InterpreterExtendedState extState = new InterpreterExtendedState();
    extState.setStmt(node);
    extState.setStateBeforeStmt(currentInterpreterStateCopy);
    newStateNode.setExtendedState(extState);
    //add node to state graph
    boolean res = stateGraph.addNode(newStateNode);
    if (!res) {
    throw new StateGraphException("Could not create new state for ASTNode " + node + " and add it to the stategraph");
    } else {
    this.root.set(newStateNode);
    //to keep track of added nodes
    addedNodes.put(node, newStateNode);
    // fireNodeAdded(new NodeAddedEvent(null, newStateNode));
    lastNode = newStateNode;
    }
    }
    public void setUpGraph() {
    ......@@ -112,19 +129,18 @@ public class StateGraphWrapper<T> {
    //careful TODO look for right edges
    //TODO handle endpoint of graph
    public PTreeNode getStepOver(PTreeNode statePointer) {
    /*Set<PTreeNode> pTreeNodesNeigbours = stateGraph.adjacentNodes(statePointer);
    if(pTreeNodesNeigbours.isEmpty()){
    return null;
    }else{
    pTreeNodesNeigbours.forEach(e-> System.out.println(e.getScriptstmt().getNodeName()+e.getScriptstmt().getStartPosition()));
    }*/
    if (statePointer == null) {
    return this.rootProperty().get();
    }
    //look for successors in the graph
    Set<PTreeNode> successors = this.stateGraph.successors(statePointer);
    //if there are no successors they have to be computed therefore return null, to trigger the proof tree controller
    if (successors.isEmpty()) {
    return null;
    } else {
    //if there are successors we want those which are connetced with State-Flow
    Object[] sucs = successors.toArray();
    getNodeWithEdgeType(statePointer, EdgeTypes.STATE_FLOW);
    return (PTreeNode) sucs[0];
    ......@@ -136,11 +152,10 @@ public class StateGraphWrapper<T> {
    public PTreeNode getStepBack(PTreeNode statePointer) {
    Set<PTreeNode> pred = this.stateGraph.predecessors(statePointer);
    //if pred is empty we have reached the root
    if (pred.isEmpty()) {
    return null;
    return statePointer;
    } else {
    Object[] sucs = pred.toArray();
    return (PTreeNode) sucs[0];
    ......@@ -179,71 +194,96 @@ public class StateGraphWrapper<T> {
    * @return
    */
    private Void createNewNode(ASTNode node) {
    //save old pointer of last node
    State<T> lastState = lastNode.getState();
    //create a new ProofTreeNode in graph with ast node as parameter
    PTreeNode newStateNode;
    newStateNode = new PTreeNode(node);
    //State<KeyData> currentState = currentInterpreter.getCurrentState().copy();
    //System.out.println("Equals of states " + currentState.equals(lastState));
    //newStateNode.setState(currentState);
    //get the state before executing ast node to save it to the extended state
    //State<T> currentState = currentInterpreter.getCurrentState().copy();
    InterpreterExtendedState<T> extState;
    //set pointer to parent extended state
    if (lastNode.getExtendedState() != null) {
    extState = new InterpreterExtendedState<T>(lastNode.getExtendedState().copy());
    } else {
    extState = new InterpreterExtendedState<T>();
    }
    extState.setStmt(node);
    // extState.setStateBeforeStmt(lastNode.getExtendedState().getStateAfterStmt());
    extState.setStateBeforeStmt(lastState);
    newStateNode.setExtendedState(extState);
    stateGraph.addNode(newStateNode);
    stateGraph.putEdgeValue(lastNode, newStateNode, EdgeTypes.STATE_FLOW);
    //inform listeners about a new node in the graph
    fireNodeAdded(new NodeAddedEvent(lastNode, newStateNode));
    addedNodes.put(node, newStateNode);
    lastNode = newStateNode;
    return null;
    }
    private void fireNodeAdded(NodeAddedEvent nodeAddedEvent) {
    changeListeners.forEach(list -> {
    Platform.runLater(() -> {
    list.graphChanged(nodeAddedEvent);
    // System.out.println("New StateGraphChange " + this.asdot());
    });
    });
    }
    /**
    * If visting a cases statement special care has to be taken for the extended state
    *
    * @param casesStatement
    * @return
    */
    private Void createNewCasesNode(CasesStatement casesStatement) {
    State<T> lastState = lastNode.getState();
    PTreeNode newStateNode;
    newStateNode = new PTreeNode(casesStatement);
    State<T> currentState = currentInterpreter.getCurrentState().copy();
    //merge des alten ext fehlt
    InterpreterExtendedState extState = new InterpreterExtendedState(lastNode.getExtendedState().copy());
    extState.setStateBeforeStmt(lastState);
    extState.setStmt(casesStatement);
    newStateNode.setExtendedState(extState);
    stateGraph.addNode(newStateNode);
    stateGraph.putEdgeValue(lastNode, newStateNode, EdgeTypes.STATE_FLOW);
    fireNodeAdded(new NodeAddedEvent(lastNode, newStateNode));
    addedNodes.put(casesStatement, newStateNode);
    lastNode = newStateNode;
    return null;
    }
    public Void addState(ASTNode node) {
    //get node from addedNodes Map
    PTreeNode newStateNode = addedNodes.get(node);
    //copy Current Interpreter state
    State<T> currentState = currentInterpreter.getCurrentState().copy();
    newStateNode.setState(currentState);
    newStateNode.setExtendedState(currentState);
    //set the state
    if (node != this.root.get().getScriptstmt()) {
    newStateNode.setState(currentState);
    newStateNode.getExtendedState().setStateAfterStmt(currentState);
    } else {
    // newStateNode.setState(currentState);
    newStateNode.getExtendedState().setStateAfterStmt(currentState);
    }
    System.out.println("\n%%%%%%%%%%%%%%%%%%\nExtended State for " + node.getStartPosition() + "\n" + newStateNode.getExtendedState().toString() + "\n%%%%%%%%%%%%%%%%%%\n");
    return null;
    }
    public void install(Interpreter<T> interpreter) {
    if (currentInterpreter != null) deinstall(interpreter);
    interpreter.getEntryListeners().add(entryListener);
    interpreter.getEntryListeners().add(exitListener);
    interpreter.getExitListeners().add(exitListener);
    currentInterpreter = interpreter;
    }
    public void deinstall(Interpreter<T> interpreter) {
    if (interpreter != null) {
    interpreter.getEntryListeners().remove(entryListener);
    interpreter.getEntryListeners().remove(exitListener);
    }
    }
    public String asdot() {
    StringBuilder sb = new StringBuilder();
    sb.append("digraph G {\nnode [shape=rect]\n ");
    stateGraph.nodes().forEach(n -> {
    sb.append(n.hashCode())
    .append(" [label=\"")
    .append(n.getScriptstmt().getNodeName())
    .append("@")
    .append(n.getScriptstmt().getStartPosition().getLineNumber())
    .append("\"]\n");
    });
    stateGraph.edges().forEach(edge -> {
    sb.append(edge.source().hashCode())
    .append(" -> ")
    .append(edge.target().hashCode())
    .append(" [label=\"")
    .append(stateGraph.edgeValue(edge.source(), edge.target()).name())
    .append("\"]\n");
    });
    sb.append("}");
    return sb.toString();
    }
    public PTreeNode getRoot() {
    return root.get();
    ......@@ -265,14 +305,11 @@ public class StateGraphWrapper<T> {
    changeListeners.remove(listener);
    }
    private void fireNodeAdded(NodeAddedEvent nodeAddedEvent) {
    changeListeners.forEach(list -> {
    Platform.runLater(() -> {
    list.graphChanged(nodeAddedEvent);
    System.out.println("New StateGraphChange " + this.asdot());
    });
    });
    public void deinstall(Interpreter<T> interpreter) {
    if (interpreter != null) {
    interpreter.getEntryListeners().remove(entryListener);
    interpreter.getExitListeners().remove(exitListener);
    }
    }
    public PTreeNode getNode(List<GoalNode<T>> newValue) {
    ......@@ -289,6 +326,37 @@ public class StateGraphWrapper<T> {
    }
    /**
    * Helper for debugging
    * @return
    */
    public String asdot() {
    StringBuilder sb = new StringBuilder();
    sb.append("digraph G {\nnode [shape=rect]\n ");
    stateGraph.nodes().forEach(n -> {
    sb.append(n.hashCode())
    .append(" [label=\"")
    .append(n.getScriptstmt().getNodeName())
    .append("@")
    .append(n.getScriptstmt().getStartPosition().getLineNumber())
    .append("\"]\n");
    });
    stateGraph.edges().forEach(edge -> {
    sb.append(edge.source().hashCode())
    .append(" -> ")
    .append(edge.target().hashCode())
    .append(" [label=\"")
    .append(stateGraph.edgeValue(edge.source(), edge.target()).name())
    .append("\"]\n");
    });
    sb.append("}");
    return sb.toString();
    }
    private class EntryListener extends DefaultASTVisitor<Void> {
    @Override
    public Void visit(ProofScript proofScript) {
    ......@@ -299,6 +367,7 @@ public class StateGraphWrapper<T> {
    createNewNode(proofScript);
    }
    }
    return null;
    }
    ......@@ -310,6 +379,7 @@ public class StateGraphWrapper<T> {
    @Override
    public Void visit(CasesStatement casesStatement) {
    // return createNewCasesNode(casesStatement);
    return createNewNode(casesStatement);
    }
    ......@@ -383,6 +453,7 @@ public class StateGraphWrapper<T> {
    @Override
    public Void visit(CallStatement call) {
    // System.out.println("Call "+call.getCommand()+" "+currentInterpreter.getCurrentState());
    return addState(call);
    }
    ......@@ -415,10 +486,12 @@ public class StateGraphWrapper<T> {
    public Void visit(ClosesCase closesCase) {
    return addState(closesCase);
    }
    /* @Override
    @Override
    public Void visit(ProofScript proofScript) {
    return addState(proofScript);
    }*/
    }
    }
    }
    ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
    View file @ 22c5c2ac
    ......@@ -658,7 +658,7 @@ public class DebuggerMain implements Initializable {
    /**
    * Perform a step back
    *TODO Uebergabe des selctirkten Knotens damit richtiges ausgewählt
    *TODO Uebergabe des selctierten Knotens damit richtiges ausgewählt
    * @param actionEvent
    */
    public void stepBack(ActionEvent actionEvent) {
    ......
    ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
    View file @ 22c5c2ac
    ......@@ -61,7 +61,7 @@ public class ProofTreeController {
    private ReadOnlyBooleanProperty executeNotPossible = interpreterService.runningProperty();
    /**
    * Node that is updated whenever a new node is added to the stategraph (this can only happen in debug mode when stepover is invoked)
    * Node that is updated whenever a new node is added to the stategraph
    */
    private SimpleObjectProperty<PTreeNode> nextComputedNode = new SimpleObjectProperty<>();
    ......@@ -96,6 +96,7 @@ public class ProofTreeController {
    * The mainscipt that is executed
    */
    private SimpleObjectProperty<ProofScript> mainScript = new SimpleObjectProperty<>();
    /**
    * Add a change listener for the stategraph, whenever a new node is added it receives an event
    */
    ......@@ -199,11 +200,11 @@ public class ProofTreeController {
    //ask for root
    currentPointer = stateGraphWrapper.rootProperty().get();
    statePointer = currentPointer;