Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
P
ProofScriptParser
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
24
Issues
24
List
Boards
Labels
Service Desk
Milestones
Merge Requests
4
Merge Requests
4
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
sarah.grebing
ProofScriptParser
Commits
d0906b07
Commit
d0906b07
authored
Jul 04, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
cleaning
parent
68463826
Changes
12
Hide whitespace changes
Inline
Side-by-side
Showing
12 changed files
with
64 additions
and
24 deletions
+64
-24
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
...t/formal/gui/controller/DebuggerMainWindowController.java
+5
-1
src/main/java/edu/kit/formal/interpreter/InterpretingService.java
.../java/edu/kit/formal/interpreter/InterpretingService.java
+2
-2
src/main/java/edu/kit/formal/interpreter/NodeAddedEvent.java
src/main/java/edu/kit/formal/interpreter/NodeAddedEvent.java
+1
-0
src/main/java/edu/kit/formal/interpreter/exceptions/StateGraphException.java
...it/formal/interpreter/exceptions/StateGraphException.java
+26
-0
src/main/java/edu/kit/formal/interpreter/graphs/ControlFlowNode.java
...va/edu/kit/formal/interpreter/graphs/ControlFlowNode.java
+3
-3
src/main/java/edu/kit/formal/interpreter/graphs/EdgeTypes.java
...ain/java/edu/kit/formal/interpreter/graphs/EdgeTypes.java
+2
-2
src/main/java/edu/kit/formal/interpreter/graphs/GraphChangedListener.java
...u/kit/formal/interpreter/graphs/GraphChangedListener.java
+3
-1
src/main/java/edu/kit/formal/interpreter/graphs/PTreeNode.java
...ain/java/edu/kit/formal/interpreter/graphs/PTreeNode.java
+2
-2
src/main/java/edu/kit/formal/interpreter/graphs/ProgramFlowVisitor.java
...edu/kit/formal/interpreter/graphs/ProgramFlowVisitor.java
+1
-1
src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java
...du/kit/formal/interpreter/graphs/ProofTreeController.java
+4
-3
src/main/java/edu/kit/formal/interpreter/graphs/StateGraphVisitor.java
.../edu/kit/formal/interpreter/graphs/StateGraphVisitor.java
+14
-9
src/test/java/edu/kit/formal/interpreter/ProgramFlowVisitorTest.java
...va/edu/kit/formal/interpreter/ProgramFlowVisitorTest.java
+1
-0
No files found.
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
View file @
d0906b07
...
...
@@ -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
;
...
...
src/main/java/edu/kit/formal/interpreter/InterpretingService.java
View file @
d0906b07
...
...
@@ -14,7 +14,7 @@ import javafx.concurrent.Task;
*
* @author A. Weigl
*/
class
InterpretingService
extends
Service
<
State
<
KeyData
>>
{
public
class
InterpretingService
extends
Service
<
State
<
KeyData
>>
{
/**
* The interpreter (with teh appropriate KeY state) that is used to traverse and execute the script
...
...
@@ -31,7 +31,7 @@ class InterpretingService extends Service<State<KeyData>> {
*/
private
PuppetMaster
blocker
;
InterpretingService
(
PuppetMaster
blocker
)
{
public
InterpretingService
(
PuppetMaster
blocker
)
{
this
.
blocker
=
blocker
;
}
...
...
src/main/java/edu/kit/formal/interpreter/NodeAddedEvent.java
View file @
d0906b07
package
edu.kit.formal.interpreter
;
import
edu.kit.formal.interpreter.graphs.PTreeNode
;
import
lombok.Getter
;
/**
...
...
src/main/java/edu/kit/formal/interpreter/exceptions/StateGraphException.java
0 → 100644
View file @
d0906b07
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
);
}
}
src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java
→
src/main/java/edu/kit/formal/interpreter/
graphs/
ControlFlowNode.java
View file @
d0906b07
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 t
eh
debugger.
* ControlFlowNode for ControlFlowGraph to look up step-edges for t
he
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"
);
}
...
...
src/main/java/edu/kit/formal/interpreter/EdgeTypes.java
→
src/main/java/edu/kit/formal/interpreter/
graphs/
EdgeTypes.java
View file @
d0906b07
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
;
...
...
src/main/java/edu/kit/formal/interpreter/GraphChangedListener.java
→
src/main/java/edu/kit/formal/interpreter/
graphs/
GraphChangedListener.java
View file @
d0906b07
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
...
...
src/main/java/edu/kit/formal/interpreter/PTreeNode.java
→
src/main/java/edu/kit/formal/interpreter/
graphs/
PTreeNode.java
View file @
d0906b07
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
{
...
...
src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java
→
src/main/java/edu/kit/formal/interpreter/
graphs/
ProgramFlowVisitor.java
View file @
d0906b07
package
edu.kit.formal.interpreter
;
package
edu.kit.formal.interpreter
.graphs
;
import
com.google.common.graph.EndpointPair
;
import
com.google.common.graph.MutableValueGraph
;
...
...
src/main/java/edu/kit/formal/interpreter/ProofTreeController.java
→
src/main/java/edu/kit/formal/interpreter/
graphs/
ProofTreeController.java
View file @
d0906b07
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
;
...
...
src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java
→
src/main/java/edu/kit/formal/interpreter/
graphs/
StateGraphVisitor.java
View file @
d0906b07
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
<
Void
>
{
...
...
@@ -85,10 +88,13 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
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<Void> {
*/
public
Void
createNewNode
(
ASTNode
node
)
{
State
<
KeyData
>
lastState
=
lastNode
.
getState
();
//maybe delete
//lastNode.setState(currentInterpreter.getCurrentState());
PTreeNode
newStateNode
;
newStateNode
=
new
PTreeNode
(
node
);
...
...
@@ -273,7 +278,7 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
}
pr
otected
void
fireNodeAdded
(
NodeAddedEvent
nodeAddedEvent
)
{
pr
ivate
void
fireNodeAdded
(
NodeAddedEvent
nodeAddedEvent
)
{
changeListeners
.
forEach
(
list
->
{
Platform
.
runLater
(()
->
{
list
.
graphChanged
(
nodeAddedEvent
);
...
...
src/test/java/edu/kit/formal/interpreter/ProgramFlowVisitorTest.java
View file @
d0906b07
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
;
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment