Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
4197f43b
Commit
4197f43b
authored
Oct 27, 2017
by
Sarah Grebing
Browse files
interim state for stategraphwrapper and cfg
parent
2577adfe
Pipeline
#14968
failed with stage
in 1 minute and 55 seconds
Changes
14
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java
View file @
4197f43b
...
...
@@ -25,6 +25,7 @@ package edu.kit.iti.formal.psdbg.parser.ast;
import
edu.kit.iti.formal.psdbg.parser.Visitable
;
import
edu.kit.iti.formal.psdbg.parser.Visitor
;
import
lombok.EqualsAndHashCode
;
import
lombok.Getter
;
import
org.antlr.v4.runtime.ParserRuleContext
;
...
...
@@ -32,6 +33,7 @@ import org.antlr.v4.runtime.ParserRuleContext;
* @author Alexander Weigl
* @version 1 (27.04.17)
*/
@EqualsAndHashCode
public
abstract
class
ASTNode
<
T
extends
ParserRuleContext
>
implements
Visitable
,
Copyable
<
ASTNode
<
T
>>
{
/**
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/AssignmentStatement.java
View file @
4197f43b
...
...
@@ -36,11 +36,13 @@ import lombok.*;
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
@Data
@ToString
(
includeFieldNames
=
true
)
@NoArgsConstructor
@RequiredArgsConstructor
()
@AllArgsConstructor
@Getter
@Setter
public
class
AssignmentStatement
extends
Statement
<
ScriptLanguageParser
.
AssignmentContext
>
{
@NonNull
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/CallStatement.java
View file @
4197f43b
...
...
@@ -34,7 +34,8 @@ import lombok.*;
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
@Data
@Getter
@Setter
@NoArgsConstructor
@RequiredArgsConstructor
@AllArgsConstructor
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/CaseStatement.java
View file @
4197f43b
...
...
@@ -23,19 +23,20 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import
edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser
;
import
edu.kit.iti.formal.psdbg.parser.Visitor
;
import
lombok.AllArgsConstructor
;
import
lombok.Data
;
import
lombok.NoArgsConstructor
;
import
lombok.Getter
;
import
lombok.RequiredArgsConstructor
;
import
lombok.Setter
;
/**
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
@Data
@NoArgsConstructor
@Getter
@Setter
@RequiredArgsConstructor
@AllArgsConstructor
public
class
CaseStatement
extends
Statement
<
ScriptLanguageParser
.
CasesListContext
>
{
public
boolean
isClosedStmt
;
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/CasesStatement.java
View file @
4197f43b
...
...
@@ -23,11 +23,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import
edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser
;
import
edu.kit.iti.formal.psdbg.parser.Visitor
;
import
lombok.
Data
;
import
lombok.
Getter
;
import
lombok.NonNull
;
import
lombok.RequiredArgsConstructor
;
import
lombok.Setter
;
import
java.util.ArrayList
;
import
java.util.List
;
...
...
@@ -36,7 +37,9 @@ import java.util.List;
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
@Data
@Setter
@Getter
@RequiredArgsConstructor
public
class
CasesStatement
extends
Statement
<
ScriptLanguageParser
.
CasesStmtContext
>
{
@NonNull
private
final
List
<
CaseStatement
>
cases
=
new
ArrayList
<>();
// @NonNull private Statements defaultCase = new Statements();
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/DefaultCaseStatement.java
View file @
4197f43b
...
...
@@ -2,9 +2,11 @@ package edu.kit.iti.formal.psdbg.parser.ast;
import
edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser
;
import
edu.kit.iti.formal.psdbg.parser.Visitor
;
import
lombok.Data
;
import
lombok.Getter
;
import
lombok.Setter
;
@Data
@Getter
@Setter
public
class
DefaultCaseStatement
extends
Statement
<
ScriptLanguageParser
.
StmtListContext
>
{
protected
Statements
body
;
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ForeachStatement.java
View file @
4197f43b
...
...
@@ -23,16 +23,17 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import
edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser
;
import
edu.kit.iti.formal.psdbg.parser.Visitor
;
import
lombok.Data
;
import
lombok.Getter
;
import
lombok.Setter
;
/**
* @author Alexander Weigl
* @version 1 (29.04.17)
*/
@Data
@Getter
@Setter
public
class
ForeachStatement
extends
GoalSelector
<
ScriptLanguageParser
.
ForEachStmtContext
>
{
public
ForeachStatement
()
{
}
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/GoalSelector.java
View file @
4197f43b
...
...
@@ -31,7 +31,13 @@ import org.antlr.v4.runtime.ParserRuleContext;
* @author Alexander Weigl
* @version 1 (29.04.17)
*/
@Data
@AllArgsConstructor
@NoArgsConstructor
public
abstract
class
GoalSelector
<
T
extends
ParserRuleContext
>
@Getter
@Setter
@AllArgsConstructor
@NoArgsConstructor
public
abstract
class
GoalSelector
<
T
extends
ParserRuleContext
>
extends
Statement
<
T
>
{
@Getter
@Setter
@NonNull
private
Statements
body
=
new
Statements
();
}
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/RepeatStatement.java
View file @
4197f43b
...
...
@@ -23,16 +23,17 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import
edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser
;
import
edu.kit.iti.formal.psdbg.parser.Visitor
;
import
lombok.Data
;
import
lombok.Getter
;
import
lombok.Setter
;
/**
* @author Alexander Weigl
* @version 1 (29.04.17)
*/
@Data
@Getter
@Setter
public
class
RepeatStatement
extends
GoalSelector
<
ScriptLanguageParser
.
RepeatStmtContext
>
{
public
RepeatStatement
()
{
}
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java
View file @
4197f43b
...
...
@@ -23,11 +23,9 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import
edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser
;
import
edu.kit.iti.formal.psdbg.parser.Visitable
;
import
edu.kit.iti.formal.psdbg.parser.Visitor
;
import
lombok.EqualsAndHashCode
;
import
lombok.ToString
;
import
java.util.*
;
...
...
@@ -40,7 +38,6 @@ import java.util.stream.Stream;
* @author Alexander Weigl
* @version 1 (27.04.17)
*/
@EqualsAndHashCode
@ToString
public
class
Statements
extends
ASTNode
<
ScriptLanguageParser
.
StmtListContext
>
implements
Visitable
,
Iterable
<
Statement
>
{
...
...
@@ -182,4 +179,5 @@ public class Statements extends ASTNode<ScriptLanguageParser.StmtListContext>
s
.
setRuleContext
(
this
.
getRuleContext
());
return
s
;
}
}
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/TheOnlyStatement.java
View file @
4197f43b
...
...
@@ -23,16 +23,17 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import
edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser
;
import
edu.kit.iti.formal.psdbg.parser.Visitor
;
import
lombok.Data
;
import
lombok.Getter
;
import
lombok.Setter
;
/**
* @author Alexander Weigl
* @version 1 (29.04.17)
*/
@Data
@Getter
@Setter
public
class
TheOnlyStatement
extends
GoalSelector
<
ScriptLanguageParser
.
TheOnlyStmtContext
>
{
public
TheOnlyStatement
()
{
}
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/ControlFlowVisitor.java
View file @
4197f43b
...
...
@@ -7,6 +7,7 @@ import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup;
import
edu.kit.iti.formal.psdbg.interpreter.funchdl.ProofScriptHandler
;
import
edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor
;
import
edu.kit.iti.formal.psdbg.parser.ast.*
;
import
javafx.util.Pair
;
import
java.util.*
;
...
...
@@ -44,6 +45,12 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
mappingOfNodes
=
new
HashMap
<>();
}
/**
* Return all nodes that have the parameter node as target in the graph
*
* @param node
* @return
*/
public
Set
<
EndpointPair
<
ControlFlowNode
>>
getAllEdgesForNodeAsTarget
(
ASTNode
node
)
{
...
...
@@ -55,9 +62,9 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
if
(
e
.
target
().
equals
(
assocNode
))
{
edges
.
add
(
e
);
System
.
out
.
println
(
e
.
target
());
System
.
out
.
println
(
e
.
source
());
System
.
out
.
println
(
graph
.
edgeValue
(
e
.
target
(),
e
.
source
()));
//
System.out.println(e.target());
//
System.out.println(e.source());
//
System.out.println(graph.edgeValue(e.target(), e.source()));
}
});
return
edges
;
...
...
@@ -66,6 +73,54 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
}
}
public
Collection
<
Pair
<
ControlFlowNode
,
EdgeTypes
>>
getPredecessorsAndTheirEdges
(
ASTNode
node
)
{
ControlFlowNode
assocNode
=
getCorrespondingNode
(
node
);
List
<
Pair
<
ControlFlowNode
,
EdgeTypes
>>
allPreds
=
new
LinkedList
<>();
if
(
assocNode
!=
null
)
{
graph
.
edges
().
forEach
(
edge
->
{
if
(
edge
.
target
().
equals
(
assocNode
))
{
allPreds
.
add
(
new
Pair
(
edge
.
source
(),
edge
));
}
});
return
allPreds
;
}
else
{
return
Collections
.
EMPTY_LIST
;
}
}
public
ControlFlowNode
getCorrespondingNode
(
ASTNode
node
)
{
ControlFlowNode
ctrl
=
null
;
for
(
ASTNode
astNode
:
mappingOfNodes
.
keySet
())
{
if
(
astNode
.
getStartPosition
().
equals
(
node
.
getStartPosition
())
&&
astNode
.
getEndPosition
().
equals
(
node
.
getEndPosition
()))
{
ctrl
=
mappingOfNodes
.
get
(
astNode
);
break
;
}
}
return
ctrl
;
}
public
Collection
<
Pair
<
ControlFlowNode
,
EdgeTypes
>>
getPredecessorsAsTarget
(
ASTNode
node
)
{
ControlFlowNode
assocNode
=
getCorrespondingNode
(
node
);
List
<
Pair
<
ControlFlowNode
,
EdgeTypes
>>
allPreds
=
new
LinkedList
<>();
if
(
assocNode
!=
null
)
{
graph
.
edges
().
forEach
(
edge
->
{
if
(
edge
.
source
().
equals
(
assocNode
))
{
allPreds
.
add
(
new
Pair
(
edge
.
target
(),
edge
));
}
});
return
allPreds
;
}
else
{
return
Collections
.
EMPTY_LIST
;
}
}
@Override
public
Void
visit
(
ProofScript
proofScript
)
{
...
...
@@ -111,6 +166,7 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
}
mappingOfNodes
.
put
(
call
,
currentNode
);
graph
.
addNode
(
currentNode
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_BACK
);
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
View file @
4197f43b
...
...
@@ -14,6 +14,7 @@ import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import
edu.kit.iti.formal.psdbg.parser.ast.*
;
import
javafx.application.Platform
;
import
javafx.beans.property.SimpleObjectProperty
;
import
javafx.util.Pair
;
import
lombok.Getter
;
import
org.apache.logging.log4j.LogManager
;
import
org.apache.logging.log4j.Logger
;
...
...
@@ -260,7 +261,8 @@ public class StateGraphWrapper<T> {
});
extState
.
setMappingOfCaseToStates
(
mappingOfCaseToStates
);
//TODO default case
//TODO default case: missing datastructure of supertype CaseStatement at the moment
newStateNode
.
setState
(
lastState
.
copy
());
}
else
{
...
...
@@ -278,9 +280,25 @@ public class StateGraphWrapper<T> {
}
newStateNode
.
setExtendedState
(
extState
);
stateGraph
.
addNode
(
newStateNode
);
Collection
<
Pair
<
ControlFlowNode
,
EdgeTypes
>>
predecessorsAndTheirEdges
=
cfgVisitor
.
getPredecessorsAndTheirEdges
(
newStateNode
.
getScriptstmt
());
for
(
Pair
<
ControlFlowNode
,
EdgeTypes
>
predecessorsAndTheirEdge
:
predecessorsAndTheirEdges
)
{
if
(
predecessorsAndTheirEdge
.
getKey
().
equals
(
lastNode
.
getScriptstmt
()))
{
stateGraph
.
putEdgeValue
(
lastNode
,
newStateNode
,
predecessorsAndTheirEdge
.
getValue
());
}
}
Collection
<
Pair
<
ControlFlowNode
,
EdgeTypes
>>
predecessorsAsTarget
=
cfgVisitor
.
getPredecessorsAsTarget
(
node
);
for
(
Pair
<
ControlFlowNode
,
EdgeTypes
>
predecessorAsTarget
:
predecessorsAsTarget
)
{
if
(
predecessorAsTarget
.
getKey
().
equals
(
lastNode
.
getScriptstmt
()))
{
stateGraph
.
putEdgeValue
(
newStateNode
,
lastNode
,
predecessorAsTarget
.
getValue
());
}
}
stateGraph
.
putEdgeValue
(
lastNode
,
newStateNode
,
EdgeTypes
.
STATE_FLOW
);
//inform listeners about a new node in the graph
...
...
@@ -324,18 +342,17 @@ public class StateGraphWrapper<T> {
return
null
;
}
private
void
fire
Stat
eAdded
(
Stat
eAddedEvent
stat
eAddedEvent
)
{
private
void
fire
Nod
eAdded
(
Nod
eAddedEvent
nod
eAddedEvent
)
{
changeListeners
.
forEach
(
list
->
Platform
.
runLater
(()
->
{
list
.
graphChanged
(
stat
eAddedEvent
);
//
LOGGER.
debug
("New StateGraphChange " + this.asdot());
list
.
graphChanged
(
nod
eAddedEvent
);
LOGGER
.
info
(
"New StateGraphChange
\n
"
+
this
.
asdot
()
+
"\n"
);
}));
}
private
void
fire
Nod
eAdded
(
Nod
eAddedEvent
nod
eAddedEvent
)
{
private
void
fire
Stat
eAdded
(
Stat
eAddedEvent
stat
eAddedEvent
)
{
changeListeners
.
forEach
(
list
->
Platform
.
runLater
(()
->
{
list
.
graphChanged
(
nodeAddedEvent
);
//TODO
// LOGGER.info("New StateGraphChange \n%%%%%%" + this.asdot() + "\n%%%%%%%");
list
.
graphChanged
(
stateAddedEvent
);
LOGGER
.
debug
(
"New StateGraphChange "
+
this
.
asdot
());
}));
}
...
...
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
View file @
4197f43b
...
...
@@ -7,10 +7,15 @@ cases{
case match `q==>`:
impRight;
notRight;
case match `==>`:
impRight;
notRight;
close;
}
auto;
}
...
...
@@ -31,7 +36,7 @@ cases{
impRight;
}
}
script test2(){
impRight;
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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