Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
P
ProofScriptParser
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
24
Issues
24
List
Boards
Labels
Service Desk
Milestones
Merge Requests
4
Merge Requests
4
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
sarah.grebing
ProofScriptParser
Commits
6019bbae
Commit
6019bbae
authored
Oct 15, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
interim
parent
0e8cb6d1
Changes
5
Show whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
79 additions
and
1 deletion
+79
-1
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/InterpreterExtendedState.java
...rmal/psdbg/interpreter/data/InterpreterExtendedState.java
+46
-0
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
...du/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
+15
-0
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
...ti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
+1
-1
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java
...a/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java
+5
-0
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
...u/kit/iti/formal/psdbg/examples/contraposition/script.kps
+12
-0
No files found.
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/InterpreterExtendedState.java
0 → 100644
View file @
6019bbae
package
edu.kit.iti.formal.psdbg.interpreter.data
;
import
edu.kit.iti.formal.psdbg.parser.ast.CaseStatement
;
import
java.util.*
;
import
java.util.stream.Collectors
;
public
class
InterpreterExtendedState
<
T
>
extends
State
<
T
>
{
private
Map
<
CaseStatement
,
List
<
GoalNode
<
T
>>>
mappingOfCaseToStates
=
new
HashMap
<>();
public
InterpreterExtendedState
(
Collection
<
GoalNode
<
T
>>
goals
,
GoalNode
selected
)
{
super
(
goals
,
selected
);
}
public
InterpreterExtendedState
(
Collection
<
GoalNode
<
T
>>
goals
,
GoalNode
selected
,
Map
<
CaseStatement
,
List
<
GoalNode
<
T
>>>
casesMapping
)
{
super
(
goals
,
selected
);
this
.
mappingOfCaseToStates
=
casesMapping
;
}
public
Map
<
CaseStatement
,
List
<
GoalNode
<
T
>>>
getMappingOfCaseToStates
()
{
return
mappingOfCaseToStates
;
}
public
void
setMappingOfCaseToStates
(
Map
<
CaseStatement
,
List
<
GoalNode
<
T
>>>
mappingOfCaseToStates
)
{
this
.
mappingOfCaseToStates
=
mappingOfCaseToStates
;
}
public
List
<
GoalNode
<
T
>>
getClosedNodes
()
{
return
super
.
getGoals
().
stream
().
filter
(
nodes
->
nodes
.
isClosed
()).
collect
(
Collectors
.
toList
());
}
public
List
<
GoalNode
<
T
>>
getopenNodes
()
{
return
super
.
getGoals
().
stream
().
filter
(
nodes
->
!
nodes
.
isClosed
()).
collect
(
Collectors
.
toList
());
}
public
List
<
GoalNode
<
T
>>
getActiveGoalsForCase
(
CaseStatement
caseStmt
)
{
return
mappingOfCaseToStates
.
getOrDefault
(
caseStmt
,
Collections
.
emptyList
());
}
//getuserSelected/
//verfuegbar im case
//map<case, listgoal>
//regel anwendbar oder nicht
}
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java
View file @
6019bbae
package
edu.kit.iti.formal.psdbg.interpreter.graphs
;
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.interpreter.data.State
;
import
edu.kit.iti.formal.psdbg.parser.ast.ASTNode
;
import
edu.kit.iti.formal.psdbg.parser.ast.ASTNode
;
import
edu.kit.iti.formal.psdbg.parser.ast.CaseStatement
;
import
java.util.LinkedList
;
import
java.util.LinkedList
;
...
@@ -15,6 +17,8 @@ public class PTreeNode<T> {
...
@@ -15,6 +17,8 @@ public class PTreeNode<T> {
*/
*/
private
State
<
T
>
state
;
private
State
<
T
>
state
;
private
InterpreterExtendedState
<
T
>
extendedState
;
/**
/**
* Statement
* Statement
*/
*/
...
@@ -58,6 +62,17 @@ public class PTreeNode<T> {
...
@@ -58,6 +62,17 @@ public class PTreeNode<T> {
this
.
context
=
context
;
this
.
context
=
context
;
}
}
public
InterpreterExtendedState
<
T
>
getExtendedState
()
{
return
extendedState
;
}
public
void
setExtendedState
(
State
<
T
>
state
)
{
this
.
extendedState
=
new
InterpreterExtendedState
<>(
state
.
getGoals
(),
state
.
getSelectedGoalNode
());
if
(
getScriptstmt
()
instanceof
CaseStatement
)
{
}
}
public
String
toString
()
{
public
String
toString
()
{
StringBuilder
sb
=
new
StringBuilder
();
StringBuilder
sb
=
new
StringBuilder
();
sb
.
append
(
"Node {"
);
sb
.
append
(
"Node {"
);
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
View file @
6019bbae
...
@@ -200,8 +200,8 @@ public class StateGraphWrapper<T> {
...
@@ -200,8 +200,8 @@ public class StateGraphWrapper<T> {
public
Void
addState
(
ASTNode
node
)
{
public
Void
addState
(
ASTNode
node
)
{
PTreeNode
newStateNode
=
addedNodes
.
get
(
node
);
PTreeNode
newStateNode
=
addedNodes
.
get
(
node
);
State
<
T
>
currentState
=
currentInterpreter
.
getCurrentState
().
copy
();
State
<
T
>
currentState
=
currentInterpreter
.
getCurrentState
().
copy
();
newStateNode
.
setState
(
currentState
);
newStateNode
.
setState
(
currentState
);
newStateNode
.
setExtendedState
(
currentState
);
return
null
;
return
null
;
}
}
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java
View file @
6019bbae
...
@@ -17,10 +17,15 @@ import javafx.scene.paint.Color;
...
@@ -17,10 +17,15 @@ import javafx.scene.paint.Color;
* @author Alexander Weigl
* @author Alexander Weigl
*/
*/
public
class
InspectionModel
{
public
class
InspectionModel
{
private
final
ObjectProperty
<
ASTNode
>
node
=
new
SimpleObjectProperty
<>(
this
,
"node"
);
private
final
ObjectProperty
<
ASTNode
>
node
=
new
SimpleObjectProperty
<>(
this
,
"node"
);
//alle aktuellen nicht geschlossene Ziele -> alle leaves später (open+closed)
private
final
ListProperty
<
GoalNode
<
KeyData
>>
goals
=
new
SimpleListProperty
<>(
this
,
"goals"
);
private
final
ListProperty
<
GoalNode
<
KeyData
>>
goals
=
new
SimpleListProperty
<>(
this
,
"goals"
);
//sicht user selected
private
final
ObjectProperty
<
GoalNode
<
KeyData
>>
selectedGoalNodeToShow
=
new
SimpleObjectProperty
<>(
this
,
"selectedGoalNodeToShow"
);
private
final
ObjectProperty
<
GoalNode
<
KeyData
>>
selectedGoalNodeToShow
=
new
SimpleObjectProperty
<>(
this
,
"selectedGoalNodeToShow"
);
//aktuell im Interpreter aktives Goal
private
final
ObjectProperty
<
GoalNode
<
KeyData
>>
currentInterpreterGoal
=
new
SimpleObjectProperty
<>(
this
,
"currentInterpreterGoal"
);
private
final
ObjectProperty
<
GoalNode
<
KeyData
>>
currentInterpreterGoal
=
new
SimpleObjectProperty
<>(
this
,
"currentInterpreterGoal"
);
private
final
MapProperty
<
GoalNode
,
Color
>
colorofEachGoalNodeinListView
=
new
SimpleMapProperty
<>(
FXCollections
.
observableHashMap
());
private
final
MapProperty
<
GoalNode
,
Color
>
colorofEachGoalNodeinListView
=
new
SimpleMapProperty
<>(
FXCollections
.
observableHashMap
());
//private final StringProperty javaString = new SimpleStringProperty();
//private final StringProperty javaString = new SimpleStringProperty();
private
final
SetProperty
<
Integer
>
highlightedJavaLines
=
new
SimpleSetProperty
<>(
FXCollections
.
observableSet
(),
"highlightedJavaLines"
);
private
final
SetProperty
<
Integer
>
highlightedJavaLines
=
new
SimpleSetProperty
<>(
FXCollections
.
observableSet
(),
"highlightedJavaLines"
);
...
...
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
View file @
6019bbae
// Please select one of the following scripts.
// Please select one of the following scripts.
//
//
script test2(){
impRight;
impLeft;
cases{
case match `q==> `:
impRight;
default:
impRight;
notRight;
}
script test(){
script test(){
}
}
...
...
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