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
dabdebca
Commit
dabdebca
authored
Oct 27, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
fixed errors
parent
4197f43b
Pipeline
#14970
failed with stage
in 1 minute and 59 seconds
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
27 additions
and
23 deletions
+27
-23
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
...du/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
+4
-2
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
...ti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
+15
-13
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
.../iti/formal/psdbg/gui/controller/ProofTreeController.java
+7
-7
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
...va/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
+1
-1
No files found.
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
View file @
dabdebca
package
edu.kit.iti.formal.psdbg.interpreter.graphs
;
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
lombok.Data
;
import
lombok.Getter
;
...
...
@@ -19,12 +18,15 @@ public class PTreeNode<T> {
* State after statement
*/
//private State<T> state;
@Getter
@Setter
private
InterpreterExtendedState
<
T
>
extendedState
=
new
InterpreterExtendedState
<>(
null
);
/**
* Statement
*/
@Getter
@Setter
private
ASTNode
scriptStmt
;
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
View file @
dabdebca
...
...
@@ -119,7 +119,7 @@ public class StateGraphWrapper<T> {
LOGGER
.
info
(
"Stepover requested for null, therefore returning root"
);
return
this
.
rootProperty
().
get
();
}
LOGGER
.
info
(
"Stepover requested for node {}@{}"
,
statePointer
.
getScript
s
tmt
(),
statePointer
.
getScript
s
tmt
().
getNodeName
());
LOGGER
.
info
(
"Stepover requested for node {}@{}"
,
statePointer
.
getScript
S
tmt
(),
statePointer
.
getScript
S
tmt
().
getNodeName
());
//look for successors in the graph
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
...
...
@@ -209,10 +209,10 @@ public class StateGraphWrapper<T> {
newStateNode
.
getContext
().
push
(
node
);
State
<
T
>
currentInterpreterStateCopy
=
currentInterpreter
.
getCurrentState
().
copy
();
//copy current state before executing statement
newStateNode
.
setState
(
currentInterpreterStateCopy
);
//
newStateNode.setState(currentInterpreterStateCopy);
//create extended State
InterpreterExtendedState
<
T
>
extState
=
new
InterpreterExtendedState
<>();
InterpreterExtendedState
<
T
>
extState
=
new
InterpreterExtendedState
<>(
null
);
extState
.
setStmt
(
node
);
extState
.
setStateBeforeStmt
(
currentInterpreterStateCopy
);
newStateNode
.
setExtendedState
(
extState
);
...
...
@@ -263,7 +263,7 @@ public class StateGraphWrapper<T> {
extState
.
setMappingOfCaseToStates
(
mappingOfCaseToStates
);
//TODO default case: missing datastructure of supertype CaseStatement at the moment
newStateNode
.
setState
(
lastState
.
copy
());
//
newStateNode.setState(lastState.copy());
}
else
{
...
...
@@ -282,17 +282,17 @@ public class StateGraphWrapper<T> {
newStateNode
.
setExtendedState
(
extState
);
stateGraph
.
addNode
(
newStateNode
);
Collection
<
Pair
<
ControlFlowNode
,
EdgeTypes
>>
predecessorsAndTheirEdges
=
cfgVisitor
.
getPredecessorsAndTheirEdges
(
newStateNode
.
getScript
s
tmt
());
Collection
<
Pair
<
ControlFlowNode
,
EdgeTypes
>>
predecessorsAndTheirEdges
=
cfgVisitor
.
getPredecessorsAndTheirEdges
(
newStateNode
.
getScript
S
tmt
());
for
(
Pair
<
ControlFlowNode
,
EdgeTypes
>
predecessorsAndTheirEdge
:
predecessorsAndTheirEdges
)
{
if
(
predecessorsAndTheirEdge
.
getKey
().
equals
(
lastNode
.
getScript
s
tmt
()))
{
if
(
predecessorsAndTheirEdge
.
getKey
().
equals
(
lastNode
.
getScript
S
tmt
()))
{
stateGraph
.
putEdgeValue
(
lastNode
,
newStateNode
,
predecessorsAndTheirEdge
.
getValue
());
}
}
Collection
<
Pair
<
ControlFlowNode
,
EdgeTypes
>>
predecessorsAsTarget
=
cfgVisitor
.
getPredecessorsAsTarget
(
node
);
for
(
Pair
<
ControlFlowNode
,
EdgeTypes
>
predecessorAsTarget
:
predecessorsAsTarget
)
{
if
(
predecessorAsTarget
.
getKey
().
equals
(
lastNode
.
getScript
s
tmt
()))
{
if
(
predecessorAsTarget
.
getKey
().
equals
(
lastNode
.
getScript
S
tmt
()))
{
stateGraph
.
putEdgeValue
(
newStateNode
,
lastNode
,
predecessorAsTarget
.
getValue
());
}
...
...
@@ -322,8 +322,8 @@ public class StateGraphWrapper<T> {
//copy Current Interpreter state
State
<
T
>
currentState
=
currentInterpreter
.
getCurrentState
().
copy
();
//set the state
if
(
node
!=
this
.
root
.
get
().
getScript
s
tmt
())
{
newStateNode
.
setState
(
currentState
);
if
(
node
!=
this
.
root
.
get
().
getScript
S
tmt
())
{
//
newStateNode.setState(currentState);
newStateNode
.
getExtendedState
().
setStateAfterStmt
(
currentState
);
if
(
newStateNode
.
getContext
().
peek
().
equals
(
node
))
{
newStateNode
.
getContext
().
pop
();
...
...
@@ -394,7 +394,9 @@ public class StateGraphWrapper<T> {
public
PTreeNode
<
T
>
getNode
(
List
<
GoalNode
<
T
>>
newValue
)
{
for
(
Map
.
Entry
<
ASTNode
,
PTreeNode
<
T
>>
next
:
addedNodes
.
entrySet
())
{
PTreeNode
value
=
next
.
getValue
();
if
(
value
.
getState
().
getGoals
().
equals
(
newValue
))
{
//if (value.getState().getGoals().equals(newValue)) {
if
(
value
.
getExtendedState
().
getStateBeforeStmt
().
getGoals
().
equals
(
newValue
))
{
return
value
;
}
}
...
...
@@ -422,9 +424,9 @@ public class StateGraphWrapper<T> {
stateGraph
.
nodes
().
forEach
(
n
->
{
sb
.
append
(
n
.
hashCode
())
.
append
(
" [label=\""
)
.
append
(
n
.
getScript
s
tmt
().
getNodeName
())
.
append
(
n
.
getScript
S
tmt
().
getNodeName
())
.
append
(
"@"
)
.
append
(
n
.
getScript
s
tmt
().
getStartPosition
().
getLineNumber
())
.
append
(
n
.
getScript
S
tmt
().
getStartPosition
().
getLineNumber
())
.
append
(
n
.
extendedStateToString
())
.
append
(
"\"]\n"
);
});
...
...
@@ -463,7 +465,7 @@ public class StateGraphWrapper<T> {
if
(
root
.
get
()
==
null
)
{
createRootNode
(
proofScript
);
}
else
{
if
(!
root
.
get
().
getScript
s
tmt
().
equals
(
proofScript
))
{
if
(!
root
.
get
().
getScript
S
tmt
().
equals
(
proofScript
))
{
createNewNode
(
proofScript
);
}
}
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
View file @
dabdebca
...
...
@@ -123,7 +123,7 @@ public class ProofTreeController {
@Override
public
void
graphChanged
(
NodeAddedEvent
nodeAddedEvent
)
{
PTreeNode
added
=
nodeAddedEvent
.
getAddedNode
();
if
(
added
.
getState
()
!=
null
)
{
if
(
added
.
get
Extended
State
()
!=
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()));
...
...
@@ -172,11 +172,11 @@ public class ProofTreeController {
nextComputedNode
.
addListener
((
observable
,
oldValue
,
newValue
)
->
{
//update statepointer
if
(
newValue
!=
null
)
{
LOGGER
.
info
(
"New node {} was computed and the statepointer was set to {}"
,
newValue
.
getScript
s
tmt
(),
newValue
);
LOGGER
.
info
(
"New node {} was computed and the statepointer was set to {}"
,
newValue
.
getScript
S
tmt
(),
newValue
);
this
.
statePointer
=
newValue
;
//setNewState(blocker.currentStateProperty().get());
setNewState
(
newValue
.
get
State
());
setNewState
(
newValue
.
get
ExtendedState
().
getStateAfterStmt
());
}
});
...
...
@@ -212,8 +212,8 @@ public class ProofTreeController {
LOGGER
.
debug
(
"New State from this command: {}@{}"
,
this
.
statePointer
.
getScript
s
tmt
().
getNodeName
(),
this
.
statePointer
.
getScript
s
tmt
().
getStartPosition
());
this
.
statePointer
.
getScript
S
tmt
().
getNodeName
(),
this
.
statePointer
.
getScript
S
tmt
().
getStartPosition
());
}
else
{
throw
new
RuntimeException
(
"The state pointer was null when setting new state"
);
}
...
...
@@ -254,7 +254,7 @@ public class ProofTreeController {
//if nextnode is null ask interpreter to execute next statement and compute next state
if
(
nextNode
!=
null
)
{
setCurrentHighlightNode
(
nextNode
.
getScript
s
tmt
());
setCurrentHighlightNode
(
nextNode
.
getScript
S
tmt
());
}
if
(
nextNode
!=
null
&&
nextNode
.
getExtendedState
().
getStateAfterStmt
()
!=
null
)
{
...
...
@@ -291,7 +291,7 @@ public class ProofTreeController {
this
.
statePointer
=
stateGraphWrapper
.
getStepBack
(
current
);
if
(
this
.
statePointer
!=
null
)
{
setNewState
(
statePointer
.
getExtendedState
().
getStateBeforeStmt
());
setCurrentHighlightNode
(
statePointer
.
getScript
s
tmt
());
setCurrentHighlightNode
(
statePointer
.
getScript
S
tmt
());
}
else
{
this
.
statePointer
=
current
;
}
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
View file @
dabdebca
...
...
@@ -119,7 +119,7 @@ public class SequentView extends CodeArea {
NamespaceSet
nss
=
services
.
getNamespaces
();
Sequent
sequent
=
node
.
get
().
sequent
();
filter
=
new
IdentitySequentPrintFilter
();
filter
=
new
IdentitySequentPrintFilter
(
sequent
);
ProgramPrinter
prgPrinter
=
new
ProgramPrinter
(
new
StringWriter
());
this
.
backend
=
new
LogicPrinter
.
PosTableStringBackend
(
80
);
...
...
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