Skip to content

GitLab

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

interim

parent e6361f70
Hide whitespace changes
Inline Side-by-side
Showing with 210 additions and 142 deletions
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RigidRuleCommandHandler.java 0 → 100644
View file @ a559e78e
package edu.kit.iti.formal.psdbg.interpreter.funchdl;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
public class RigidRuleCommandHandler implements CommandHandler<KeyData> {
@Override
public boolean handles(CallStatement call) throws IllegalArgumentException {
return true;
}
@Override
public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params) {
}
}
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/StateAddedEvent.java
View file @ a559e78e
package edu.kit.iti.formal.psdbg.interpreter;
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.graphs.PTreeNode;
import lombok.Getter;
/**
* Event that is fired if a new state was added to a PTreeNode in the Stategraph
*/
public class StateAddedEvent {
@Getter
PTreeNode changedNode;
......@@ -12,9 +16,13 @@ public class StateAddedEvent {
@Getter
State addedState;
public StateAddedEvent(PTreeNode addedNode, State addedState) {
@Getter
InterpreterExtendedState addedExtState;
public StateAddedEvent(PTreeNode addedNode, State addedState, InterpreterExtendedState addedExtState) {
this.changedNode = addedNode;
this.addedState = addedState;
this.addedExtState = addedExtState;
}
public String toString() {
......
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/InterpreterExtendedState.java
View file @ a559e78e
......@@ -91,7 +91,9 @@ public class InterpreterExtendedState<T> {
@Override
public String toString() {
StringBuilder sb = new StringBuilder("\n%%%%%%%%%%%%%%%%%%%%%\nExtended State ");
StringBuilder sb = new StringBuilder();
//sb.append("\n%%%%%%%%%%%%%%%%%%%%%\n");
sb.append("Extended State ");
if (getStmt() != null) {
sb.append(getStmt().getNodeName() + ": \n");
}
......@@ -107,7 +109,14 @@ public class InterpreterExtendedState<T> {
} else {
sb.append("After is empty");
}
sb.append("\n%%%%%%%%%%%%%%%%%%%%\n");
if (getMappingOfCaseToStates().containsKey(stmt)) {
sb.append("Case Stmt with");
getMappingOfCaseToStates().get(stmt).forEach(tGoalNode -> {
sb.append(tGoalNode.getData());
});
}
//sb.append("\n%%%%%%%%%%%%%%%%%%%%\n");
return sb.toString();
// this.stateBeforeStmt.toString()+"\n"+this.stateAfterStmt.toString();
}
......
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
View file @ a559e78e
......@@ -4,7 +4,7 @@ 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 java.util.LinkedList;
import java.util.Stack;
/**
* Inner class representing nodes in the stategraph graph
......@@ -27,7 +27,15 @@ public class PTreeNode<T> {
/**
* Call context
*/
private LinkedList<ASTNode> context = new LinkedList<>();
private Stack<ASTNode> context = new Stack<>();
public Stack<ASTNode> getContext() {
return context;
}
public void setContext(Stack<ASTNode> context) {
this.context = context;
}
private boolean root;
......@@ -51,19 +59,11 @@ public class PTreeNode<T> {
this.scriptstmt = scriptstmt;
}
public LinkedList<ASTNode> getContext() {
return context;
}
public void setContext(LinkedList<ASTNode> context) {
this.context = context;
}
InterpreterExtendedState<T> getExtendedState() {
public InterpreterExtendedState<T> getExtendedState() {
return extendedState;
}
void setExtendedState(InterpreterExtendedState<T> extendedState) {
public void setExtendedState(InterpreterExtendedState<T> extendedState) {
this.extendedState = extendedState;
}
......@@ -75,10 +75,15 @@ public class PTreeNode<T> {
} else {
sb.append("Root Node");
}
if (hasState()) {
/* 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();
......
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
View file @ a559e78e
......@@ -18,6 +18,10 @@ 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.*;
/**
......@@ -87,35 +91,7 @@ public class StateGraphWrapper<T> {
}
/**
* Create the root Node for the state graph
* @param node
*/
public void createRootNode(ASTNode node) {
LOGGER.info("Creating Root for State graph with statement {}@{}", node.getNodeName(), node.getStartPosition());
PTreeNode<T> newStateNode = new PTreeNode<>(node);
State<T> currentInterpreterStateCopy = currentInterpreter.getCurrentState().copy();
//copy current state before executing statement
newStateNode.setState(currentInterpreterStateCopy);
//create extended State
InterpreterExtendedState<T> 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;
}
}
private static int counter = 0;
public MutableValueGraph<PTreeNode<T>, EdgeTypes> getStateGraph() {
return stateGraph;
......@@ -207,6 +183,41 @@ public class StateGraphWrapper<T> {
return createNewNode(node, false);
}
private static Path graph = Paths.get("/tmp/test.dot");
/**
* Create the root Node for the state graph
*
* @param node
*/
public void createRootNode(ASTNode node) {
LOGGER.info("Creating Root for State graph with statement {}@{}", node.getNodeName(), node.getStartPosition());
PTreeNode<T> newStateNode = new PTreeNode<>(node);
newStateNode.setContext(new Stack<>());
newStateNode.getContext().push(node);
State<T> currentInterpreterStateCopy = currentInterpreter.getCurrentState().copy();
//copy current state before executing statement
newStateNode.setState(currentInterpreterStateCopy);
//create extended State
InterpreterExtendedState<T> 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;
}
}
/**
* Create a new node for the state graph and add edges to already existing nodes
*
......@@ -216,26 +227,49 @@ public class StateGraphWrapper<T> {
private Void createNewNode(ASTNode node, boolean isCasesStmt) {
LOGGER.info("Creating Node for State graph with statement {}@{}", node.getNodeName(), node.getStartPosition());
//save old pointer of last node
State<T> lastState = lastNode.getState();
//State<T> lastState = lastNode.getState();
State<T> lastState;
// if(lastNode.getExtendedState().getStateAfterStmt() != null) {
// lastState = lastNode.getExtendedState().getStateAfterStmt().copy();
// }else{
lastState = currentInterpreter.getCurrentState().copy();
// }
//create a new ProofTreeNode in graph with ast node as parameter
PTreeNode<T> newStateNode = new PTreeNode<>(node);
newStateNode.setContext(lastNode.getContext());
//get the state before executing ast node to save it to the extended state
//State<T> currentState = currentInterpreter.getCurrentState().copy();
InterpreterExtendedState<T> extState;
if (isCasesStmt) {
newStateNode.getContext().push(node);
extState = new InterpreterExtendedState<>(lastNode.getExtendedState().copy());
extState.setStmt(node);
extState.setStateBeforeStmt(lastState);
newStateNode.setState(lastState);
//TODO: implement special handling for cases stmts
//extState = null;
extState.setStateBeforeStmt(lastState.copy());
Map<CaseStatement, List<GoalNode<T>>> mappingOfCaseToStates = extState.getMappingOfCaseToStates();
CasesStatement cs = (CasesStatement) node;
//initialize the cases in the mapping map
cs.getCases().forEach(caseStatement -> {
mappingOfCaseToStates.put(caseStatement, Collections.emptyList());
});
extState.setMappingOfCaseToStates(mappingOfCaseToStates);
//TODO default case
newStateNode.setState(lastState.copy());
} else {
//set pointer to parent extended state
extState = new InterpreterExtendedState<>(lastNode.getExtendedState().copy());
extState.setStmt(node);
extState.setStateBeforeStmt(lastState);
//check whether case statement
if (extState.getMappingOfCaseToStates().containsKey(node)) {
extState.getMappingOfCaseToStates().get(node).add(lastState.getSelectedGoalNode().deepCopy());
extState.setStateBeforeStmt(new State<T>(extState.getMappingOfCaseToStates().get(node), lastState.getSelectedGoalNode().deepCopy()));
} else {
extState.setStateBeforeStmt(lastState);
}
}
newStateNode.setExtendedState(extState);
......@@ -250,31 +284,15 @@ public class StateGraphWrapper<T> {
}
private void fireNodeAdded(NodeAddedEvent nodeAddedEvent) {
counter++;
System.out.println("XXXXXXXXXX counter = " + counter);
changeListeners.forEach(list -> Platform.runLater(() -> {
list.graphChanged(nodeAddedEvent);
LOGGER.debug("New StateGraphChange " + this.asdot());
//TODO
LOGGER.info("New StateGraphChange \n%%%%%%" + this.asdot() + "\n%%%%%%%");
}));
}
private Void addState(ASTNode node) {
LOGGER.info("Adding a new state for statement {}@{}", node.getNodeName(), node.getStartPosition());
//get node from addedNodes Map
PTreeNode<T> newStateNode = addedNodes.get(node);
//copy Current Interpreter state
State<T> currentState = currentInterpreter.getCurrentState().copy();
//set the state
if (node != this.root.get().getScriptstmt()) {
newStateNode.setState(currentState);
newStateNode.getExtendedState().setStateAfterStmt(currentState);
} else {
// newStateNode.setState(currentState);
newStateNode.getExtendedState().setStateAfterStmt(currentState);
}
fireStateAdded(new StateAddedEvent(newStateNode, currentState));
// LOGGER.info("\n%%%%%%%%%%%%%%%%%%\n Extended state for {} updated with {} \n%%%%%%%%%%%%%%%%%%\n", node.getStartPosition(), newStateNode.getExtendedState().toString());
return null;
}
public void install(Interpreter<T> interpreter) {
if (currentInterpreter != null) deinstall(interpreter);
interpreter.getEntryListeners().add(entryListener);
......@@ -337,6 +355,7 @@ public class StateGraphWrapper<T> {
.append(n.getScriptstmt().getNodeName())
.append("@")
.append(n.getScriptstmt().getStartPosition().getLineNumber())
.append(n.extendedStateToString())
.append("\"]\n");
});
......@@ -350,9 +369,47 @@ public class StateGraphWrapper<T> {
});
sb.append("}");
//TODO: debugging
try (java.io.BufferedWriter writer =
java.nio.file.Files.newBufferedWriter(graph, StandardCharsets.UTF_8)
) {
writer.write(sb.toString());
writer.flush();
} catch (IOException e) {
e.printStackTrace();
}
//TODO: end debugging
return sb.toString();
}
private Void addState(ASTNode node) {
LOGGER.info("Adding a new state for statement {}@{}", node.getNodeName(), node.getStartPosition());
//get node from addedNodes Map
PTreeNode<T> newStateNode = addedNodes.get(node);
//copy Current Interpreter state
State<T> currentState = currentInterpreter.getCurrentState().copy();
//set the state
if (node != this.root.get().getScriptstmt()) {
newStateNode.setState(currentState);
newStateNode.getExtendedState().setStateAfterStmt(currentState);
if (newStateNode.getContext().peek().equals(node)) {
newStateNode.getContext().pop();
}
} else {
// newStateNode.setState(currentState);
newStateNode.getExtendedState().setStateAfterStmt(currentState);
if (newStateNode.getContext().peek().equals(node)) {
newStateNode.getContext().pop();
}
}
fireStateAdded(new StateAddedEvent(newStateNode, currentState, newStateNode.getExtendedState()));
LOGGER.debug("Extended state for {} updated with {} \n", node.getStartPosition(), newStateNode.getExtendedState().toString());
return null;
}
private class EntryListener extends DefaultASTVisitor<Void> {
@Override
public Void visit(ProofScript proofScript) {
......@@ -431,11 +488,11 @@ public class StateGraphWrapper<T> {
return addState(assignment);
}
@Override
/* @Override
public Void visit(CasesStatement casesStatement) {
return addState(casesStatement);
}
*/
/*@Override
public Void visit(CaseStatement caseStatement) {
return addState(caseStatement);
......@@ -472,10 +529,10 @@ public class StateGraphWrapper<T> {
return addState(tryCase);
}
@Override
/* @Override
public Void visit(SimpleCaseStatement simpleCaseStatement) {
return addState(simpleCaseStatement);
}
}*/
@Override
public Void visit(ClosesCase closesCase) {
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
View file @ a559e78e
......@@ -10,6 +10,7 @@ import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
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.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.interpreter.graphs.*;
......@@ -118,12 +119,9 @@ public class ProofTreeController {
@Override
public void graphChanged(StateAddedEvent stateAddedEvent) {
PTreeNode changedNode = stateAddedEvent.getChangedNode();
// if(changedNode.getScriptstmt().equals(statePointer.getScriptstmt())){
LOGGER.info("Graph changed by adding a state to PTreeNode: {} and the statepointer points to {}", stateAddedEvent, statePointer);
nextComputedNode.set(changedNode);
Events.fire(new Events.NewNodeExecuted(changedNode.getScriptstmt()));
// }
}
};
......@@ -145,33 +143,9 @@ public class ProofTreeController {
* and bind properties
*/
public ProofTreeController() {
/* blocker.currentStateProperty().addListener((observable, oldValue, newValue) ->
{
Platform.runLater(() -> {
if (newValue != null) {
setNewState(newValue);
}
});
});*/
//get state from blocker, who communicates with interpreter
//this.currentSelectedGoal.bindBidirectional(blocker.currentSelectedGoalProperty());
/* blocker.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> {
Platform.runLater(() -> {
if (newValue != null) {
this.setCurrentSelectedGoal(newValue);
}
});
blocker.currentStateProperty().addListener((observable, oldValue, newValue) -> {
LOGGER.info("The state in the Puppetmaster changed to " + newValue.toString());
});
blocker.currentGoalsProperty().addListener((observable, oldValue, newValue) -> {
Platform.runLater(() -> {
if (newValue != null) {
this.setCurrentGoals(newValue);
}
});
});*/
//add listener to nextcomputed node, that is updated whenever a new node is added to the stategraph
nextComputedNode.addListener((observable, oldValue, newValue) -> {
//update statepointer
......@@ -192,7 +166,7 @@ public class ProofTreeController {
* @param state
*/
private void setNewState(State<KeyData> state) {
// LOGGER.info("Setting new State "+state.toString());
LOGGER.info("Setting new State " + state.toString());
//Statepointer null wenn anfangszustand?
if (statePointer != null && state != null) {
setCurrentHighlightNode(statePointer.getScriptstmt());
......@@ -251,26 +225,21 @@ public class ProofTreeController {
PTreeNode<KeyData> nextNode = stateGraphWrapper.getStepOver(currentPointer);
//if nextnode is null ask interpreter to execute next statement and compute next state
if (nextNode != null) {
if (nextNode != null && nextNode.getExtendedState().getStateAfterStmt() != null) {
PTreeNode<KeyData> lastNode = this.statePointer;
PTreeNode<KeyData> possibleextNode = nextNode;
if (possibleextNode.getState().getGoals() == null || possibleextNode.getState().getGoals().isEmpty() || possibleextNode.getState() == null) {
InterpreterExtendedState<KeyData> extendedStateOfStmt = possibleextNode.getExtendedState();
//check whether we have reached an endpoint in the graph
if (lastNode.equals(nextNode)) {
nextComputedNode.setValue(lastNode);
} else {
nextComputedNode.setValue(possibleextNode);
if (extendedStateOfStmt.getStateBeforeStmt() == null || extendedStateOfStmt.getStateBeforeStmt().getGoals() == null || extendedStateOfStmt.getStateBeforeStmt().getGoals().isEmpty()) {
nextComputedNode.setValue(lastNode);
} else {
nextComputedNode.setValue(possibleextNode);
}
}
/* State<KeyData> lastState = this.statePointer.getState();
this.statePointer = nextNode;
//TODO: replace this code by firing a nodeChangedEvent
State<KeyData> state = this.statePointer.getState();
//if statepointer is at the end, the set of goals is empty therefore return old pointer
if (state.getGoals().isEmpty()) {
setNewState(lastState);
} else {
setNewState(state);
}*/
// setHighlightStmt(this.statePointer.getScriptstmt().getStartPosition(), this.statePointer.getScriptstmt().getStartPosition());
} else {
//no next node is present yet
//let interpreter run for one step and let listener handle updating the statepointer
......@@ -328,24 +297,18 @@ public class ProofTreeController {
blocker.deinstall();
blocker.install(currentInterpreter);
/* if (!debugMode) {
statusBar.setText("Starting in execution mode for script " + mainScript.getName());
statusBar.indicateProgress();
blocker.getStepUntilBlock().set(-1);
} else {*/
statusBar.setText("Starting in debug mode for script " + mainScript.getName());
statusBar.indicateProgress();
setCurrentHighlightNode(mainScript.get());
//build CFG
buildControlFlowGraph(mainScript.get());
//build StateGraph
statusBar.setText("Starting in debug mode for script " + mainScript.getName());
statusBar.indicateProgress();
setCurrentHighlightNode(mainScript.get());
//build CFG
buildControlFlowGraph(mainScript.get());
//build StateGraph
this.stateGraphWrapper = new StateGraphWrapper<>(currentInterpreter, mainScript.get(), this.controlFlowGraphVisitor);
this.stateGraphWrapper.install(currentInterpreter);
this.stateGraphWrapper.addChangeListener(graphChangedListener);
statusBar.stopProgress();
//}
this.stateGraphWrapper.install(currentInterpreter);
this.stateGraphWrapper.addChangeListener(graphChangedListener);
statusBar.stopProgress();
//create interpreter service and start
if (interpreterService.getState() == Worker.State.SUCCEEDED
......@@ -370,7 +333,6 @@ public class ProofTreeController {
statusBar.setText("Failed to execute script");
statusBar.stopProgress();
});
}
/**
......@@ -419,11 +381,6 @@ public class ProofTreeController {
this.currentInterpreter = currentInterpreter;
}
/* public void setMainScript(ProofScript mainScript) {
this.mainScript = mainScript;
}*/
public StateGraphWrapper getStateVisitor() {
return this.stateGraphWrapper;
}
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/PuppetMaster.java
View file @ a559e78e
......@@ -88,7 +88,7 @@ public class PuppetMaster {
//<0 run
if (stepUntilBlock.get() > 0)
stepUntilBlock.decrementAndGet();
System.out.println("Blocker: " + stepUntilBlock.get());
if (stepUntilBlock.get() == 0) {
publishState();
block();
......@@ -111,6 +111,7 @@ public class PuppetMaster {
if (puppet != null) {
final State<KeyData> state = puppet.getCurrentState().copy();
this.setCurrentState(state);
Platform.runLater(() -> {
......
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/fol/script.kps
View file @ a559e78e
......@@ -6,4 +6,17 @@ script main() {
//allLeft formula=`\forall` with=`a`;
allLeft on=`\forall s x; f(f(x)) = f(x)` inst_t=`c`;
}
script proj() {
impRight;
eqSymm formula = `f(c) = f(f(f(c)))`;
allLeft on =`\forall s x; f(f(x)) = f(x)` inst_t=`f(f(c))`;
allLeft on =`\forall s x; f(f(x)) = f(x)` inst_t=`c`;
//applyEqRigid;
//applyEq formula=`f(f(f(c))) = f(c)` occ=`f(f(c))`;
//applyEq formula=`f(f(f(c))) = f(c)` occ=4;
applyEq on=`f(f(c))` formula=`f(f(f(c))) = f(c)` ;
close;
//close formula=`f(f(c))=f(c)`;
}
\ 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