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

Implementation of trycase such that listsners are only infomred when try was successful

parent 9bc8b3f8
Pipeline #13336 failed with stage
in 2 minutes and 46 seconds
......@@ -204,4 +204,5 @@ public class InterpreterBuilder {
interpreter.newState(startGoal);
return this;
}
}
......@@ -43,6 +43,7 @@ public class KeyInterpreter extends Interpreter<KeyData> {
}
@Override
public Object visit(ClosesCase closesCase) {
State<KeyData> currentStateToMatch = peekState();
......@@ -75,14 +76,21 @@ public class KeyInterpreter extends Interpreter<KeyData> {
}
@Override
public Object visit(TryCase TryCase) {
public Object visit(TryCase tryCase) {
State<KeyData> currentStateToMatch = peekState();
State<KeyData> currentStateToMatchCopy = currentStateToMatch.copy(); //deepcopy
GoalNode<KeyData> selectedGoalNode = currentStateToMatch.getSelectedGoalNode();
GoalNode<KeyData> selectedGoalCopy = currentStateToMatch.getSelectedGoalNode().deepCopy(); //deepcopy
enterScope(TryCase);
executeBody(TryCase.getBody(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
//historylistener for recording try
logger.info(String.format("Beginning side computation of %s", tryCase.getNodeName()));
startSideComputation();
TryCaseHistoryLogger list = new TryCaseHistoryLogger(this);
enterScope(tryCase);
executeBody(tryCase.getBody(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
State<KeyData> stateafterIsClosable = peekState();
List<GoalNode<KeyData>> goals = stateafterIsClosable.getGoals();
boolean allClosed = true;
......@@ -93,18 +101,27 @@ public class KeyInterpreter extends Interpreter<KeyData> {
break;
}
}
logger.info(String.format("Ended Side Computation of %s", tryCase.getNodeName()));
endSideComputation();
if (!allClosed) {
System.out.println("IsClosable was not successful, rolling back proof");
logger.info("Try was not successful, rolling back proof");
Proof currentKeYproof = selectedGoalNode.getData().getProof();
ImmutableList<Goal> subtreeGoals = currentKeYproof.getSubtreeGoals(((KeyData) selectedGoalNode.getData()).getNode());
currentKeYproof.pruneProof(selectedGoalCopy.getData().getNode());
popState();
pushState(currentStateToMatchCopy);
}
} else {
//replay all proof events
//check if state is closed
exitScope(TryCase);
exitScope(tryCase);
list.printSequenceOfEvents();
list.replayEvents(this);
logger.info("Replaying Events finished");
}
return allClosed;
/* //executeBody and if goal is closed afterwards return true
//else prune proof and return false
......
package edu.kit.iti.formal.psdbg.interpreter;
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.State;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import javafx.util.Pair;
import lombok.Getter;
import lombok.Setter;
import java.util.HashMap;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
/**
* Logger for Interpreting a try case. If the case was successful,
* the logged Events can be replayed by the parent interpreter listeners
*/
public class TryCaseHistoryLogger extends HistoryListener {
private Interpreter currentInterpreter;
private EntryListener entryListener = new EntryListener();
;
private ExitListener exitListener = new ExitListener();
private Map<ASTNode, EntryExitPair> mapOfNodesAndStates = new HashMap<>();
private List<Pair<EntryName, ASTNode>> sequenceOfEvents = new LinkedList<>();
public TryCaseHistoryLogger(Interpreter interpreter) {
super(interpreter);
this.currentInterpreter = interpreter;
install(interpreter);
}
public void install(Interpreter interpreter) {
if (currentInterpreter != null) deinstall(interpreter);
interpreter.getEntryListeners().add(entryListener);
interpreter.getExitListeners().add(exitListener);
this.currentInterpreter = interpreter;
}
public void deinstall(Interpreter interpreter) {
if (interpreter != null) {
interpreter.getEntryListeners().remove(entryListener);
interpreter.getExitListeners().remove(exitListener);
}
}
public void printSequenceOfEvents() {
for (int i = 0; i < sequenceOfEvents.size(); i++) {
Pair<EntryName, ASTNode> entryNameASTNodePair = sequenceOfEvents.get(i);
System.out.println(entryNameASTNodePair.getKey() + " " + entryNameASTNodePair.getValue().getStartPosition());
}
}
private Void createNewEntry(ASTNode node, State state) {
this.sequenceOfEvents.add(new Pair<>(EntryName.ENTRY, node));
this.mapOfNodesAndStates.put(node, new EntryExitPair(state));
return null;
}
private Void updateEntry(ASTNode node, State state) {
this.sequenceOfEvents.add(new Pair<>(EntryName.EXIT, node));
this.mapOfNodesAndStates.get(node).setExitState(state);
return null;
}
/**
* Play events back to interpreter that listeners are informed about computation
*
* @param interpreter
*/
public void replayEvents(Interpreter interpreter) {
assert sequenceOfEvents.get(0).getKey().equals(EntryName.ENTRY);
//get entry and exit listeners to inform about events
List<Visitor> entryListeners = interpreter.getEntryListeners();
List<Visitor> exitListeners = interpreter.getExitListeners();
//assert start state is equal to first entry state
State<GoalNode<KeyData>> entryState = mapOfNodesAndStates.get(sequenceOfEvents.get(0).getValue()).entryState;
assert interpreter.peekState().equals(entryState);
for (Pair<EntryName, ASTNode> nextevent : sequenceOfEvents) {
ASTNode node = nextevent.getValue();
if (nextevent.getKey().equals(EntryName.ENTRY)) {
if (entryListeners.size() != 0) {
entryListeners.forEach(node::accept);
}
interpreter.popState();
interpreter.pushState(mapOfNodesAndStates.get(node).entryState);
} else {
if (exitListeners.size() != 0) {
exitListeners.forEach(node::accept);
}
interpreter.popState();
interpreter.pushState(mapOfNodesAndStates.get(node).exitState);
}
}
//interpreter.popState()
}
private enum EntryName {ENTRY, EXIT}
private class EntryExitPair {
@Getter
@Setter
private State<GoalNode<KeyData>> entryState;
@Getter
@Setter
private State<GoalNode<KeyData>> exitState;
public EntryExitPair(State<GoalNode<KeyData>> entry, State<GoalNode<KeyData>> exit) {
this.entryState = entry;
this.exitState = exit;
}
public EntryExitPair(State<GoalNode<KeyData>> entryState) {
this.entryState = entryState;
}
}
private class EntryListener extends DefaultASTVisitor<Void> {
@Override
public Void defaultVisit(ASTNode node) {
return createNewEntry(node, currentInterpreter.peekState());
}
}
private class ExitListener extends DefaultASTVisitor<Void> {
@Override
public Void defaultVisit(ASTNode node) {
return updateEntry(node, currentInterpreter.peekState());
}
}
}
......@@ -30,13 +30,18 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
implements ScopeObservable {
private static final int MAX_ITERATIONS = 5;
private static Logger logger = Logger.getLogger("interpreter");
protected static Logger logger = Logger.getLogger("interpreter");
//TODO later also include information about source line for each state (for debugging purposes and rewind purposes)
private Stack<State<T>> stateStack = new Stack<>();
@Getter
private List<Visitor> entryListeners = new ArrayList<>(),
exitListeners = new ArrayList<>();
private Stack<List<Visitor>> entryListenerStack = new Stack<>();
private Stack<List<Visitor>> exitListenerStack = new Stack<>();
//@Getter
//private List<Visitor> entryListeners = new ArrayList<>(),
// exitListeners = new ArrayList<>();
@Getter
@Setter
private MatcherApi<T> matcherApi;
......@@ -52,6 +57,18 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
public Interpreter(CommandLookup lookup) {
functionLookup = lookup;
entryListenerStack.push(new ArrayList<>());
exitListenerStack.push(new ArrayList<>());
}
@Override
public List<Visitor> getExitListeners() {
return exitListenerStack.peek();
}
@Override
public List<Visitor> getEntryListeners() {
return entryListenerStack.peek();
}
/**
......@@ -141,8 +158,8 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
enterScope(expr);
Evaluator evaluator = new Evaluator(g.getAssignments(), g);
evaluator.setMatcher(matcherApi);
evaluator.getEntryListeners().addAll(entryListeners);
evaluator.getExitListeners().addAll(exitListeners);
evaluator.getEntryListeners().addAll(entryListenerStack.peek());
evaluator.getExitListeners().addAll(exitListenerStack.peek());
exitScope(expr);
return evaluator.eval(expr);
}
......@@ -416,8 +433,8 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
private VariableAssignment evaluateMatchInGoal(Expression matchExpression, GoalNode<T> goal) {
enterScope(matchExpression);
MatchEvaluator mEval = new MatchEvaluator(goal.getAssignments(), goal, matcherApi);
mEval.getEntryListeners().addAll(entryListeners);
mEval.getExitListeners().addAll(exitListeners);
mEval.getEntryListeners().addAll(entryListenerStack.peek());
mEval.getExitListeners().addAll(exitListenerStack.peek());
exitScope(matchExpression);
List<VariableAssignment> matchResult = mEval.eval(matchExpression);
......@@ -709,6 +726,24 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
return getCurrentState().getGoals();
}
//endregion
/**
* Start a new context where already registered listsners are not informed
*/
protected void startSideComputation() {
entryListenerStack.push(new ArrayList<>());
exitListenerStack.push(new ArrayList<>());
}
/**
* End side computation and restore listeners
*/
protected void endSideComputation() {
assert !exitListenerStack.empty() && !entryListenerStack.empty();
entryListenerStack.pop();
exitListenerStack.pop();
}
}
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