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
cad71758
Commit
cad71758
authored
May 24, 2018
by
Alexander Weigl
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
bug fixing, a framework for script trees
parent
591415cf
Pipeline
#22019
passed with stages
in 6 minutes and 41 seconds
Changes
11
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
11 changed files
with
54 additions
and
36 deletions
+54
-36
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java
.../kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java
+1
-1
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java
.../edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java
+1
-1
rt-key/src/main/java/edu/kit/iti/formal/psdbg/storage/KeyPersistentFacade.java
...edu/kit/iti/formal/psdbg/storage/KeyPersistentFacade.java
+1
-1
rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/KeyMatcherDerivableTest.java
...iti/formal/psdbg/interpreter/KeyMatcherDerivableTest.java
+1
-1
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java
...a/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java
+28
-18
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/PTreeNode.java
...a/edu/kit/iti/formal/psdbg/interpreter/dbg/PTreeNode.java
+3
-2
rt/src/test/java/edu/kit/iti/formal/psdbg/interpreter/EvalTest.java
...t/java/edu/kit/iti/formal/psdbg/interpreter/EvalTest.java
+1
-1
rt/src/test/java/edu/kit/iti/formal/psdbg/interpreter/EvaluatorTest.java
...a/edu/kit/iti/formal/psdbg/interpreter/EvaluatorTest.java
+2
-2
rt/src/test/java/edu/kit/iti/formal/psdbg/interpreter/MatchEvaluatorTest.java
.../kit/iti/formal/psdbg/interpreter/MatchEvaluatorTest.java
+2
-2
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
...java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
+8
-6
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java
...ava/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java
+6
-1
No files found.
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java
View file @
cad71758
...
...
@@ -206,7 +206,7 @@ public class InterpreterBuilder {
ImmutableList
<
Goal
>
openGoals
=
proof
.
getSubtreeGoals
(
proof
.
root
());
List
<
GoalNode
<
KeyData
>>
goals
=
openGoals
.
stream
().
map
(
g
->
new
GoalNode
<>(
null
,
new
KeyData
(
g
,
keyEnvironment
,
proof
)
,
false
))
new
GoalNode
<>(
new
KeyData
(
g
,
keyEnvironment
,
proof
)))
.
collect
(
Collectors
.
toList
());
...
...
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java
View file @
cad71758
...
...
@@ -265,7 +265,7 @@ public class KeYProofFacade {
KeYEnvironment
env
=
getEnvironment
();
ImmutableList
<
Goal
>
openGoals
=
p
.
getSubtreeGoals
(
p
.
root
());
List
<
GoalNode
<
KeyData
>>
goals
=
openGoals
.
stream
().
map
(
g
->
new
GoalNode
<>(
null
,
new
KeyData
(
g
,
env
,
p
)
,
false
))
new
GoalNode
<>(
new
KeyData
(
g
,
env
,
p
)))
.
collect
(
Collectors
.
toList
());
return
goals
;
}
...
...
rt-key/src/main/java/edu/kit/iti/formal/psdbg/storage/KeyPersistentFacade.java
View file @
cad71758
...
...
@@ -43,7 +43,7 @@ public class KeyPersistentFacade {
Node
node
=
WalkableLabelFacade
.
findNode
(
proof
,
pg
.
getGoalIdentifier
());
Goal
goal
=
proof
.
getGoal
(
node
);
KeyData
kd
=
new
KeyData
(
goal
,
env
,
proof
);
GoalNode
<
KeyData
>
gn
=
new
GoalNode
<>(
null
,
kd
,
false
);
GoalNode
<
KeyData
>
gn
=
new
GoalNode
<>(
kd
);
state
.
getGoals
().
add
(
gn
);
if
(
pg
.
isSelected
())
state
.
setSelectedGoalNode
(
gn
);
...
...
rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/KeyMatcherDerivableTest.java
View file @
cad71758
...
...
@@ -25,7 +25,7 @@ public class KeyMatcherDerivableTest {
Goal
g
=
proof
.
getGoal
(
proof
.
root
());
KeyData
newKeYData
=
new
KeyData
(
g
,
f
.
getEnvironment
(),
proof
);
GoalNode
<
KeyData
>
gn
=
new
GoalNode
<>(
null
,
newKeYData
,
newKeYData
.
isClosedNode
()
);
GoalNode
<
KeyData
>
gn
=
new
GoalNode
<>(
newKeYData
);
Term
termQ
=
new
TermBuilder
(
f
.
getEnvironment
().
getServices
().
getTermFactory
(),
f
.
getEnvironment
().
getServices
()).
parseTerm
(
"q"
);
System
.
out
.
println
(
termQ
);
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java
View file @
cad71758
...
...
@@ -3,17 +3,21 @@ package edu.kit.iti.formal.psdbg.interpreter.data;
import
edu.kit.iti.formal.psdbg.parser.ast.Variable
;
import
edu.kit.iti.formal.psdbg.parser.data.Value
;
import
edu.kit.iti.formal.psdbg.parser.types.Type
;
import
lombok.EqualsAndHashCode
;
import
lombok.Getter
;
import
lombok.Setter
;
import
lombok.ToString
;
import
javax.annotation.Nonnull
;
/**
* Objects of this class represent a GoalNode in a script state
* If parent is null, this is the root
*
* @author S.Grebing
*/
@ToString
@ToString
(
of
=
"id"
)
@EqualsAndHashCode
(
of
=
"id"
)
public
class
GoalNode
<
T
>
{
@Getter
@Setter
...
...
@@ -28,26 +32,34 @@ public class GoalNode<T> {
@Getter
private
boolean
isClosed
;
/**
*
*
* @param parent
* @param data
*/
public
GoalNode
(
GoalNode
<
T
>
parent
,
T
data
,
boolean
isClosed
)
{
this
.
assignments
=
new
VariableAssignment
(
parent
==
null
?
null
:
parent
.
getAssignments
().
deepCopy
());
this
.
parent
=
parent
;
this
.
data
=
data
;
this
.
isClosed
=
isClosed
;
private
int
id
=
super
.
hashCode
();
public
GoalNode
(
T
data
)
{
this
(
null
,
new
VariableAssignment
(),
data
,
false
);
}
public
GoalNode
(
@Nonnull
GoalNode
<
T
>
parent
,
T
data
,
boolean
isClosed
)
{
this
(
parent
,
parent
.
getAssignments
(),
data
,
isClosed
);
}
private
GoalNode
(
GoalNode
<
T
>
parent
,
VariableAssignment
assignments
,
T
data
,
boolean
isClosed
)
{
this
.
assignments
=
assignments
.
deepCopy
();
this
.
assignments
=
assignments
.
push
();
this
.
parent
=
parent
;
this
.
data
=
data
;
this
.
isClosed
=
isClosed
;
}
private
GoalNode
(
int
id
,
GoalNode
<
T
>
tGoalNode
,
T
data
,
boolean
isClosed
)
{
this
(
tGoalNode
,
data
,
isClosed
);
this
.
id
=
id
;
}
private
GoalNode
(
int
id
,
T
data
,
boolean
isClosed
)
{
this
(
data
);
this
.
isClosed
=
isClosed
;
this
.
id
=
id
;
}
/**
* @param varname
* @return value of variable if it exists
...
...
@@ -111,12 +123,10 @@ public class GoalNode<T> {
public
GoalNode
<
T
>
deepCopy
()
{
if
(
parent
!=
null
)
{
return
new
GoalNode
<
T
>(
parent
.
deepCopy
(),
data
,
isClosed
);
return
new
GoalNode
<
T
>(
id
,
parent
.
deepCopy
(),
data
,
isClosed
);
}
else
{
return
new
GoalNode
<
T
>(
parent
,
assignments
.
deepCopy
()
,
data
,
isClosed
);
return
new
GoalNode
<
T
>(
id
,
data
,
isClosed
);
}
}
public
VariableAssignment
enterScope
(
VariableAssignment
va
)
{
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/PTreeNode.java
View file @
cad71758
...
...
@@ -121,13 +121,14 @@ public class PTreeNode<T> {
}
public
Collection
<
GoalNode
<
T
>>
getMutatedNodes
()
{
if
(
statement
instanceof
CallStatement
)
{
//TODO better predicate for mutators
if
(!
(
statement
instanceof
CallStatement
)
)
{
//TODO better predicate for mutators
return
Collections
.
emptyList
();
}
assert
stateAfterStmt
!=
null
&&
stateBeforeStmt
!=
null
;
ArrayList
<
PTreeNode
<
T
>>
list
=
new
ArrayList
<>();
GoalNode
<
T
>
incoming
=
stateBeforeStmt
.
getSelectedGoalNode
();
return
stateAfterStmt
.
getGoals
().
stream
().
filter
(
gn
->
gn
.
getParent
()
==
incoming
).
collect
(
Collectors
.
toList
());
return
stateAfterStmt
.
getGoals
().
stream
().
filter
(
gn
->
gn
.
getParent
().
equals
(
incoming
)).
collect
(
Collectors
.
toList
());
}
}
\ No newline at end of file
rt/src/test/java/edu/kit/iti/formal/psdbg/interpreter/EvalTest.java
View file @
cad71758
...
...
@@ -57,7 +57,7 @@ public class EvalTest {
Expression
e_exp
=
TestHelper
.
toExpr
(
expResult
);
VariableAssignment
s
=
createAssignments
();
Evaluator
evaluator
=
new
Evaluator
(
s
,
new
GoalNode
(
null
,
null
,
true
));
Evaluator
<
String
>
evaluator
=
new
Evaluator
<>
(
s
,
new
GoalNode
<>
(
null
));
Value
is
=
evaluator
.
eval
(
e_is
);
Value
exp
=
evaluator
.
eval
(
e_exp
);
...
...
rt/src/test/java/edu/kit/iti/formal/psdbg/interpreter/EvaluatorTest.java
View file @
cad71758
...
...
@@ -35,14 +35,14 @@ public class EvaluatorTest {
@Before
public
void
setup
()
{
GoalNode
<
String
>
parent
=
new
GoalNode
<>(
null
,
"pa"
,
false
);
GoalNode
<
String
>
parent
=
new
GoalNode
<>(
"pa"
);
parent
.
getAssignments
()
.
declare
(
"a"
,
SimpleType
.
INT
)
.
declare
(
"b"
,
SimpleType
.
INT
)
.
assign
(
"a"
,
Value
.
from
(
1
))
.
assign
(
"b"
,
Value
.
from
(
1
));
GoalNode
<
String
>
selected
=
new
GoalNode
<>(
parent
,
"selg"
,
false
);
eval
=
new
Evaluator
(
selected
.
getAssignments
(),
selected
);
eval
=
new
Evaluator
<>
(
selected
.
getAssignments
(),
selected
);
eval
.
setMatcher
(
new
PseudoMatcher
());
}
...
...
rt/src/test/java/edu/kit/iti/formal/psdbg/interpreter/MatchEvaluatorTest.java
View file @
cad71758
...
...
@@ -17,13 +17,13 @@ public class MatchEvaluatorTest {
@Before
public
void
setup
()
{
GoalNode
<
String
>
parent
=
new
GoalNode
<>(
null
,
"pa"
,
false
);
GoalNode
<
String
>
parent
=
new
GoalNode
<>(
"pa"
);
parent
.
declareVariable
(
new
Variable
(
"a"
),
SimpleType
.
INT
);
parent
.
declareVariable
(
new
Variable
(
"b"
),
SimpleType
.
INT
);
VariableAssignment
va
=
parent
.
getAssignments
();
va
.
assign
(
new
Variable
(
"a"
),
Value
.
from
(
1
));
va
.
assign
(
new
Variable
(
"b"
),
Value
.
from
(
1
));
GoalNode
selected
=
new
GoalNode
(
parent
,
"selg"
,
false
);
GoalNode
<
String
>
selected
=
new
GoalNode
<>
(
parent
,
"selg"
,
false
);
mEval
=
new
MatchEvaluator
(
va
,
selected
,
new
PseudoMatcher
());
}
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
View file @
cad71758
...
...
@@ -433,11 +433,13 @@ public class ProofTree extends BorderPane {
mutatedBy
.
clear
();
nodes
.
forEach
(
pn
->
{
try
{
Node
startNode
=
pn
.
getStateBeforeStmt
().
getSelectedGoalNode
().
getData
().
getNode
();
mutatedBy
.
put
(
startNode
,
pn
.
getStatement
());
pn
.
getMutatedNodes
().
forEach
(
mn
->
{
entryExitMap
.
put
(
startNode
,
mn
.
getData
().
getNode
());
});
if
(
pn
.
isAtomic
())
{
Node
startNode
=
pn
.
getStateBeforeStmt
().
getSelectedGoalNode
().
getData
().
getNode
();
mutatedBy
.
put
(
startNode
,
pn
.
getStatement
());
pn
.
getMutatedNodes
().
forEach
(
mn
->
{
entryExitMap
.
put
(
startNode
,
mn
.
getData
().
getNode
());
});
}
}
catch
(
NullPointerException
e
)
{
}
}
...
...
@@ -450,7 +452,7 @@ public class ProofTree extends BorderPane {
val
currentItem
=
itemFactory
(
n
);
for
(
Node
child
:
entryExitMap
.
get
(
n
))
{
if
(
isMutated
(
child
))
{
currentItem
.
getChildren
().
add
(
populate
(
""
,
n
));
currentItem
.
getChildren
().
add
(
populate
(
""
,
child
));
}
else
{
currentItem
.
getChildren
().
add
(
super
.
itemFactory
(
child
));
}
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java
View file @
cad71758
...
...
@@ -10,6 +10,7 @@ import edu.kit.iti.formal.psdbg.gui.actions.inline.InlineActionSupplier;
import
edu.kit.iti.formal.psdbg.gui.controller.Events
;
import
edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier
;
import
edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint
;
import
edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerCommand
;
import
edu.kit.iti.formal.psdbg.lint.LintProblem
;
import
edu.kit.iti.formal.psdbg.lint.LinterStrategy
;
import
edu.kit.iti.formal.psdbg.parser.Facade
;
...
...
@@ -98,6 +99,8 @@ public class ScriptArea extends BorderPane {
*/
private
final
BooleanProperty
dirty
=
new
SimpleBooleanProperty
(
this
,
"dirty"
,
false
);
/**
* CSS classes for regions, used for "manually" highlightning. e.g. debugging marker
*/
...
...
@@ -130,6 +133,8 @@ public class ScriptArea extends BorderPane {
@Getter
@Setter
private
List
<
InlineActionSupplier
>
inlineActionSuppliers
=
new
ArrayList
<>();
private
Logger
consoleLogger
=
LogManager
.
getLogger
(
"console"
);
public
ScriptArea
()
{
init
();
...
...
@@ -192,9 +197,9 @@ public class ScriptArea extends BorderPane {
installPopup
();
setOnMouseClicked
(
evt
->
{
System
.
out
.
println
(
"ScriptArea.init"
+
evt
.
isControlDown
());
inlineToolbar
.
hide
();
if
(
evt
.
isControlDown
()
&&
evt
.
getButton
()
==
MouseButton
.
PRIMARY
)
{
consoleLogger
.
info
(
"Show inline toolbar"
);
inlineToolbar
.
show
();
evt
.
consume
();
}
...
...
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