Skip to content

GitLab

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

interim

parent a559e78e
Hide whitespace changes
Inline Side-by-side
Showing with 214 additions and 114 deletions
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RigidRuleCommandHandler.java
View file @ a6919087
......@@ -14,5 +14,8 @@ public class RigidRuleCommandHandler implements CommandHandler<KeyData> {
@Override
public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params) {
// Evaluator evaluator = new Evaluator(g.getAssignments(), g);
// evaluator.setMatcher(interpreter.getMatcherApi());
//taclet.getExecutor().apply(env.getLoadedProof().root(), env.getServices());
}
}
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Evaluator.java
View file @ a6919087
package edu.kit.iti.formal.psdbg.interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.Operator;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
import edu.kit.iti.formal.psdbg.parser.types.TermType;
import edu.kit.iti.formal.psdbg.parser.types.TypeFacade;
......@@ -67,6 +66,7 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
*/
@Override
public Value visit(MatchExpression match) {
enterScope(match);
if (match.getSignature() != null && !match.getSignature().isEmpty()) {
throw new IllegalStateException("not supported");
}
......@@ -81,7 +81,7 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
}
}
exitScope(match);
return va != null && va.size() > 0 ? Value.TRUE : Value.FALSE;
}
......
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java
View file @ a6919087
......@@ -266,10 +266,12 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
@Override
public Object visit(SimpleCaseStatement simpleCaseStatement) {
Expression matchExpression = simpleCaseStatement.getGuard();
State<T> currentStateToMatch = peekState();
GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
VariableAssignment va = evaluateMatchInGoal(matchExpression, selectedGoal);
if (va != null) {
enterScope(simpleCaseStatement);
executeBody(simpleCaseStatement.getBody(), selectedGoal, va);
......
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
View file @ a6919087
......@@ -71,16 +71,19 @@ public class StateGraphWrapper<T> {
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 inter
* @param mainScript
* @param cfgVisitor
*
*/
public StateGraphWrapper(Interpreter<T> inter, ProofScript mainScript, ControlFlowVisitor cfgVisitor) {
stateGraph = ValueGraphBuilder.directed().build();
......@@ -106,17 +109,11 @@ public class StateGraphWrapper<T> {
return lastNode;
}
public void setUpGraph() {
//create empty graph
stateGraph = ValueGraphBuilder.directed().build();
}
//careful TODO look for right edges
//TODO handle endpoint of graph
public PTreeNode<T> getStepOver(PTreeNode statePointer) {
if (statePointer == null) {
LOGGER.info("Stepover requested for null, therefore returning root");
return this.rootProperty().get();
......@@ -126,6 +123,7 @@ public class StateGraphWrapper<T> {
Set<PTreeNode<T>> 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
......@@ -227,19 +225,13 @@ 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;
// 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) {
......@@ -284,12 +276,12 @@ public class StateGraphWrapper<T> {
}
private void fireNodeAdded(NodeAddedEvent nodeAddedEvent) {
counter++;
System.out.println("XXXXXXXXXX counter = " + counter);
//counter++;
//System.out.println("XXXXXXXXXX counter = " + counter);
changeListeners.forEach(list -> Platform.runLater(() -> {
list.graphChanged(nodeAddedEvent);
//TODO
LOGGER.info("New StateGraphChange \n%%%%%%" + this.asdot() + "\n%%%%%%%");
// LOGGER.info("New StateGraphChange \n%%%%%%" + this.asdot() + "\n%%%%%%%");
}));
}
......@@ -309,11 +301,8 @@ public class StateGraphWrapper<T> {
this.root.set(root);
}
private void fireStateAdded(StateAddedEvent stateAddedEvent) {
changeListeners.forEach(list -> Platform.runLater(() -> {
list.graphChanged(stateAddedEvent);
LOGGER.debug("New StateGraphChange " + this.asdot());
}));
private Void addState(ASTNode node) {
return addState(node, true);
}
public void addChangeListener(GraphChangedListener listener) {
......@@ -385,7 +374,7 @@ public class StateGraphWrapper<T> {
return sb.toString();
}
private Void addState(ASTNode node) {
private Void addState(ASTNode node, boolean fireStateAdded) {
LOGGER.info("Adding a new state for statement {}@{}", node.getNodeName(), node.getStartPosition());
//get node from addedNodes Map
PTreeNode<T> newStateNode = addedNodes.get(node);
......@@ -405,11 +394,20 @@ public class StateGraphWrapper<T> {
newStateNode.getContext().pop();
}
}
fireStateAdded(new StateAddedEvent(newStateNode, currentState, newStateNode.getExtendedState()));
if (fireStateAdded) {
fireStateAdded(new StateAddedEvent(newStateNode, currentState, newStateNode.getExtendedState()));
}
LOGGER.debug("Extended state for {} updated with {} \n", node.getStartPosition(), newStateNode.getExtendedState().toString());
return null;
}
private void fireStateAdded(StateAddedEvent stateAddedEvent) {
changeListeners.forEach(list -> Platform.runLater(() -> {
list.graphChanged(stateAddedEvent);
// LOGGER.debug("New StateGraphChange " + this.asdot());
}));
}
private class EntryListener extends DefaultASTVisitor<Void> {
@Override
public Void visit(ProofScript proofScript) {
......@@ -460,6 +458,11 @@ public class StateGraphWrapper<T> {
return createNewNode(repeatStatement);
}
@Override
public Void visit(MatchExpression matchExpression) {
return createNewNode(matchExpression);
}
@Override
public Void visit(TryCase tryCase) {
return createNewNode(tryCase);
......@@ -488,14 +491,19 @@ public class StateGraphWrapper<T> {
return addState(assignment);
}
/* @Override
@Override
public Void visit(ProofScript proofScript) {
return addState(proofScript, false);
}
@Override
public Void visit(CasesStatement casesStatement) {
return addState(casesStatement);
return addState(casesStatement, false);
}
*/
/*@Override
public Void visit(CaseStatement caseStatement) {
return addState(caseStatement);
return addState(caseStatement, false);
}*/
@Override
......@@ -529,20 +537,17 @@ public class StateGraphWrapper<T> {
return addState(tryCase);
}
/* @Override
@Override
public Void visit(SimpleCaseStatement simpleCaseStatement) {
return addState(simpleCaseStatement);
}*/
return addState(simpleCaseStatement, false);
}
@Override
public Void visit(ClosesCase closesCase) {
return addState(closesCase);
}
/* @Override
public Void visit(ProofScript proofScript) {
return addState(proofScript);
}*/
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/InterpretingService.java
View file @ a6919087
......@@ -22,6 +22,9 @@ public class InterpretingService extends Service<State<KeyData>> {
* The interpreter (with the appropriate KeY state) that is used to traverse and execute the script
*/
private final SimpleObjectProperty<Interpreter<KeyData>> interpreter = new SimpleObjectProperty<>();
/**
* Statusbar for indication of progress
*/
private DebuggerStatusBar statusBar;
/**
......@@ -99,6 +102,7 @@ public class InterpretingService extends Service<State<KeyData>> {
protected edu.kit.iti.formal.psdbg.interpreter.data.State<KeyData> call() throws Exception {
if (statusBar != null) {
statusBar.indicateProgress();
statusBar.publishMessage("Interpreting " + ast.getName());
}
i.interpret(ast);
return i.peekState();
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @ a6919087
......@@ -172,6 +172,7 @@ public class DebuggerMain implements Initializable {
private void marriageProofTreeControllerWithActiveInspectionView() {
InspectionModel imodel = getInspectionViewsController().getActiveInspectionViewTab().getModel();
//set all listeners
proofTreeController.currentGoalsProperty().addListener((o, old, fresh) -> {
if (fresh != null) {
......@@ -495,24 +496,11 @@ public class DebuggerMain implements Initializable {
openKeyFile(keyFile);
}
//endregion
//region Santa's Little Helper
public void openJavaFile() {
loadJavaFile();
showCodeDock(null);
}
//endregion
//region Santa's Little Helper
@FXML
protected void loadJavaFile() {
File javaFile = openFileChooserOpenDialog("Select Java File", "Java Files", "java");
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
View file @ a6919087
......@@ -101,6 +101,20 @@ public class ProofTreeController {
*/
private SimpleObjectProperty<ProofScript> mainScript = new SimpleObjectProperty<>();
/*public State getBlockerState() {
return blockerState.get();
}
public SimpleObjectProperty<State> blockerStateProperty() {
return blockerState;
}
public void setBlockerState(State blockerState) {
this.blockerState.set(blockerState);
}
*/
// private SimpleObjectProperty<State> blockerState = new SimpleObjectProperty<>();
/**
* Add a change listener for the stategraph, whenever a new node is added it receives an event
*/
......@@ -111,7 +125,7 @@ public class ProofTreeController {
if (added.getState() != null) {
LOGGER.info("Graph changed with the following PTreeNode: {} and the statepointer points to {}", nodeAddedEvent.getAddedNode(), statePointer);
nextComputedNode.setValue(nodeAddedEvent.getAddedNode());
Events.fire(new Events.NewNodeExecuted(nodeAddedEvent.getAddedNode().getScriptstmt()));
// Events.fire(new Events.NewNodeExecuted(nodeAddedEvent.getAddedNode().getScriptstmt()));
}
}
......@@ -121,7 +135,8 @@ public class ProofTreeController {
PTreeNode changedNode = stateAddedEvent.getChangedNode();
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()));
//Events.fire(new Events.NewNodeExecuted(changedNode.getScriptstmt()));
}
};
......@@ -138,34 +153,45 @@ public class ProofTreeController {
return mainScript;
}
/**
* Create a new ProofTreeController
* and bind properties
*/
public ProofTreeController() {
blocker.currentStateProperty().addListener((observable, oldValue, newValue) -> {
/* blocker.currentStateProperty().addListener((observable, oldValue, newValue) -> {
//setNewState(newValue);
setBlockerState(newValue);
LOGGER.info("The state in the Puppetmaster changed to " + newValue.toString());
});
});*/
//add listener to nextcomputed node, that is updated whenever a new node is added to the stategraph
nextComputedNode.addListener((observable, oldValue, newValue) -> {
//update statepointer
if (newValue != null) {
LOGGER.info("New node {} was computed and the statepointer was set to {}", newValue.getScriptstmt(), newValue);
this.statePointer = newValue;
//setNewState(blocker.currentStateProperty().get());
setNewState(newValue.getState());
}
});
}
/**
* Sets the properties that may notify GUI about statechanges with new state values
*
* CurrentGoalsProperty and SelectedGoal are both listened by InspectionViewModel
* @param state
*/
private void setNewState(State<KeyData> state) {
LOGGER.info("Setting new State " + state.toString());
//Statepointer null wenn anfangszustand?
if (statePointer != null && state != null) {
......@@ -191,6 +217,7 @@ public class ProofTreeController {
throw new RuntimeException("The state pointer was null when setting new state");
}
}
//TODO handle endpoint
......@@ -223,7 +250,11 @@ public class ProofTreeController {
}
//get next node
PTreeNode<KeyData> nextNode = stateGraphWrapper.getStepOver(currentPointer);
//if nextnode is null ask interpreter to execute next statement and compute next state
if (nextNode != null) {
setCurrentHighlightNode(nextNode.getScriptstmt());
}
if (nextNode != null && nextNode.getExtendedState().getStateAfterStmt() != null) {
PTreeNode<KeyData> lastNode = this.statePointer;
......@@ -297,17 +328,20 @@ public class ProofTreeController {
blocker.deinstall();
blocker.install(currentInterpreter);
statusBar.setText("Starting in debug mode for script " + mainScript.getName());
statusBar.setText("Starting to interpret script " + mainScript.getName());
statusBar.indicateProgress();
setCurrentHighlightNode(mainScript.get());
//build CFG
buildControlFlowGraph(mainScript.get());
//build StateGraph
this.stateGraphWrapper = new StateGraphWrapper<>(currentInterpreter, mainScript.get(), this.controlFlowGraphVisitor);
statusBar.publishMessage("Controlflow graph ws build");
//build StateGraph
this.stateGraphWrapper = new StateGraphWrapper(currentInterpreter, mainScript.get(), this.controlFlowGraphVisitor);
this.stateGraphWrapper.install(currentInterpreter);
this.stateGraphWrapper.addChangeListener(graphChangedListener);
statusBar.publishMessage("Stategraph was set up");
statusBar.stopProgress();
//create interpreter service and start
......@@ -322,6 +356,7 @@ public class ProofTreeController {
interpreterService.start();
interpreterService.setOnSucceeded(event -> {
statusBar.setText("Executed until end of script.");
System.out.println("Number of Goals " + currentGoals.get().size());
//TODO is this the right position??
if (currentGoals.isEmpty()) {
......@@ -344,7 +379,7 @@ public class ProofTreeController {
this.controlFlowGraphVisitor = new ControlFlowVisitor(currentInterpreter.getFunctionLookup());
mainScript.accept(controlFlowGraphVisitor);
this.setMainScript(mainScript);
System.out.println("CFG\n" + controlFlowGraphVisitor.asdot());
LOGGER.debug("CFG\n" + controlFlowGraphVisitor.asdot());
}
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/PuppetMaster.java
View file @ a6919087
......@@ -3,7 +3,6 @@ package edu.kit.iti.formal.psdbg.gui.controller;
import edu.kit.iti.formal.psdbg.interpreter.HistoryListener;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
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;
......@@ -13,7 +12,6 @@ import javafx.application.Platform;
import javafx.beans.property.SimpleObjectProperty;
import java.util.Collections;
import java.util.List;
import java.util.Set;
import java.util.concurrent.ConcurrentSkipListSet;
import java.util.concurrent.atomic.AtomicInteger;
......@@ -30,8 +28,8 @@ public class PuppetMaster {
/**
* Properties that are changed, when new states are added using the blocker
*/
private final SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoals = new SimpleObjectProperty<>();
private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoal = new SimpleObjectProperty<>();
//private final SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoals = new SimpleObjectProperty<>();
//private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoal = new SimpleObjectProperty<>();
private final SimpleObjectProperty<State<KeyData>> currentState = new SimpleObjectProperty<>();
......@@ -46,6 +44,8 @@ public class PuppetMaster {
public SimpleObjectProperty<State<KeyData>> currentStateProperty() {
return currentState;
}
private KeyInterpreter puppet;
private AtomicInteger stepUntilBlock = new AtomicInteger(-1);
private HistoryListener historyLogger;
......@@ -60,9 +60,9 @@ public class PuppetMaster {
install(puppet);
}
public SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoalsProperty() {
/*public SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoalsProperty() {
return currentGoals;
}
}*/
public HistoryListener getHistoryLogger() {
return historyLogger;
......@@ -90,13 +90,14 @@ public class PuppetMaster {
stepUntilBlock.decrementAndGet();
System.out.println("Blocker: " + stepUntilBlock.get());
if (stepUntilBlock.get() == 0) {
publishState();
//publishState();
block();
}
int lineNumber = node.getStartPosition().getLineNumber();
if (brkpnts.contains(lineNumber)) {
publishState();
//publishState();
block();
}
return null;
......@@ -109,17 +110,20 @@ public class PuppetMaster {
//("PuppetMaster.publishState");
//puppet is null if successful interpreter state and publish state
if (puppet != null) {
final State<KeyData> state = puppet.getCurrentState().copy();
this.setCurrentState(state);
Platform.runLater(() -> {
this.setCurrentState(state);
});
/* Platform.runLater(() -> {
//filter whether all goals are closed
Object[] arr = state.getGoals().stream().filter(keyDataGoalNode -> !keyDataGoalNode.isClosed()).toArray();
currentState.set(state);
if (state.getSelectedGoalNode() == null) {
setCurrentState(state);
//currentState.set(state);
/*if (state.getSelectedGoalNode() == null) {
if (arr.length == 0) {
currentGoals.set(Collections.emptyList());
//currentSelectedGoal.set(state.getGoals().get(0));
......@@ -133,14 +137,13 @@ public class PuppetMaster {
currentSelectedGoal.set(state.getSelectedGoalNode());
}
});
});*/
} else {
//if puppet is null an empty state may be reached therefore state get goals etc returns null
Platform.runLater(() -> {
setCurrentState(new State<KeyData>(Collections.emptyList(), null));
currentGoals.set(Collections.emptyList());
currentSelectedGoal.set(null);
// currentGoals.set(Collections.emptyList());
// currentSelectedGoal.set(null);
});
}
......@@ -175,7 +178,7 @@ public class PuppetMaster {
}
public GoalNode<KeyData> getCurrentSelectedGoal() {
/* public GoalNode<KeyData> getCurrentSelectedGoal() {
return currentSelectedGoal.get();
}
......@@ -227,6 +230,7 @@ public class PuppetMaster {
return checkForHalt(assignment);
}
@Override
public Void visit(CasesStatement casesStatement) {
return checkForHalt(casesStatement);
......@@ -237,11 +241,23 @@ public class PuppetMaster {
return checkForHalt(caseStatement);
}
@Override
public Void visit(MatchExpression matchExpression) {
// System.out.println("Checkforhalt matchexpression");
return checkForHalt(matchExpression);
}
@Override
public Void visit(CallStatement call) {
// System.out.println("Checkforhalt callstatement");
return checkForHalt(call);
}
@Override
public Void visit(SimpleCaseStatement simpleCaseStatement) {
return checkForHalt(simpleCaseStatement);
}
@Override
public Void visit(TheOnlyStatement theOnly) {
return checkForHalt(theOnly);
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
View file @ a6919087
......@@ -102,6 +102,21 @@ public class ProofTree extends BorderPane {
treeProof.refresh();
}
/**
* From https://www.programcreek.com/java-api-examples/index.php?api=javafx.scene.control.TreeItem
*
* @param candidate
*/
private static void expandRootToItem(TreeItem candidate) {
if (candidate != null) {
expandRootToItem(candidate.getParent());
if (!candidate.isLeaf()) {
candidate.setExpanded(true);
}
}
}
private TreeCell<Node> cellFactory(TreeView<Node> nodeTreeView) {
TextFieldTreeCell<Node> tftc = new TextFieldTreeCell<>();
tftc.setConverter(new StringConverter<Node>() {
......@@ -132,17 +147,25 @@ public class ProofTree extends BorderPane {
return tftc;
}
/**
*
* @param tftc
*/
private void repaint(TextFieldTreeCell<Node> tftc) {
Node n = tftc.getItem();
tftc.setStyle("");
if (n != null) {
if (n.isClosed()) {
tftc.setStyle("-fx-background-color: greenyellow");
colorOfNodes.putIfAbsent(n, "green");
//tftc.setStyle("-fx-background-color: greenyellow");
}
if (colorOfNodes.containsKey(n)) {
tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";");
}
}
expandRootToItem(tftc.getTreeItem());
}
public Object getColorOfNodes() {
......@@ -182,6 +205,8 @@ public class ProofTree extends BorderPane {
}
}
class TreeItemNode extends TreeItem<Node> {
public TreeItemNode(Node value) {
super(value);
......
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
View file @ a6919087
......@@ -4,9 +4,13 @@ script test23(){
impRight;
impLeft;
cases{
case match `q==>`:
impRight;
notRight;
case match `==>`:
impRight;
notRight;
}