Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
sarah.grebing
ProofScriptParser
Commits
f9302e14
Commit
f9302e14
authored
Jun 30, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
listener for graphchanges
parent
f167cf52
Changes
7
Hide whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
139 additions
and
53 deletions
+139
-53
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
...t/formal/gui/controller/DebuggerMainWindowController.java
+1
-1
src/main/java/edu/kit/formal/gui/controls/InspectionViewTabPane.java
...va/edu/kit/formal/gui/controls/InspectionViewTabPane.java
+1
-0
src/main/java/edu/kit/formal/interpreter/GraphChangedListener.java
...java/edu/kit/formal/interpreter/GraphChangedListener.java
+11
-0
src/main/java/edu/kit/formal/interpreter/NodeAddedEvent.java
src/main/java/edu/kit/formal/interpreter/NodeAddedEvent.java
+26
-0
src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java
...n/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java
+5
-5
src/main/java/edu/kit/formal/interpreter/ProofTreeController.java
.../java/edu/kit/formal/interpreter/ProofTreeController.java
+53
-23
src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java
...in/java/edu/kit/formal/interpreter/StateGraphVisitor.java
+42
-24
No files found.
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
View file @
f9302e14
...
...
@@ -189,7 +189,7 @@ public class DebuggerMainWindowController implements Initializable {
@FXML
public
void
executeScriptFromCursor
()
{
//
InterpreterBuilder ib = facade.buildInterpreter();
InterpreterBuilder
ib
=
facade
.
buildInterpreter
();
// ib.inheritState(interpreterService.interpreterProperty().get());
///*
// LineMapping lm = new LineMapping(scriptArea.getText());
...
...
src/main/java/edu/kit/formal/gui/controls/InspectionViewTabPane.java
View file @
f9302e14
...
...
@@ -52,6 +52,7 @@ public class InspectionViewTabPane extends TabPane {
this
.
getTabs
().
add
(
tab
);
}
//TODO schauen wie Goallist ins model kommt
public
void
bindGoalNodesWithCurrentTab
(
RootModel
model
)
{
getActiveInspectionViewTab
().
getGoalView
().
itemsProperty
().
bind
(
model
.
currentGoalNodesProperty
());
model
.
currentSelectedGoalNodeProperty
().
addListener
((
p
,
old
,
fresh
)
->
{
...
...
src/main/java/edu/kit/formal/interpreter/GraphChangedListener.java
0 → 100644
View file @
f9302e14
package
edu.kit.formal.interpreter
;
/**
* Listener for Change events in the state graph
*/
public
interface
GraphChangedListener
{
abstract
void
graphChanged
(
NodeAddedEvent
nodeAddedEvent
);
}
src/main/java/edu/kit/formal/interpreter/NodeAddedEvent.java
0 → 100644
View file @
f9302e14
package
edu.kit.formal.interpreter
;
import
lombok.Getter
;
/**
* Event that is fired when a node is added to the StateGraph
*/
public
class
NodeAddedEvent
{
@Getter
PTreeNode
addedNode
;
@Getter
PTreeNode
lastPointer
;
public
NodeAddedEvent
(
PTreeNode
lastPointer
,
PTreeNode
addedNode
)
{
this
.
addedNode
=
addedNode
;
this
.
lastPointer
=
lastPointer
;
}
public
String
toString
()
{
return
addedNode
.
getScriptstmt
().
getNodeName
()
+
addedNode
.
getScriptstmt
().
getStartPosition
();
}
}
src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java
View file @
f9302e14
...
...
@@ -89,14 +89,14 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public
Void
visit
(
Statements
statements
)
{
ControlFlowNode
curLastNode
=
lastNode
;
//
ControlFlowNode curLastNode = lastNode;
for
(
Statement
stmnt
:
statements
)
{
stmnt
.
accept
(
this
);
graph
.
putEdgeValue
(
curLastNode
,
lastNode
,
EdgeTypes
.
STEP_OVER
);
graph
.
putEdgeValue
(
lastNode
,
curLastNode
,
EdgeTypes
.
STEP_BACK
);
curLastNode
=
lastNode
;
//
graph.putEdgeValue(curLastNode, lastNode, EdgeTypes.STEP_OVER);
//
graph.putEdgeValue(lastNode, curLastNode, EdgeTypes.STEP_BACK);
//
curLastNode = lastNode;
}
lastNode
=
curLastNode
;
//
lastNode = curLastNode;
return
null
;
}
...
...
src/main/java/edu/kit/formal/interpreter/ProofTreeController.java
View file @
f9302e14
...
...
@@ -5,8 +5,11 @@ import edu.kit.formal.interpreter.data.GoalNode;
import
edu.kit.formal.interpreter.data.KeyData
;
import
edu.kit.formal.proofscriptparser.Visitor
;
import
edu.kit.formal.proofscriptparser.ast.ProofScript
;
import
javafx.beans.property.ListProperty
;
import
javafx.beans.property.ReadOnlyBooleanProperty
;
import
javafx.beans.property.SimpleListProperty
;
import
javafx.beans.property.SimpleObjectProperty
;
import
javafx.collections.FXCollections
;
import
java.util.List
;
...
...
@@ -21,11 +24,17 @@ public class ProofTreeController {
* To control stepping
*/
private
final
PuppetMaster
blocker
=
new
PuppetMaster
();
private
final
SimpleObjectProperty
<
List
<
GoalNode
<
KeyData
>>>
currentGoals
=
blocker
.
currentGoalsProperty
();
private
final
SimpleObjectProperty
<
GoalNode
<
KeyData
>>
currentSelectedGoal
=
blocker
.
currentSelectedGoalProperty
();
private
final
SimpleObjectProperty
<
List
<
GoalNode
<
KeyData
>>>
currentGoals
=
new
SimpleObjectProperty
<>();
//= blocker.currentGoalsProperty();
private
final
ListProperty
<
GoalNode
<
KeyData
>>
currentGoalList
=
new
SimpleListProperty
<>(
FXCollections
.
observableArrayList
());
private
final
SimpleObjectProperty
<
GoalNode
<
KeyData
>>
currentSelectedGoal
=
new
SimpleObjectProperty
<>();
//= blocker.currentSelectedGoalProperty();
//new SimpleBooleanProperty(false);
private
InterpretingService
interpreterService
=
new
InterpretingService
(
blocker
);
private
ReadOnlyBooleanProperty
executeNotPossible
=
interpreterService
.
runningProperty
();
private
SimpleObjectProperty
<
PTreeNode
>
nextComputedNode
=
new
SimpleObjectProperty
<>();
/**
* Visitor to retrieve state graph
*/
...
...
@@ -50,23 +59,25 @@ public class ProofTreeController {
private
ProofScript
mainScript
;
public
ProofTreeController
()
{
/**
* Add a change listener for the stategraph
*/
private
GraphChangedListener
graphChangedListener
=
nodeAddedEvent
->
{
if
(
statePointer
.
equals
(
nodeAddedEvent
.
getLastPointer
()))
{
nextComputedNode
.
setValue
(
nodeAddedEvent
.
getAddedNode
());
}
}
private
ProofTreeController
(
Interpreter
<
KeyData
>
inter
,
ProofScript
mainScript
)
{
blocker
.
deinstall
();
};
this
.
currentInterpreter
=
inter
;
buildControlFlowGraph
(
mainScript
);
this
.
stateGraphVisitor
=
new
StateGraphVisitor
(
inter
,
mainScript
,
controlFlowGraphVisitor
);
//statePointer = stateGraphVisitor.getRoot();
public
ProofTreeController
()
{
this
.
currentGoals
.
bindBidirectional
(
blocker
.
currentGoalsProperty
());
this
.
currentSelectedGoal
.
bindBidirectional
(
blocker
.
currentSelectedGoalProperty
());
blocker
.
getStepUntilBlock
().
set
(
1
);
blocker
.
install
(
currentInterpreter
);
}
/**
* Build the control flow graph for looking up step-edges for the given script inligning called script commands
*
...
...
@@ -79,28 +90,37 @@ public class ProofTreeController {
}
//TODO handle endpoint
//handle inconsistency
public
PTreeNode
stepOver
()
{
PTreeNode
currentPointer
=
statePointer
;
if
(
statePointer
==
null
)
{
if
(
currentPointer
==
null
)
{
System
.
out
.
println
(
"StatePointer is null"
);
}
else
{
if
(
this
.
statePointer
.
getState
()
!=
null
&&
this
.
statePointer
.
getScriptstmt
()
!=
null
)
{
System
.
out
.
println
(
"StatePointer is "
+
currentPointer
.
getScriptstmt
().
getNodeName
()
+
currentPointer
.
getScriptstmt
().
getStartPosition
());
}
else
{
System
.
out
.
println
(
"Possibly root node"
);
}
PTreeNode
nextNode
=
stateGraphVisitor
.
getStepOver
(
currentPointer
);
if
(
nextNode
!=
null
)
{
this
.
statePointer
=
nextNode
;
}
else
{
nextComputedNode
.
addListener
((
observable
,
oldValue
,
newValue
)
->
{
this
.
statePointer
=
newValue
;
System
.
out
.
println
(
"Added new Value to Statepointer: "
+
this
.
statePointer
.
getScriptstmt
().
getNodeName
()
+
this
.
statePointer
.
getScriptstmt
().
getStartPosition
());
});
//let interpreter run for one step
blocker
.
getStepUntilBlock
().
addAndGet
(
1
);
blocker
.
unlock
();
//sync problem???
//TODO make this right!
//TODO handle endpoint of graph
nextNode
=
stateGraphVisitor
.
getStepOver
(
currentPointer
);
while
(
nextNode
==
null
)
{
nextNode
=
stateGraphVisitor
.
getStepOver
(
currentPointer
);
}
this
.
statePointer
=
nextNode
;
//stateGraphListener
//this.statePointer = nextNode;
}
System
.
out
.
println
(
"NEXT NODE \n\n"
+
this
.
statePointer
+
"\n-------------------\n"
);
}
...
...
@@ -111,7 +131,14 @@ public class ProofTreeController {
public
PTreeNode
stepBack
()
{
PTreeNode
current
=
statePointer
;
this
.
statePointer
=
stateGraphVisitor
.
getStepBack
(
current
);
System
.
out
.
println
(
"PRED NODE \n\n"
+
this
.
statePointer
+
"\n-------------------\n"
);
if
(
this
.
statePointer
==
null
)
{
}
else
{
this
.
currentGoals
.
set
(
this
.
statePointer
.
getState
().
getGoals
());
this
.
currentSelectedGoal
.
set
(
this
.
statePointer
.
getState
().
getSelectedGoalNode
());
}
System
.
out
.
println
(
"PRED NODE \n\n"
+
this
.
statePointer
.
getState
().
getSelectedGoalNode
().
getData
().
getNode
().
serialNr
()
+
":"
+
this
.
statePointer
.
getScriptstmt
().
getNodeName
()
+
"@"
+
this
.
statePointer
.
getScriptstmt
().
getStartPosition
()
+
"\n-------------------\n"
);
return
null
;
}
...
...
@@ -137,6 +164,7 @@ public class ProofTreeController {
// this.stateGraphVisitor = new StateGraphVisitor(blocker, this.mainScript, this.controlFlowGraphVisitor);
currentInterpreter
.
getEntryListeners
().
add
(
this
.
stateGraphVisitor
);
this
.
stateGraphVisitor
.
addChangeListener
(
graphChangedListener
);
//
// stateGraphVisitor.rootProperty().addListener((observable, oldValue, newValue) -> {
// this.statePointer = newValue;
...
...
@@ -167,6 +195,7 @@ public class ProofTreeController {
this
.
mainScript
=
mainScript
;
}
public
Visitor
getStateVisitor
()
{
return
this
.
stateGraphVisitor
;
}
...
...
@@ -203,4 +232,5 @@ public class ProofTreeController {
return
executeNotPossible
;
}
}
src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java
View file @
f9302e14
...
...
@@ -4,22 +4,35 @@ package edu.kit.formal.interpreter;
import
com.google.common.graph.MutableValueGraph
;
import
com.google.common.graph.ValueGraphBuilder
;
import
edu.kit.formal.gui.controller.PuppetMaster
;
import
edu.kit.formal.interpreter.data.KeyData
;
import
edu.kit.formal.proofscriptparser.DefaultASTVisitor
;
import
edu.kit.formal.proofscriptparser.ast.*
;
import
javafx.beans.property.SimpleObjectProperty
;
import
lombok.Getter
;
import
java.util.ArrayList
;
import
java.util.HashSet
;
import
java.util.List
;
import
java.util.Set
;
/**
* Created by sarah on 6/26/17.
* 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}
* Edges are computed on the fly while
*/
public
class
StateGraphVisitor
extends
DefaultASTVisitor
<
Void
>
{
/**
* Listeners getting informed when new node added to state graph
*/
@Getter
private
List
<
GraphChangedListener
>
changeListeners
=
new
ArrayList
();
/**
* Interpreter
*/
private
Interpreter
currentInterpreter
;
private
Interpreter
<
KeyData
>
currentInterpreter
;
private
PuppetMaster
blocker
;
/**
...
...
@@ -48,27 +61,23 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
*/
private
PTreeNode
currentStatePointer
;
private
ProofScript
mainScript
;
public
StateGraphVisitor
(
Interpreter
inter
,
ProofScript
mainScript
,
ProgramFlowVisitor
cfgVisitor
)
{
stateGraph
=
ValueGraphBuilder
.
directed
().
build
();
this
.
currentInterpreter
=
inter
;
this
.
cfgVisitor
=
cfgVisitor
;
this
.
mainScript
=
mainScript
;
createRootNode
();
}
/* public StateGraphVisitor(PuppetMaster blocker, ProofScript mainScript, ProgramFlowVisitor cfgVisitor) {
stateGraph = ValueGraphBuilder.directed().build();
this.cfgVisitor = cfgVisitor;
this.blocker = blocker;
createRootNode();
}*/
public
MutableValueGraph
<
PTreeNode
,
EdgeTypes
>
getStateGraph
()
{
return
stateGraph
;
}
public
PTreeNode
getLastNode
()
{
return
lastNode
;
}
...
...
@@ -86,7 +95,6 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
//careful TODO look for right edges
//TODO handle endpoint of graph
public
PTreeNode
getStepOver
(
PTreeNode
statePointer
)
{
Set
<
PTreeNode
>
successors
=
this
.
stateGraph
.
successors
(
statePointer
);
if
(
successors
.
isEmpty
())
{
return
null
;
...
...
@@ -99,7 +107,7 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
}
//TODO handle endpoint of graph
public
PTreeNode
getStepBack
(
PTreeNode
statePointer
)
{
Set
<
PTreeNode
>
pred
=
this
.
stateGraph
.
predecessors
(
statePointer
);
...
...
@@ -130,10 +138,11 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
chosenNodes
.
add
(
succ
);
}
});
chosenNodes
.
forEach
(
n
->
System
.
out
.
println
(
n
.
toString
()));
//
chosenNodes.forEach(n -> System.out.println(n.toString()));
//stateGraph.edgeValue()
return
null
;
}
/**
* Create a new node for the state graph and add edges to already existing nodes
*
...
...
@@ -141,21 +150,16 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
* @return
*/
public
Void
createNewNode
(
ASTNode
node
)
{
PTreeNode
newStateNode
;
newStateNode
=
new
PTreeNode
(
node
);
PTreeNode
newStateNode
=
new
PTreeNode
(
node
);
newStateNode
.
setState
(
currentInterpreter
.
getCurrentState
());
stateGraph
.
addNode
(
newStateNode
);
/*Set<EndpointPair<ControlFlowNode>> targetEdges = cfgVisitor.getAllEdgesForNodeAsTarget(node);
for (EndpointPair<ControlFlowNode> targetEdge : targetEdges) {
ControlFlowNode cfn = targetEdge.source();
ASTNode assocNode = cfn.getScriptstmt();
//mapping
}*/
stateGraph
.
putEdgeValue
(
lastNode
,
newStateNode
,
EdgeTypes
.
STATE_FLOW
);
fireNodeAdded
(
new
NodeAddedEvent
(
lastNode
,
newStateNode
));
lastNode
=
newStateNode
;
return
null
;
}
...
...
@@ -171,10 +175,6 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
return
createNewNode
(
assignment
);
}
@Override
public
Void
visit
(
Statements
statements
)
{
return
createNewNode
(
statements
);
}
@Override
public
Void
visit
(
CasesStatement
casesStatement
)
{
...
...
@@ -245,4 +245,22 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
return
root
;
}
public
void
addChangeListener
(
GraphChangedListener
listener
)
{
changeListeners
.
add
(
listener
);
}
public
void
removeChangeListener
(
GraphChangedListener
listener
)
{
changeListeners
.
remove
(
listener
);
}
protected
void
fireNodeAdded
(
NodeAddedEvent
nodeAddedEvent
)
{
System
.
out
.
println
(
"New Node added "
+
nodeAddedEvent
.
toString
());
changeListeners
.
forEach
(
list
->
{
list
.
graphChanged
(
nodeAddedEvent
);
});
}
}
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