Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
sarah.grebing
ProofScriptParser
Commits
18d2aec5
Commit
18d2aec5
authored
Nov 12, 2018
by
Lulu Luong
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
#45
parent
f2597ce9
Pipeline
#31829
failed with stages
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
140 additions
and
19 deletions
+140
-19
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
...edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
+2
-2
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/RepeatTreeNode.java
.../formal/psdbg/gui/controls/ScriptTree/RepeatTreeNode.java
+48
-0
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTreeGraph.java
...du/kit/iti/formal/psdbg/gui/controls/ScriptTreeGraph.java
+72
-14
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTreeView.java
...edu/kit/iti/formal/psdbg/gui/controls/ScriptTreeView.java
+18
-3
No files found.
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @
18d2aec5
...
...
@@ -1406,7 +1406,7 @@ public class DebuggerMain implements Initializable {
keyWindow
.
makePrettyView
();
keyWindow
.
setVisible
(
true
);
}
catch
(
SecurityException
e
)
{
e
.
printStackTrace
();
//
e.printStackTrace();
}
...
...
@@ -1566,7 +1566,7 @@ public class DebuggerMain implements Initializable {
private
class
KeYSecurityManager
extends
SecurityManager
{
@Override
public
void
checkExit
(
int
status
)
{
throw
new
SecurityException
();
throw
new
SecurityException
(
"KeY window closed"
);
}
@Override
public
void
checkPermission
(
Permission
perm
)
{
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTree/RepeatTreeNode.java
0 → 100644
View file @
18d2aec5
package
edu.kit.iti.formal.psdbg.gui.controls.ScriptTree
;
import
de.uka.ilkd.key.proof.Node
;
import
edu.kit.iti.formal.psdbg.gui.controls.TreeNode
;
import
edu.kit.iti.formal.psdbg.interpreter.data.KeyData
;
import
edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode
;
import
edu.kit.iti.formal.psdbg.parser.ast.CallStatement
;
import
edu.kit.iti.formal.psdbg.parser.ast.GuardedCaseStatement
;
import
edu.kit.iti.formal.psdbg.parser.ast.MatchExpression
;
import
edu.kit.iti.formal.psdbg.parser.ast.TermLiteral
;
import
lombok.Getter
;
import
lombok.RequiredArgsConstructor
;
import
lombok.Setter
;
/**
* This calss represents a node in the script tree, whcih can be of different kinds.
* The scriptTreeNodes is the model calls for TreeNodes
*/
public
class
RepeatTreeNode
extends
AbstractTreeNode
{
@Getter
private
final
PTreeNode
<
KeyData
>
scriptState
;
@Getter
@Setter
private
final
int
linenr
;
private
final
boolean
repeatstart
;
public
RepeatTreeNode
(
Node
node
,
PTreeNode
<
KeyData
>
scriptState
,
int
linenr
,
boolean
repeatstart
)
{
super
(
node
);
this
.
scriptState
=
scriptState
;
this
.
linenr
=
linenr
;
this
.
repeatstart
=
repeatstart
;
}
@Override
public
String
toString
(){
return
scriptState
.
getStatement
().
toString
()+
" with ID "
+
scriptState
.
getId
();
}
@Override
public
TreeNode
toTreeNode
()
{
String
label
=
(
repeatstart
)?
"repeat in line "
+
linenr
+
" START"
:
"repeat in line "
+
linenr
+
" END"
;
return
new
TreeNode
(
label
,
getNode
());
}
}
\ No newline at end of file
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTreeGraph.java
View file @
18d2aec5
...
...
@@ -43,7 +43,14 @@ public class ScriptTreeGraph {
private
List
<
PlaceholderNode
>
placeholderNodes
;
private
HashMap
<
Node
,
PTreeNode
>
foreachNodes
;
private
HashMap
<
Node
,
PTreeNode
>
repeatNodes
;
/**
* statistic of scripttree
*/
private
int
openGoals
=
0
;
private
int
closedGoals
=
0
;
...
...
@@ -54,6 +61,7 @@ public class ScriptTreeGraph {
ScriptTreeNode
rootNode
=
new
ScriptTreeNode
(
root
,
rootPTreeNode
,
rootPTreeNode
.
getStatement
().
getStartPosition
().
getLineNumber
());
mapping
=
new
HashMap
<>();
foreachNodes
=
new
HashMap
<>();
repeatNodes
=
new
HashMap
<>();
placeholderNodes
=
new
ArrayList
<>();
front
=
new
ArrayList
<>();
sortedList
=
new
ArrayList
<>();
...
...
@@ -70,7 +78,8 @@ public class ScriptTreeGraph {
computeList
();
compute
();
addGoals
();
System
.
out
.
println
(
"openGoals = "
+
openGoals
);
System
.
out
.
println
(
"closedGoals = "
+
closedGoals
);
}
...
...
@@ -250,6 +259,7 @@ public class ScriptTreeGraph {
switch
(
children
.
size
())
{
case
0
:
putIntoFront
(
callnode
);
checkIfRepeatEnd
(
callnode
);
checkIfForeachEnd
(
callnode
);
addPlaceholder
(
sn
,
sn
.
getNode
());
break
;
...
...
@@ -291,7 +301,10 @@ public class ScriptTreeGraph {
}
if
(
children
.
size
()
>
0
)
{
children
.
forEach
(
k
->
checkIfForeachEnd
(
k
.
getData
().
getNode
()));
children
.
forEach
(
k
->
{
checkIfRepeatEnd
(
k
.
getData
().
getNode
());
checkIfForeachEnd
(
k
.
getData
().
getNode
());
});
}
return
null
;
...
...
@@ -355,6 +368,34 @@ public class ScriptTreeGraph {
aftergoals
.
forEach
(
k
->
foreachNodes
.
put
(
k
.
getData
().
getNode
(),
nextPtreeNode
));
return
null
;
}
@Override
public
Void
visit
(
RepeatStatement
repeat
){
List
<
GoalNode
<
KeyData
>>
goals
=
nextPtreeNode
.
getStateBeforeStmt
().
getGoals
();
if
(
goals
.
size
()
==
0
)
return
null
;
goals
.
forEach
(
k
->
{
RepeatTreeNode
ftn
=
new
RepeatTreeNode
(
k
.
getData
().
getNode
(),
nextPtreeNode
,
nextPtreeNode
.
getStatement
().
getStartPosition
().
getLineNumber
(),
true
);
replacePlaceholder
(
searchParentInMapping
(
k
.
getData
().
getNode
()),
ftn
);
addPlaceholder
(
ftn
,
k
.
getData
().
getNode
());
});
// add to repeat list -> so the end of a repeat can be catched
List
<
GoalNode
<
KeyData
>>
aftergoals
=
(
nextPtreeNode
.
getStateAfterStmt
()
!=
null
)?
nextPtreeNode
.
getStateAfterStmt
().
getGoals
()
:
(
nextPtreeNode
.
getStepOver
()
!=
null
&&
nextPtreeNode
.
getStepOver
().
getStateBeforeStmt
()
!=
null
)
?
nextPtreeNode
.
getStepOver
().
getStateBeforeStmt
().
getGoals
()
:
new
ArrayList
<>();
aftergoals
.
forEach
(
k
->
repeatNodes
.
put
(
k
.
getData
().
getNode
(),
nextPtreeNode
));
return
null
;
}
}
...
...
@@ -460,6 +501,25 @@ public class ScriptTreeGraph {
}
}
/*
checks if given node is the end of a repeat-statement
*/
private
void
checkIfRepeatEnd
(
Node
n
)
{
if
(
repeatNodes
.
containsKey
(
n
))
{
PTreeNode
ptn
=
repeatNodes
.
get
(
n
);
RepeatTreeNode
ftn
=
new
RepeatTreeNode
(
n
,
ptn
,
ptn
.
getStatement
().
getStartPosition
().
getLineNumber
(),
false
);
replacePlaceholder
(
n
,
ftn
);
addPlaceholder
(
ftn
,
n
);
repeatNodes
.
remove
(
n
);
}
}
/**
* Get all Branchlabels from child to parent GoalNode
* Order of Branchlabels is from bottom to top
...
...
@@ -491,17 +551,6 @@ public class ScriptTreeGraph {
return
branchlabels
;
}
private
boolean
sameBranchlabelBefore
(
List
<
BranchLabelNode
>
branchlabels
,
Node
node
)
{
if
(
branchlabels
.
size
()
==
0
)
return
false
;
return
branchlabels
.
get
(
branchlabels
.
size
()-
1
).
getNode
().
serialNr
()
==
node
.
serialNr
();
}
private
boolean
isBranchLabel
(
String
label
)
{
if
(
label
.
contains
(
"rule"
)
||
label
.
contains
(
"rules"
)
||
label
.
equals
(
"Normal Execution"
))
return
false
;
return
true
;
}
/**
* Inserts given node after Branchlabelnodes
* @param node
...
...
@@ -572,7 +621,16 @@ public class ScriptTreeGraph {
}
private
void
addGoals
()
{
front
.
forEach
(
k
->
replacePlaceholder
(
k
,
new
DummyGoalNode
(
k
,
k
.
isClosed
())));
front
.
forEach
(
k
->
{
replacePlaceholder
(
k
,
new
DummyGoalNode
(
k
,
k
.
isClosed
()));
//fill statistics
if
(
k
.
isClosed
())
{
closedGoals
++;
}
else
{
openGoals
++;
}
});
}
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptTreeView.java
View file @
18d2aec5
package
edu.kit.iti.formal.psdbg.gui.controls
;
import
com.sun.javafx.css.Style
;
import
de.uka.ilkd.key.proof.Node
;
import
edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain
;
import
edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.*
;
import
javafx.beans.binding.Bindings
;
import
javafx.beans.property.MapProperty
;
import
javafx.beans.property.SimpleMapProperty
;
import
javafx.collections.FXCollections
;
import
javafx.fxml.FXML
;
import
javafx.scene.control.ColorPicker
;
import
javafx.scene.control.TreeCell
;
import
javafx.scene.control.TreeItem
;
import
javafx.scene.control.TreeView
;
import
javafx.scene.control.cell.TextFieldTreeCell
;
import
javafx.scene.layout.Background
;
import
javafx.scene.layout.BackgroundFill
;
import
javafx.scene.layout.BorderPane
;
import
javafx.scene.layout.CornerRadii
;
import
javafx.util.StringConverter
;
import
lombok.Setter
;
import
java.awt.*
;
import
java.util.List
;
import
java.util.Map
;
...
...
@@ -45,6 +52,7 @@ public class ScriptTreeView extends BorderPane {
private
TreeCell
<
AbstractTreeNode
>
cellFactory
(
TreeView
<
AbstractTreeNode
>
nodeTreeView
)
{
TextFieldTreeCell
<
AbstractTreeNode
>
tftc
=
new
TextFieldTreeCell
<>();
StringConverter
<
AbstractTreeNode
>
stringConverter
=
new
StringConverter
<
AbstractTreeNode
>()
{
@Override
...
...
@@ -129,9 +137,9 @@ public class ScriptTreeView extends BorderPane {
private
void
repaint
(
TextFieldTreeCell
<
AbstractTreeNode
>
tftc
)
{
AbstractTreeNode
item
=
tftc
.
getItem
();
Node
n
=
item
.
getNode
();
tftc
.
styleProperty
().
unbind
();
tftc
.
setStyle
(
""
);
if
(
n
!=
null
)
{
if
(
item
instanceof
ScriptTreeNode
)
{
tftc
.
setStyle
(
"-fx-text-fill: grey"
);
}
else
if
(
item
instanceof
BranchLabelNode
)
{
...
...
@@ -140,9 +148,14 @@ public class ScriptTreeView extends BorderPane {
}
else
if
(
item
instanceof
DummyGoalNode
)
{
if
(
n
.
isClosed
())
{
tftc
.
setStyle
(
"-fx-background-color: lightgreen"
);
tftc
.
styleProperty
().
setValue
(
"-fx-background-color: lightgreen"
);
//styleProperty().bind(tftc.styleProperty());
}
else
{
tftc
.
setStyle
(
"-fx-background-color: indianred"
);
tftc
.
styleProperty
().
setValue
(
"-fx-background-color: indianred"
);
//styleProperty().bind(tftc.styleProperty());
// tftc.setStyle("-fx-background-color: indianred");
//colorOfNodes.putIfAbsent(n, "indianred");
}
}
...
...
@@ -156,5 +169,7 @@ public class ScriptTreeView extends BorderPane {
}
}
}
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