From d0906b076ea5a88cdd6ebcb8d6c3b7e223235123 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Tue, 4 Jul 2017 09:19:31 +0200 Subject: [PATCH] cleaning --- .../DebuggerMainWindowController.java | 6 ++++- .../interpreter/InterpretingService.java | 4 +-- .../formal/interpreter/NodeAddedEvent.java | 1 + .../exceptions/StateGraphException.java | 26 +++++++++++++++++++ .../{ => graphs}/ControlFlowNode.java | 6 ++--- .../interpreter/{ => graphs}/EdgeTypes.java | 4 +-- .../{ => graphs}/GraphChangedListener.java | 4 ++- .../interpreter/{ => graphs}/PTreeNode.java | 4 +-- .../{ => graphs}/ProgramFlowVisitor.java | 2 +- .../{ => graphs}/ProofTreeController.java | 7 ++--- .../{ => graphs}/StateGraphVisitor.java | 23 +++++++++------- .../interpreter/ProgramFlowVisitorTest.java | 1 + 12 files changed, 64 insertions(+), 24 deletions(-) create mode 100644 src/main/java/edu/kit/formal/interpreter/exceptions/StateGraphException.java rename src/main/java/edu/kit/formal/interpreter/{ => graphs}/ControlFlowNode.java (88%) rename src/main/java/edu/kit/formal/interpreter/{ => graphs}/EdgeTypes.java (52%) rename src/main/java/edu/kit/formal/interpreter/{ => graphs}/GraphChangedListener.java (63%) rename src/main/java/edu/kit/formal/interpreter/{ => graphs}/PTreeNode.java (94%) rename src/main/java/edu/kit/formal/interpreter/{ => graphs}/ProgramFlowVisitor.java (99%) rename src/main/java/edu/kit/formal/interpreter/{ => graphs}/ProofTreeController.java (97%) rename src/main/java/edu/kit/formal/interpreter/{ => graphs}/StateGraphVisitor.java (92%) diff --git a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java index 0aed8113..94a3a039 100644 --- a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java +++ b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java @@ -4,8 +4,12 @@ import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.speclang.Contract; import edu.kit.formal.gui.controls.*; import edu.kit.formal.gui.model.RootModel; -import edu.kit.formal.interpreter.*; +import edu.kit.formal.interpreter.Interpreter; +import edu.kit.formal.interpreter.InterpreterBuilder; +import edu.kit.formal.interpreter.KeYProofFacade; import edu.kit.formal.interpreter.data.KeyData; +import edu.kit.formal.interpreter.graphs.PTreeNode; +import edu.kit.formal.interpreter.graphs.ProofTreeController; import edu.kit.formal.proofscriptparser.Facade; import edu.kit.formal.proofscriptparser.ast.ProofScript; import javafx.beans.property.SimpleBooleanProperty; diff --git a/src/main/java/edu/kit/formal/interpreter/InterpretingService.java b/src/main/java/edu/kit/formal/interpreter/InterpretingService.java index 2cd4f245..41da703d 100644 --- a/src/main/java/edu/kit/formal/interpreter/InterpretingService.java +++ b/src/main/java/edu/kit/formal/interpreter/InterpretingService.java @@ -14,7 +14,7 @@ import javafx.concurrent.Task; * * @author A. Weigl */ -class InterpretingService extends Service> { +public class InterpretingService extends Service> { /** * The interpreter (with teh appropriate KeY state) that is used to traverse and execute the script @@ -31,7 +31,7 @@ class InterpretingService extends Service> { */ private PuppetMaster blocker; - InterpretingService(PuppetMaster blocker) { + public InterpretingService(PuppetMaster blocker) { this.blocker = blocker; } diff --git a/src/main/java/edu/kit/formal/interpreter/NodeAddedEvent.java b/src/main/java/edu/kit/formal/interpreter/NodeAddedEvent.java index b1e04746..a3bdc464 100644 --- a/src/main/java/edu/kit/formal/interpreter/NodeAddedEvent.java +++ b/src/main/java/edu/kit/formal/interpreter/NodeAddedEvent.java @@ -1,5 +1,6 @@ package edu.kit.formal.interpreter; +import edu.kit.formal.interpreter.graphs.PTreeNode; import lombok.Getter; /** diff --git a/src/main/java/edu/kit/formal/interpreter/exceptions/StateGraphException.java b/src/main/java/edu/kit/formal/interpreter/exceptions/StateGraphException.java new file mode 100644 index 00000000..47daed56 --- /dev/null +++ b/src/main/java/edu/kit/formal/interpreter/exceptions/StateGraphException.java @@ -0,0 +1,26 @@ +package edu.kit.formal.interpreter.exceptions; + +/** + * Exception that is thrown if State graph could not be build properly + */ +public class StateGraphException extends RuntimeException { + public StateGraphException() { + super(); + } + + public StateGraphException(String message) { + super(message); + } + + public StateGraphException(String message, Throwable cause) { + super(message, cause); + } + + public StateGraphException(Throwable cause) { + super(cause); + } + + protected StateGraphException(String message, Throwable cause, boolean enableSuppression, boolean writableStackTrace) { + super(message, cause, enableSuppression, writableStackTrace); + } +} diff --git a/src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java b/src/main/java/edu/kit/formal/interpreter/graphs/ControlFlowNode.java similarity index 88% rename from src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java rename to src/main/java/edu/kit/formal/interpreter/graphs/ControlFlowNode.java index 529e4f6f..7692e153 100644 --- a/src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java +++ b/src/main/java/edu/kit/formal/interpreter/graphs/ControlFlowNode.java @@ -1,4 +1,4 @@ -package edu.kit.formal.interpreter; +package edu.kit.formal.interpreter.graphs; import edu.kit.formal.proofscriptparser.ast.ASTNode; @@ -6,7 +6,7 @@ import java.util.LinkedList; import java.util.List; /** - * ControlFlowNode for ControlFlowGraph to look up step-edges for teh debugger. + * ControlFlowNode for ControlFlowGraph to look up step-edges for the debugger. */ public class ControlFlowNode { @@ -47,7 +47,7 @@ public class ControlFlowNode { StringBuilder sb = new StringBuilder(); sb.append("Node {"); if (scriptstmt != null) { - sb.append(scriptstmt.getNodeName().toString() + "@" + scriptstmt.getStartPosition()); + sb.append(scriptstmt.getNodeName()).append("@").append(scriptstmt.getStartPosition()); } else { sb.append("No Stmt"); } diff --git a/src/main/java/edu/kit/formal/interpreter/EdgeTypes.java b/src/main/java/edu/kit/formal/interpreter/graphs/EdgeTypes.java similarity index 52% rename from src/main/java/edu/kit/formal/interpreter/EdgeTypes.java rename to src/main/java/edu/kit/formal/interpreter/graphs/EdgeTypes.java index af433117..14f657ba 100644 --- a/src/main/java/edu/kit/formal/interpreter/EdgeTypes.java +++ b/src/main/java/edu/kit/formal/interpreter/graphs/EdgeTypes.java @@ -1,7 +1,7 @@ -package edu.kit.formal.interpreter; +package edu.kit.formal.interpreter.graphs; /** - * Created by sarah on 6/20/17. + * Edge Types a state graph and control flow graph may have */ public enum EdgeTypes { STEP_INTO, STEP_OVER, STEP_BACK, STEP_RETURN, STEP_OVER_COND, STATE_FLOW; diff --git a/src/main/java/edu/kit/formal/interpreter/GraphChangedListener.java b/src/main/java/edu/kit/formal/interpreter/graphs/GraphChangedListener.java similarity index 63% rename from src/main/java/edu/kit/formal/interpreter/GraphChangedListener.java rename to src/main/java/edu/kit/formal/interpreter/graphs/GraphChangedListener.java index 602a1630..2eb2cfea 100644 --- a/src/main/java/edu/kit/formal/interpreter/GraphChangedListener.java +++ b/src/main/java/edu/kit/formal/interpreter/graphs/GraphChangedListener.java @@ -1,4 +1,6 @@ -package edu.kit.formal.interpreter; +package edu.kit.formal.interpreter.graphs; + +import edu.kit.formal.interpreter.NodeAddedEvent; /** * Listener for Change events in the state graph diff --git a/src/main/java/edu/kit/formal/interpreter/PTreeNode.java b/src/main/java/edu/kit/formal/interpreter/graphs/PTreeNode.java similarity index 94% rename from src/main/java/edu/kit/formal/interpreter/PTreeNode.java rename to src/main/java/edu/kit/formal/interpreter/graphs/PTreeNode.java index b3c4919a..ac6e5777 100644 --- a/src/main/java/edu/kit/formal/interpreter/PTreeNode.java +++ b/src/main/java/edu/kit/formal/interpreter/graphs/PTreeNode.java @@ -1,4 +1,4 @@ -package edu.kit.formal.interpreter; +package edu.kit.formal.interpreter.graphs; import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.State; @@ -7,7 +7,7 @@ import edu.kit.formal.proofscriptparser.ast.ASTNode; import java.util.LinkedList; /** - * Inner class representing nodes in the graph + * 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. */ public class PTreeNode { diff --git a/src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java b/src/main/java/edu/kit/formal/interpreter/graphs/ProgramFlowVisitor.java similarity index 99% rename from src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java rename to src/main/java/edu/kit/formal/interpreter/graphs/ProgramFlowVisitor.java index 1015ae81..12d4cac8 100644 --- a/src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java +++ b/src/main/java/edu/kit/formal/interpreter/graphs/ProgramFlowVisitor.java @@ -1,4 +1,4 @@ -package edu.kit.formal.interpreter; +package edu.kit.formal.interpreter.graphs; import com.google.common.graph.EndpointPair; import com.google.common.graph.MutableValueGraph; diff --git a/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java b/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java similarity index 97% rename from src/main/java/edu/kit/formal/interpreter/ProofTreeController.java rename to src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java index 59f1f02b..47b7039f 100644 --- a/src/main/java/edu/kit/formal/interpreter/ProofTreeController.java +++ b/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java @@ -1,6 +1,8 @@ -package edu.kit.formal.interpreter; +package edu.kit.formal.interpreter.graphs; import edu.kit.formal.gui.controller.PuppetMaster; +import edu.kit.formal.interpreter.Interpreter; +import edu.kit.formal.interpreter.InterpretingService; import edu.kit.formal.interpreter.data.GoalNode; import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.State; @@ -162,8 +164,7 @@ public class ProofTreeController { */ public PTreeNode stepBack() { PTreeNode current = statePointer; - PTreeNode backState = stateGraphVisitor.getStepBack(current); - this.statePointer = backState; + this.statePointer = stateGraphVisitor.getStepBack(current); setNewState(statePointer.getState()); return statePointer; diff --git a/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java b/src/main/java/edu/kit/formal/interpreter/graphs/StateGraphVisitor.java similarity index 92% rename from src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java rename to src/main/java/edu/kit/formal/interpreter/graphs/StateGraphVisitor.java index 76be23f2..5b079151 100644 --- a/src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java +++ b/src/main/java/edu/kit/formal/interpreter/graphs/StateGraphVisitor.java @@ -1,10 +1,13 @@ -package edu.kit.formal.interpreter; +package edu.kit.formal.interpreter.graphs; import com.google.common.graph.MutableValueGraph; import com.google.common.graph.ValueGraphBuilder; +import edu.kit.formal.interpreter.Interpreter; +import edu.kit.formal.interpreter.NodeAddedEvent; import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.State; +import edu.kit.formal.interpreter.exceptions.StateGraphException; import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.ast.*; import javafx.application.Platform; @@ -19,7 +22,7 @@ import java.util.Set; /** * State graph that is computed on the fly while stepping through script - * A Node in the graph is a PTreeNode {@link edu.kit.formal.interpreter.PTreeNode} + * A Node in the graph is a PTreeNode {@link PTreeNode} * Edges are computed on the fly while */ public class StateGraphVisitor extends DefaultASTVisitor { @@ -85,10 +88,13 @@ public class StateGraphVisitor extends DefaultASTVisitor { public void createRootNode(ASTNode node) { PTreeNode newStateNode = new PTreeNode(node); newStateNode.setState(currentInterpreter.getCurrentState().copy()); - stateGraph.addNode(newStateNode); - this.root.set(newStateNode); - lastNode = newStateNode; - + 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); + lastNode = newStateNode; + } } public void setUpGraph() { @@ -161,8 +167,7 @@ public class StateGraphVisitor extends DefaultASTVisitor { */ public Void createNewNode(ASTNode node) { State lastState = lastNode.getState(); - //maybe delete - //lastNode.setState(currentInterpreter.getCurrentState()); + PTreeNode newStateNode; newStateNode = new PTreeNode(node); @@ -273,7 +278,7 @@ public class StateGraphVisitor extends DefaultASTVisitor { } - protected void fireNodeAdded(NodeAddedEvent nodeAddedEvent) { + private void fireNodeAdded(NodeAddedEvent nodeAddedEvent) { changeListeners.forEach(list -> { Platform.runLater(() -> { list.graphChanged(nodeAddedEvent); diff --git a/src/test/java/edu/kit/formal/interpreter/ProgramFlowVisitorTest.java b/src/test/java/edu/kit/formal/interpreter/ProgramFlowVisitorTest.java index edb13a23..ff9c3d54 100644 --- a/src/test/java/edu/kit/formal/interpreter/ProgramFlowVisitorTest.java +++ b/src/test/java/edu/kit/formal/interpreter/ProgramFlowVisitorTest.java @@ -1,6 +1,7 @@ package edu.kit.formal.interpreter; import edu.kit.formal.interpreter.funchdl.DefaultLookup; +import edu.kit.formal.interpreter.graphs.ProgramFlowVisitor; import edu.kit.formal.proofscriptparser.Facade; import edu.kit.formal.proofscriptparser.ScriptLanguageParser; import edu.kit.formal.proofscriptparser.TransformAst; -- GitLab