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
9dfb35b5
Commit
9dfb35b5
authored
Oct 27, 2017
by
Alexander Weigl
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
libraries repair
parent
534d76ca
Changes
14
Hide whitespace changes
Inline
Side-by-side
Showing
14 changed files
with
96 additions
and
136 deletions
+96
-136
DockFX/DockFX.iml
DockFX/DockFX.iml
+3
-1
keydeps/README.user
keydeps/README.user
+5
-0
keydeps/lib/components/key.core.jar
keydeps/lib/components/key.core.jar
+0
-0
keydeps/lib/components/key.ui.jar
keydeps/lib/components/key.ui.jar
+0
-0
keydeps/lib/components/key.util.jar
keydeps/lib/components/key.util.jar
+0
-0
keydeps/lib/libs/recoderKey.jar
keydeps/lib/libs/recoderKey.jar
+0
-0
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java
...ava/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java
+0
-2
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/NodeAddedEvent.java
.../edu/kit/iti/formal/psdbg/interpreter/NodeAddedEvent.java
+1
-1
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/StateAddedEvent.java
...edu/kit/iti/formal/psdbg/interpreter/StateAddedEvent.java
+1
-1
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/InterpreterExtendedState.java
...rmal/psdbg/interpreter/data/InterpreterExtendedState.java
+15
-32
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
...du/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
+12
-37
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
...ti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
+10
-16
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
.../iti/formal/psdbg/gui/controller/ProofTreeController.java
+44
-42
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
...va/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
+5
-4
No files found.
DockFX/DockFX.iml
View file @
9dfb35b5
<?xml version="1.0" encoding="UTF-8"?>
<module
org.jetbrains.idea.maven.project.MavenProjectsManager.isMavenModule=
"true"
type=
"JAVA_MODULE"
version=
"4"
>
<component
name=
"NewModuleRootManager"
LANGUAGE_LEVEL=
"JDK_1_8"
>
<component
name=
"NewModuleRootManager"
LANGUAGE_LEVEL=
"JDK_1_8"
inherit-compiler-output=
"false"
>
<output
url=
"file://$MODULE_DIR$/target/classes"
/>
<output-test
url=
"file://$MODULE_DIR$/target/test-classes"
/>
<content
url=
"file://$MODULE_DIR$"
>
...
...
@@ -10,6 +10,8 @@
</content>
<orderEntry
type=
"inheritedJdk"
/>
<orderEntry
type=
"sourceFolder"
forTests=
"false"
/>
<orderEntry
type=
"library"
name=
"Maven: org.apache.logging.log4j:log4j-api:2.6"
level=
"project"
/>
<orderEntry
type=
"library"
name=
"Maven: org.apache.logging.log4j:log4j-core:2.6"
level=
"project"
/>
<orderEntry
type=
"library"
scope=
"TEST"
name=
"Maven: junit:junit:4.12"
level=
"project"
/>
<orderEntry
type=
"library"
scope=
"TEST"
name=
"Maven: org.hamcrest:hamcrest-core:1.3"
level=
"project"
/>
<orderEntry
type=
"library"
scope=
"PROVIDED"
name=
"Maven: org.projectlombok:lombok:1.16.16"
level=
"project"
/>
...
...
keydeps/README.user
100644 → 100755
View file @
9dfb35b5
#!/bin/bash -x
# Execute this in this folder.
# Set to key/key/deployment/components/
COMPONENTS
=
${
COMPONENTS
:-
/home/sarah/Documents/KIT_Mitarbeiter/KeYDevelopment/KeYGitDir/key/key/deployment/components/
}
COMPONENTS
=
$HOME
/work/key/key/deployment/components/
mvn
install
:install-file
-Dfile
=
$COMPONENTS
/key.core.jar
\
...
...
keydeps/lib/components/key.core.jar
View file @
9dfb35b5
No preview for this file type
keydeps/lib/components/key.ui.jar
View file @
9dfb35b5
No preview for this file type
keydeps/lib/components/key.util.jar
View file @
9dfb35b5
No preview for this file type
keydeps/lib/recoderKey.jar
→
keydeps/lib/
libs/
recoderKey.jar
View file @
9dfb35b5
File moved
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java
View file @
9dfb35b5
...
...
@@ -770,7 +770,5 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
assert
!
exitListenerStack
.
empty
()
&&
!
entryListenerStack
.
empty
();
entryListenerStack
.
pop
();
exitListenerStack
.
pop
();
}
}
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/NodeAddedEvent.java
View file @
9dfb35b5
...
...
@@ -20,7 +20,7 @@ public class NodeAddedEvent {
}
public
String
toString
()
{
return
addedNode
.
getScript
s
tmt
().
getNodeName
()
+
addedNode
.
getScript
s
tmt
().
getStartPosition
();
return
addedNode
.
getScript
S
tmt
().
getNodeName
()
+
addedNode
.
getScript
S
tmt
().
getStartPosition
();
}
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/StateAddedEvent.java
View file @
9dfb35b5
...
...
@@ -26,7 +26,7 @@ public class StateAddedEvent {
}
public
String
toString
()
{
return
"State added to "
+
changedNode
.
getScript
s
tmt
().
getNodeName
()
+
changedNode
.
getScript
s
tmt
().
getStartPosition
();
return
"State added to "
+
changedNode
.
getScript
S
tmt
().
getNodeName
()
+
changedNode
.
getScript
S
tmt
().
getStartPosition
();
}
}
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/InterpreterExtendedState.java
View file @
9dfb35b5
...
...
@@ -3,9 +3,7 @@ package edu.kit.iti.formal.psdbg.interpreter.data;
import
edu.kit.iti.formal.psdbg.parser.ast.ASTNode
;
import
edu.kit.iti.formal.psdbg.parser.ast.CaseStatement
;
import
lombok.Data
;
import
lombok.Getter
;
import
lombok.RequiredArgsConstructor
;
import
lombok.Setter
;
import
java.util.Collections
;
import
java.util.HashMap
;
...
...
@@ -16,60 +14,45 @@ import java.util.Map;
@Data
public
class
InterpreterExtendedState
<
T
>
{
@Getter
@Setter
/**
* Null if root
*/
private
final
InterpreterExtendedState
<
T
>
predecessor
;
/**
* If we are in a case statement, this map defines which
*/
private
Map
<
CaseStatement
,
List
<
GoalNode
<
T
>>>
mappingOfCaseToStates
=
new
HashMap
<>();
/**
* State before the statement;
*/
@Getter
@Setter
private
State
<
T
>
stateBeforeStmt
;
/**
* State after execution of statement
*/
@Getter
@Setter
private
State
<
T
>
stateAfterStmt
;
/**
* Statement
*/
@Getter
@Setter
private
ASTNode
stmt
;
/**
* Null if root
*/
@Getter
@Setter
private
InterpreterExtendedState
<
T
>
predecessor
;
public
InterpreterExtendedState
(
InterpreterExtendedState
<
T
>
pred
)
{
this
.
predecessor
=
pred
;
}
public
InterpreterExtendedState
<
T
>
copy
()
{
InterpreterExtendedState
<
T
>
ext
=
new
InterpreterExtendedState
<>();
if
(
this
.
predecessor
!=
null
)
{
ext
.
setPredecessor
(
this
.
predecessor
.
copy
());
}
else
{
ext
.
predecessor
=
null
;
}
InterpreterExtendedState
<
T
>
ext
=
new
InterpreterExtendedState
<>(
this
.
predecessor
!=
null
?
this
.
predecessor
.
copy
()
:
null
);
ext
.
setStmt
(
stmt
);
if
(
stateAfterStmt
!=
null
)
{
ext
.
setStateAfterStmt
(
this
.
stateAfterStmt
.
copy
());
}
else
{
ext
.
setStateAfterStmt
(
null
);
}
if
(
stateBeforeStmt
!=
null
)
{
ext
.
setStateBeforeStmt
(
this
.
stateBeforeStmt
.
copy
());
}
else
{
ext
.
setStateBeforeStmt
(
null
);
}
return
ext
;
}
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
View file @
9dfb35b5
...
...
@@ -3,6 +3,9 @@ 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
;
import
lombok.Setter
;
import
java.util.Stack
;
...
...
@@ -10,57 +13,32 @@ import java.util.Stack;
* 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.
*/
@Data
public
class
PTreeNode
<
T
>
{
/**
* State after statement
*/
private
State
<
T
>
state
;
//
private State<T> state;
private
InterpreterExtendedState
<
T
>
extendedState
=
new
InterpreterExtendedState
<>();
private
InterpreterExtendedState
<
T
>
extendedState
=
new
InterpreterExtendedState
<>(
null
);
/**
* Statement
*/
private
ASTNode
script
s
tmt
;
private
ASTNode
script
S
tmt
;
/**
* Call context
*/
@Getter
@Setter
private
Stack
<
ASTNode
>
context
=
new
Stack
<>();
public
Stack
<
ASTNode
>
getContext
()
{
return
context
;
}
public
void
setContext
(
Stack
<
ASTNode
>
context
)
{
this
.
context
=
context
;
}
private
boolean
root
;
PTreeNode
(
ASTNode
node
)
{
this
.
setScriptstmt
(
node
);
}
public
State
<
T
>
getState
()
{
return
state
;
}
public
void
setState
(
State
<
T
>
state
)
{
this
.
state
=
state
;
}
public
ASTNode
getScriptstmt
()
{
return
scriptstmt
;
}
private
void
setScriptstmt
(
ASTNode
scriptstmt
)
{
this
.
scriptstmt
=
scriptstmt
;
}
public
InterpreterExtendedState
<
T
>
getExtendedState
()
{
return
extendedState
;
this
.
setScriptStmt
(
node
);
}
public
void
setExtendedState
(
InterpreterExtendedState
<
T
>
extendedState
)
{
...
...
@@ -70,8 +48,8 @@ public class PTreeNode<T> {
public
String
toString
()
{
StringBuilder
sb
=
new
StringBuilder
();
sb
.
append
(
"Node {"
);
if
(
script
s
tmt
!=
null
)
{
sb
.
append
(
script
s
tmt
.
getNodeName
()
+
"\n"
);
if
(
script
S
tmt
!=
null
)
{
sb
.
append
(
script
S
tmt
.
getNodeName
()
+
"\n"
);
}
else
{
sb
.
append
(
"Root Node"
);
}
...
...
@@ -89,9 +67,6 @@ public class PTreeNode<T> {
return
sb
.
toString
();
}
public
boolean
hasState
()
{
return
state
!=
null
;
}
public
String
extendedStateToString
()
{
return
this
.
extendedState
.
toString
();
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
View file @
9dfb35b5
...
...
@@ -94,8 +94,6 @@ public class StateGraphWrapper<T> {
}
private
static
int
counter
=
0
;
public
MutableValueGraph
<
PTreeNode
<
T
>,
EdgeTypes
>
getStateGraph
()
{
return
stateGraph
;
}
...
...
@@ -118,7 +116,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
...
...
@@ -195,10 +193,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
);
...
...
@@ -236,7 +234,7 @@ public class StateGraphWrapper<T> {
if
(
isCasesStmt
)
{
newStateNode
.
getContext
().
push
(
node
);
extState
=
new
InterpreterExtendedState
<>(
lastNode
.
getExtendedState
()
.
copy
()
);
extState
=
new
InterpreterExtendedState
<>(
lastNode
.
getExtendedState
());
extState
.
setStmt
(
node
);
extState
.
setStateBeforeStmt
(
lastState
.
copy
());
Map
<
CaseStatement
,
List
<
GoalNode
<
T
>>>
mappingOfCaseToStates
=
extState
.
getMappingOfCaseToStates
();
...
...
@@ -247,11 +245,7 @@ public class StateGraphWrapper<T> {
});
extState
.
setMappingOfCaseToStates
(
mappingOfCaseToStates
);
//TODO default case
newStateNode
.
setState
(
lastState
.
copy
());
}
else
{
//set pointer to parent extended state
extState
=
new
InterpreterExtendedState
<>(
lastNode
.
getExtendedState
().
copy
());
extState
.
setStmt
(
node
);
...
...
@@ -321,7 +315,7 @@ 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
.
get
State
().
getGoals
().
equals
(
newValue
))
{
if
(
value
.
get
ExtendedState
().
getStateBeforeStmt
().
getGoals
().
equals
(
newValue
))
{
return
value
;
}
}
...
...
@@ -339,9 +333,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"
);
});
...
...
@@ -379,8 +373,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
();
...
...
@@ -412,7 +406,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 @
9dfb35b5
...
...
@@ -2,6 +2,7 @@ package edu.kit.iti.formal.psdbg.gui.controller;
import
com.google.common.eventbus.Subscribe
;
import
com.google.common.graph.MutableValueGraph
;
import
de.uka.ilkd.key.proof.Goal
;
import
edu.kit.iti.formal.psdbg.InterpretingService
;
import
edu.kit.iti.formal.psdbg.gui.controls.ASTNodeHiglightListener
;
import
edu.kit.iti.formal.psdbg.gui.controls.DebuggerStatusBar
;
...
...
@@ -26,6 +27,7 @@ import org.apache.logging.log4j.Logger;
import
java.util.Collections
;
import
java.util.List
;
import
java.util.Set
;
import
java.util.stream.Collectors
;
/**
* Class controlling and maintaining proof tree structure for debugger and handling step functions for the debugger
...
...
@@ -39,8 +41,10 @@ public class ProofTreeController {
* To control stepping
*/
private
final
PuppetMaster
blocker
=
new
PuppetMaster
();
/**
* Goals of the state which is referenced by the statePointer
* TODO: weigl I don't understand this.
*/
private
final
ListProperty
<
GoalNode
<
KeyData
>>
currentGoals
=
new
SimpleListProperty
<>(
FXCollections
.
observableArrayList
());
...
...
@@ -123,10 +127,10 @@ public class ProofTreeController {
@Override
public
void
graphChanged
(
NodeAddedEvent
nodeAddedEvent
)
{
PTreeNode
added
=
nodeAddedEvent
.
getAddedNode
();
if
(
added
.
get
State
()
!=
null
)
{
if
(
added
.
get
ExtendedState
().
getStateBeforeStmt
()
!=
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().getScript
s
tmt()));
// Events.fire(new Events.NewNodeExecuted(nodeAddedEvent.getAddedNode().getScript
S
tmt()));
}
}
...
...
@@ -136,28 +140,15 @@ 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.getScript
s
tmt()));
//Events.fire(new Events.NewNodeExecuted(changedNode.getScript
S
tmt()));
}
};
public
ProofScript
getMainScript
()
{
return
mainScript
.
get
();
}
public
void
setMainScript
(
ProofScript
mainScript
)
{
this
.
mainScript
.
set
(
mainScript
);
}
public
SimpleObjectProperty
<
ProofScript
>
mainScriptProperty
()
{
return
mainScript
;
}
/**
*
Create a new ProofTreeController
*
and bind properties
* Create a new ProofTreeController
* and bind properties
*/
public
ProofTreeController
()
{
...
...
@@ -172,38 +163,61 @@ 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
().
getStateBeforeStmt
());
}
});
}
private
static
boolean
compareCtrlFlowNodes
(
ControlFlowNode
newNode
,
ControlFlowNode
oldNode
)
{
return
newNode
.
getScriptstmt
().
getNodeName
().
equals
(
oldNode
.
getScriptstmt
().
getNodeName
());
}
private
static
boolean
comparePTreeNodes
(
PTreeNode
newTreeNode
,
PTreeNode
oldTreeNode
)
{
return
false
;
}
public
ProofScript
getMainScript
()
{
return
mainScript
.
get
();
}
public
void
setMainScript
(
ProofScript
mainScript
)
{
this
.
mainScript
.
set
(
mainScript
);
}
//TODO handle endpoint
public
SimpleObjectProperty
<
ProofScript
>
mainScriptProperty
()
{
return
mainScript
;
}
//TODO handle endpoint of graph
/**
* 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
)
{
//setCurrentHighlightNode(statePointer.getScriptstmt());
LOGGER
.
info
(
"Setting new State "
+
state
.
toString
());
//setCurrentHighlightNode(statePointer.getScriptStmt());
//get all goals that are open
Object
[]
arr
=
state
.
getGoals
().
stream
().
filter
(
keyDataGoalNode
->
!
keyDataGoalNode
.
isClosed
()).
toArray
(
);
//List<GoalNode<KeyData>>
arr = state.getGoals().stream().filter(keyDataGoalNode -> !keyDataGoalNode.isClosed()).
collect(Collectors.toList()
);
//if there is no selected goal node we might have reached
//a closed proof
if
(
state
.
getSelectedGoalNode
()
==
null
)
{
setCurrentSelectedGoal
(
null
);
setCurrentGoals
(
arr
.
length
==
0
?
Collections
.
emptyList
()
:
state
.
getGoals
());
setCurrentGoals
(
state
.
getGoals
());
}
else
{
setCurrentGoals
(
state
.
getGoals
());
...
...
@@ -212,8 +226,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"
);
}
...
...
@@ -221,19 +235,6 @@ public class ProofTreeController {
}
//TODO handle endpoint
private
static
boolean
compareCtrlFlowNodes
(
ControlFlowNode
newNode
,
ControlFlowNode
oldNode
)
{
return
newNode
.
getScriptstmt
().
getNodeName
().
equals
(
oldNode
.
getScriptstmt
().
getNodeName
());
}
//TODO handle endpoint of graph
private
static
boolean
comparePTreeNodes
(
PTreeNode
newTreeNode
,
PTreeNode
oldTreeNode
)
{
return
false
;
}
/**
* StepOver and return the node to which the state pointer is pointing to
*
...
...
@@ -254,7 +255,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
)
{
...
...
@@ -290,7 +291,7 @@ public class ProofTreeController {
if
(
current
!=
null
)
{
this
.
statePointer
=
stateGraphWrapper
.
getStepBack
(
current
);
if
(
this
.
statePointer
!=
null
)
{
setNewState
(
statePointer
.
get
State
());
setNewState
(
statePointer
.
get
ExtendedState
().
getStateBeforeStmt
());
}
else
{
this
.
statePointer
=
current
;
}
...
...
@@ -307,6 +308,7 @@ public class ProofTreeController {
/**
* Execute script with breakpoints
*
* @param debugMode
* @param statusBar
* @param breakpoints
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
View file @
9dfb35b5
...
...
@@ -9,9 +9,9 @@ import de.uka.ilkd.key.proof.Goal;
import
de.uka.ilkd.key.proof.Node
;
import
de.uka.ilkd.key.settings.ProofIndependentSettings
;
import
edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade
;
import
edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath
;
import
edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade
;
import
edu.kit.iti.formal.psdbg.termmatcher.Matchings
;
import
edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath
;
import
javafx.beans.Observable
;
import
javafx.beans.property.SimpleObjectProperty
;
import
javafx.beans.value.ObservableBooleanValue
;
...
...
@@ -119,7 +119,7 @@ public class SequentView extends CodeArea {
NamespaceSet
nss
=
services
.
getNamespaces
();
Sequent
sequent
=
node
.
get
().
sequent
();
filter
=
new
IdentitySequentPrintFilter
(
sequent
);
filter
=
new
IdentitySequentPrintFilter
();
ProgramPrinter
prgPrinter
=
new
ProgramPrinter
(
new
StringWriter
());
this
.
backend
=
new
LogicPrinter
.
PosTableStringBackend
(
80
);
...
...
@@ -195,7 +195,7 @@ public class SequentView extends CodeArea {
if
(
node
.
get
().
sequent
()
!=
null
)
{
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
node
.
get
().
sequent
(),
true
);
if
(
m
.
size
()
==
0
)
return
false
;
Map
<
String
,
MatchPath
>
va
=
m
.
first
();
Map
<
String
,
MatchPath
>
va
=
m
.
first
();
System
.
out
.
println
(
va
);
//TODO remove
for
(
MatchPath
mp
:
va
.
values
())
{
System
.
out
.
println
(
mp
.
pio
());
...
...
@@ -209,7 +209,8 @@ public class SequentView extends CodeArea {
if
(
backend
==
null
)
{
return
;
}
ImmutableList
<
Integer
>
path
=
ImmutableSLList
.
singleton
(
1
);
ImmutableList
<
Integer
>
path
=
ImmutableSLList
.<
Integer
>
nil
().
append
(
1
);
Range
r
=
backend
.
getInitialPositionTable
().
rangeForPath
(
path
);
setStyle
(
r
.
start
(),
r
.
end
(),
Collections
.
singleton
(
"search-highlight"
));
}
...
...
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