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
7fbd75b5
Commit
7fbd75b5
authored
Jun 14, 2018
by
Lulu Luong
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
whole underline
+ Proof tree
parent
a19583e8
Pipeline
#22642
passed with stages
in 3 minutes and 18 seconds
Changes
6
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
131 additions
and
13 deletions
+131
-13
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/KeyData.java
...va/edu/kit/iti/formal/psdbg/interpreter/data/KeyData.java
+0
-1
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/SaveCommand.java
...kit/iti/formal/psdbg/interpreter/funchdl/SaveCommand.java
+4
-1
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
...edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
+2
-1
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
...java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
+111
-7
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTreeContextMenu.java
...t/iti/formal/psdbg/gui/controls/ProofTreeContextMenu.java
+7
-1
ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.fxml
...rces/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.fxml
+7
-2
No files found.
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/KeyData.java
View file @
7fbd75b5
...
...
@@ -19,7 +19,6 @@ import java.util.Set;
*/
@Data
@AllArgsConstructor
@ToString
@EqualsAndHashCode
@RequiredArgsConstructor
public
class
KeyData
{
...
...
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/SaveCommand.java
View file @
7fbd75b5
...
...
@@ -17,6 +17,7 @@ import org.apache.logging.log4j.Logger;
import
javax.annotation.Nullable
;
import
javax.xml.bind.JAXBException
;
import
java.io.File
;
import
java.io.FileWriter
;
import
java.io.IOException
;
import
java.io.StringWriter
;
import
java.util.Optional
;
...
...
@@ -76,7 +77,9 @@ public class SaveCommand implements CommandHandler<KeyData> {
if
(
execute
.
get
())
interpreter
.
getSelectedNode
().
getData
().
getProof
().
saveToFile
(
newFile
);
KeyPersistentFacade
.
write
(
interpreter
.
getCurrentState
(),
new
StringWriter
());
KeyPersistentFacade
.
write
(
interpreter
.
getCurrentState
(),
new
FileWriter
(
sp
.
getPersistedStateFile
(
newFile
)));
System
.
out
.
println
();
}
catch
(
IOException
e
)
{
e
.
printStackTrace
();
}
catch
(
InterruptedException
e
)
{
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @
7fbd75b5
...
...
@@ -1271,7 +1271,8 @@ public class DebuggerMain implements Initializable {
try
{
KeyPersistentFacade
.
read
(
FACADE
.
getEnvironment
(),
FACADE
.
getProof
(),
new
StringReader
(
selected
.
getPersistedStateFile
(
FACADE
.
getFilepath
()).
toString
()));
State
state
=
KeyPersistentFacade
.
read
(
FACADE
.
getEnvironment
(),
FACADE
.
getProof
(),
new
StringReader
(
selected
.
getPersistedStateFile
(
FACADE
.
getFilepath
()).
toString
()));
//TODO setstate
}
catch
(
JAXBException
e
)
{
e
.
printStackTrace
();
}
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
View file @
7fbd75b5
...
...
@@ -21,6 +21,7 @@ import javafx.collections.ObservableList;
import
javafx.collections.ObservableMap
;
import
javafx.collections.ObservableSet
;
import
javafx.fxml.FXML
;
import
javafx.fxml.FXMLLoader
;
import
javafx.scene.control.ContextMenu
;
import
javafx.scene.control.TreeCell
;
import
javafx.scene.control.TreeItem
;
...
...
@@ -50,6 +51,12 @@ public class ProofTree extends BorderPane {
private
MapProperty
<
Node
,
String
>
colorOfNodes
=
new
SimpleMapProperty
<
Node
,
String
>(
FXCollections
.
observableHashMap
());
@FXML
private
TreeView
<
TreeNode
>
treeProof
;
//TODO: added for testing
@FXML
private
TreeView
<
TreeNode
>
treeScript
;
private
ContextMenu
contextMenu
;
private
BooleanProperty
deactivateRefresh
=
new
SimpleBooleanProperty
();
...
...
@@ -105,6 +112,9 @@ public class ProofTree extends BorderPane {
}
};
private
TreeTransformationKey
treeCreation
;
@Getter
private
TreeTransformationScript
treeScriptCreation
;
private
DebuggerMain
main
;
public
ProofTree
(
DebuggerMain
main
)
{
Utils
.
createWithFXML
(
this
);
...
...
@@ -112,9 +122,12 @@ public class ProofTree extends BorderPane {
//main.getModel().debuggerFrameworkProperty().addListener((p, n, m) -> {
// treeCreation = new TreeTransformationScript(m.getPtreeManager());
//});
this
.
main
=
main
;
treeCreation
=
new
TreeTransformationKey
();
treeProof
.
setCellFactory
(
this
::
cellFactory
);
treeScript
.
setCellFactory
(
this
::
cellFactory
);
root
.
addListener
(
o
->
init
());
proof
.
addListener
((
prop
,
old
,
n
)
->
{
if
(
old
!=
null
)
{
...
...
@@ -167,6 +180,7 @@ public class ProofTree extends BorderPane {
//val treeNode = new TreeNode("Proof", root.get());
treeProof
.
setRoot
(
item
);
treeScript
.
setRoot
(
item
);
}
}
...
...
@@ -196,7 +210,6 @@ public class ProofTree extends BorderPane {
}
private
void
init
()
{
}
private
TreeCell
<
TreeNode
>
cellFactory
(
TreeView
<
TreeNode
>
nodeTreeView
)
{
...
...
@@ -314,18 +327,24 @@ public class ProofTree extends BorderPane {
}
public
void
repopulate
()
{
treeScriptCreation
=
new
TreeTransformationScript
(
main
.
getModel
().
getDebuggerFramework
().
getPtreeManager
());
if
(
deactivateRefresh
.
get
())
return
;
if
(
root
.
get
()
!=
null
)
{
TreeItem
<
TreeNode
>
item
=
treeCreation
.
create
(
proof
.
get
());
treeProof
.
setRoot
(
item
);
TreeItem
<
TreeNode
>
scriptTree
=
treeScriptCreation
.
buildScriptTree
(
root
.
get
());
treeScript
.
setRoot
(
scriptTree
);
}
treeProof
.
refresh
();
treeScript
.
refresh
();
}
@AllArgsConstructor
private
static
class
TreeNode
{
String
label
;
...
...
@@ -414,7 +433,6 @@ public class ProofTree extends BorderPane {
}
@RequiredArgsConstructor
class
TreeTransformationScript
extends
TreeTransformationKey
{
final
ProofTreeManager
<
KeyData
>
manager
;
...
...
@@ -477,7 +495,7 @@ public class ProofTree extends BorderPane {
//TODO: Reverse ArrayList in the end or nah?
@Deprecated
public
ArrayList
<
String
>
getBranchLabels
(
TreeNode
node
)
{
public
ArrayList
<
String
>
getBranchLabels
(
TreeNode
node
)
{
TreeItem
<
TreeNode
>
proofTree
=
create
(
proof
.
get
());
ArrayList
<
String
>
branchlabels
=
new
ArrayList
<>();
...
...
@@ -485,7 +503,7 @@ public class ProofTree extends BorderPane {
int
i
=
0
;
branchlabels
.
set
(
0
,
node
.
label
);
while
(
node
!=
null
)
{
if
(!
branchlabels
.
get
(
i
).
equals
(
node
.
label
))
{
if
(!
branchlabels
.
get
(
i
).
equals
(
node
.
label
))
{
i
++;
branchlabels
.
set
(
i
,
node
.
label
);
}
...
...
@@ -495,7 +513,7 @@ public class ProofTree extends BorderPane {
return
branchlabels
;
}
public
ArrayList
<
String
>
getBranchLabels
(
Node
node
)
{
public
ArrayList
<
String
>
getBranchLabels
(
Node
node
)
{
ArrayList
<
String
>
branchlabels
=
new
ArrayList
<>();
int
i
=
0
;
...
...
@@ -503,7 +521,7 @@ public class ProofTree extends BorderPane {
branchlabels
.
set
(
0
,
node
.
getNodeInfo
().
getBranchLabel
());
Node
n
=
node
.
parent
();
while
(
n
!=
null
)
{
if
(!
branchlabels
.
get
(
i
).
equals
(
n
.
getNodeInfo
().
getBranchLabel
()))
{
if
(!
branchlabels
.
get
(
i
).
equals
(
n
.
getNodeInfo
().
getBranchLabel
()))
{
i
++;
branchlabels
.
set
(
i
,
n
.
getNodeInfo
().
getBranchLabel
());
}
...
...
@@ -512,5 +530,91 @@ public class ProofTree extends BorderPane {
return
branchlabels
;
}
public
void
showScriptTree
()
{
if
(
main
.
getModel
().
getDebuggerFramework
().
getPtreeManager
()
==
null
)
{
Utils
.
showInfoDialog
(
"Execute Script"
,
"Execute Script"
,
"Please execute a script first."
);
return
;
}
treeScriptCreation
=
new
TreeTransformationScript
(
main
.
getModel
().
getDebuggerFramework
().
getPtreeManager
());
if
(
root
!=
null
)
{
//TODO not sure prooftree for what
TreeItem
<
TreeNode
>
tree
=
treeScriptCreation
.
create
(
proof
.
get
());
treeScript
.
setRoot
(
treeScriptCreation
.
buildScriptTree
(
root
.
get
()));
treeScript
.
refresh
();
}
}
private
TreeItem
<
TreeNode
>
buildScriptTree
(
Node
node
)
{
TreeItem
<
TreeNode
>
currentItem
=
new
TreeItem
<>(
createTreeNode
(
node
));
if
(
node
==
null
||
currentItem
.
getValue
()
==
null
)
{
return
null
;
}
assert
node
.
childrenCount
()
>=
0
;
if
(
sentinels
.
contains
(
node
))
{
return
currentItem
;
}
if
(
node
.
childrenCount
()
==
0
)
{
// TreeItem<TreeNode> e = new TreeItem<>(new TreeNode(
// n.isClosed() ? "CLOSED GOAL" : "OPEN GOAL", null));
// currentItem.getChildren().addCell(e);
return
currentItem
;
}
//no branchlabel needed
if
(
node
.
childrenCount
()
==
1
)
{
//check if same mutator as child
Node
child
=
node
.
child
(
0
);
if
(!
entryExitMap
.
get
(
node
).
contains
(
child
))
{
currentItem
.
getChildren
().
add
(
buildScriptTree
(
child
));
return
currentItem
;
}
else
{
//skip node
return
buildScriptTree
(
child
);
}
}
//node.childrenCount() > 1
//branch labels
Iterator
<
Node
>
iterator
=
node
.
childrenIterator
();
int
counter
=
0
;
while
(
iterator
.
hasNext
())
{
Node
child
=
iterator
.
next
();
String
branchlabel
=
"BRANCH "
+
counter
;
//TODO:getBranchLabels(child).get(0);
currentItem
.
getChildren
().
add
(
counter
,
new
TreeItem
<>(
new
TreeNode
(
branchlabel
,
child
)));
currentItem
.
getChildren
().
get
(
counter
).
getChildren
().
add
(
buildScriptTree
(
child
.
child
(
0
)));
counter
++;
}
return
currentItem
;
}
public
TreeNode
createTreeNode
(
Node
node
)
{
try
{
//TODO stupid hack for now
return
new
TreeNode
(
node
.
getAppliedRuleApp
().
rule
().
name
()
+
" (line TODO)"
,
node
);
}
catch
(
NullPointerException
e
)
{
System
.
out
.
println
(
node
);
e
.
printStackTrace
();
return
null
;
}
}
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTreeContextMenu.java
View file @
7fbd75b5
...
...
@@ -24,6 +24,11 @@ public class ProofTreeContextMenu extends javafx.scene.control.ContextMenu {
MenuItem
showSequent
=
new
MenuItem
(
"Show Sequent"
);
MenuItem
showGoal
=
new
MenuItem
(
"Show in Goal List"
);
MenuItem
expandAllNodes
=
new
MenuItem
(
"Expand Tree"
);
MenuItem
showScriptTree
=
new
MenuItem
(
"Show ScriptTree"
);
//TODO: zum Testen
private
ProofTree
proofTree
;
public
ProofTreeContextMenu
(
ProofTree
proofTree
)
{
...
...
@@ -83,7 +88,8 @@ public class ProofTreeContextMenu extends javafx.scene.control.ContextMenu {
proofTree
.
expandRootToLeaves
(
proofTree
.
getTreeProof
().
getRoot
());
});
getItems
().
setAll
(
refresh
,
expandAllNodes
,
new
SeparatorMenuItem
(),
copy
,
createCases
,
showSequent
,
showGoal
);
showScriptTree
.
setOnAction
(
event
->
proofTree
.
getTreeScriptCreation
().
showScriptTree
());
getItems
().
setAll
(
refresh
,
expandAllNodes
,
new
SeparatorMenuItem
(),
copy
,
createCases
,
showSequent
,
showGoal
,
showScriptTree
);
setAutoFix
(
true
);
setAutoHide
(
true
);
}
...
...
ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.fxml
View file @
7fbd75b5
...
...
@@ -3,9 +3,14 @@
<?import javafx.scene.control.TreeView?>
<?import javafx.scene.layout.BorderPane?>
<fx:root
type=
"javafx.scene.layout.BorderPane"
xmlns:fx=
"http://javafx.com/fxml/1"
fx:id=
"rootPane"
xmlns=
"http://javafx.com/javafx/8.0.112"
>
<
center
>
<
left
>
<TreeView
fx:id=
"treeProof"
editable=
"false"
>
</TreeView>
</center>
</left>
<right>
<TreeView
fx:id=
"treeScript"
editable=
"false"
>
</TreeView>
</right>
</fx:root>
\ No newline at end of file
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