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
7924590f
Commit
7924590f
authored
Jan 31, 2018
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Plain Diff
Merge remote-tracking branch 'origin/master'
parents
02be8c3b
5064f230
Pipeline
#17631
canceled with stages
Changes
10
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
10 changed files
with
126 additions
and
105 deletions
+126
-105
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java
...java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java
+12
-11
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html
...ources/edu/kit/iti/formal/psdbg/commands/instantiate.html
+1
-0
ui/src/main/java/edu/kit/iti/formal/psdbg/examples/lulu/bigIntProof/BigIntExample.java
...formal/psdbg/examples/lulu/bigIntProof/BigIntExample.java
+4
-2
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
...edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
+62
-55
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java
...ormal/psdbg/gui/controller/InteractiveModeController.java
+35
-30
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/JavaArea.java
.../java/edu/kit/iti/formal/psdbg/gui/controls/JavaArea.java
+6
-4
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java
.../kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java
+0
-1
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java
...a/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java
+3
-0
ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example
...TA-INF/services/edu.kit.iti.formal.psdbg.examples.Example
+2
-1
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
...u/kit/iti/formal/psdbg/examples/contraposition/script.kps
+1
-1
No files found.
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java
View file @
7924590f
...
...
@@ -160,16 +160,6 @@ public class KeYMatcher implements MatcherApi<KeyData> {
return
assignments
.
isEmpty
()?
null
:
assignments
;
}
private
Value
<
String
>
toValueTerm
(
KeyData
currentState
,
Term
matched
)
{
String
reprTerm
=
LogicPrinter
.
quickPrintTerm
(
matched
,
currentState
.
getEnv
().
getServices
());
//Hack: to avoid newlines
String
reprTermReformatted
=
reprTerm
.
trim
();
return
new
Value
<>(
new
TermType
(
new
SortType
(
matched
.
sort
())),
reprTermReformatted
);
}
@Override
public
List
<
VariableAssignment
>
matchSeq
(
GoalNode
<
KeyData
>
currentState
,
String
data
,
...
...
@@ -178,7 +168,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
//System.out.println("Signature " + sig.toString());
Matchings
m
=
MatcherFacade
.
matches
(
data
,
currentState
.
getData
().
getNode
().
sequent
(),
false
,
s
ervices
);
currentState
.
getData
().
getNode
().
sequent
(),
false
,
currentState
.
getData
().
getProof
().
getS
ervices
()
);
if
(
m
.
isEmpty
())
{
LOGGER
.
debug
(
"currentState has no match= "
+
currentState
.
getData
().
getNode
().
sequent
());
...
...
@@ -208,6 +198,17 @@ public class KeYMatcher implements MatcherApi<KeyData> {
}
}
private
Value
<
String
>
toValueTerm
(
KeyData
currentState
,
Term
matched
)
{
String
reprTerm
=
LogicPrinter
.
quickPrintTerm
(
matched
,
currentState
.
getProof
().
getServices
());
//Hack: to avoid newlines
String
reprTermReformatted
=
reprTerm
.
trim
();
return
new
Value
<>(
new
TermType
(
new
SortType
(
matched
.
sort
())),
reprTermReformatted
);
}
//private TermLiteral from(SequentFormula sf) {
// return new TermLiteral(sf.toString());
...
...
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html
View file @
7924590f
...
...
@@ -16,5 +16,6 @@
<li><code>
occ
</code>
:
<em>
INT
</em>
occurence of the top-level formula
</li>
<li><code>
with
</code>
:
<em>
TERM
</em>
the term with which variables should be instantiated
</li>
</ul>
</body>
</html>
\ No newline at end of file
ui/src/main/java/edu/kit/iti/formal/psdbg/examples/lulu/bigIntProof/BigIntExample.java
View file @
7924590f
package
edu.kit.iti.formal.psdbg.examples.lulu.bigIntProof
;
import
edu.kit.iti.formal.psdbg.examples.
Java
Example
;
import
edu.kit.iti.formal.psdbg.examples.Example
;
public
class
BigIntExample
extends
Java
Example
{
public
class
BigIntExample
extends
Example
{
public
BigIntExample
()
{
setName
(
"BigInt"
);
defaultInit
(
getClass
());
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @
7924590f
...
...
@@ -428,31 +428,50 @@ public class DebuggerMain implements Initializable {
executeScript
(
FACADE
.
buildInterpreter
(),
addInitBreakpoint
);
}
/**
* Reload a problem from the beginning
*
* @param event
*/
@FXML
public
void
abortExecution
()
{
if
(
model
.
getDebuggerFramework
()
!=
null
)
{
try
{
// try to friendly
Future
future
=
executorService
.
submit
(()
->
{
model
.
getDebuggerFramework
().
stop
();
model
.
getDebuggerFramework
().
unregister
();
model
.
getDebuggerFramework
().
release
();
});
public
void
reloadProblem
(
ActionEvent
event
)
{
//abort current execution();
//save old information and refresh models
statusBar
.
publishMessage
(
"Reloading..."
);
File
lastLoaded
;
if
(
model
.
getKeyFile
()
!=
null
)
{
lastLoaded
=
model
.
getKeyFile
();
}
else
{
Contract
chosen
=
model
.
getChosenContract
();
lastLoaded
=
model
.
getJavaFile
();
}
//model.reload();
abortExecution
();
handleStatePointerUI
(
null
);
model
.
setStatePointer
(
null
);
//reload getInspectionViewsController().getActiveInspectionViewTab().getModel()
InspectionModel
iModel
=
getInspectionViewsController
().
getActiveInspectionViewTab
().
getModel
();
//iModel.setHighlightedJavaLines(FXCollections.emptyObservableSet());
iModel
.
clearHighlightLines
();
iModel
.
getGoals
().
clear
();
iModel
.
setSelectedGoalNodeToShow
(
null
);
// wait a second!
future
.
get
(
1
,
TimeUnit
.
SECONDS
);
// urgently stop
model
.
getDebuggerFramework
().
hardStop
();
}
catch
(
InterruptedException
|
ExecutionException
|
TimeoutException
e
)
{
e
.
printStackTrace
();
}
finally
{
model
.
setDebuggerFramework
(
null
);
try
{
FACADE
.
reload
(
lastLoaded
);
if
(
iModel
.
getGoals
().
size
()
>
0
)
{
iModel
.
setSelectedGoalNodeToShow
(
iModel
.
getGoals
().
get
(
0
));
}
}
else
{
LOGGER
.
info
(
"no interpreter running"
);
if
(
FACADE
.
getReadyToExecute
())
{
LOGGER
.
info
(
"Reloaded Successfully"
);
statusBar
.
publishMessage
(
"Reloaded Sucessfully"
);
}
}
catch
(
ProofInputException
e
)
{
e
.
printStackTrace
();
}
catch
(
ProblemLoaderException
e
)
{
e
.
printStackTrace
();
}
assert
model
.
getDebuggerFramework
()
==
null
;
}
@FXML
...
...
@@ -768,44 +787,32 @@ public class DebuggerMain implements Initializable {
}
}
/**
* Reload a problem from the beginning
*
* @param event
*/
@FXML
public
void
reloadProblem
(
ActionEvent
event
)
{
//abort current execution();
//save old information and refresh models
File
lastLoaded
;
if
(
model
.
getKeyFile
()
!=
null
)
{
lastLoaded
=
model
.
getKeyFile
();
}
else
{
Contract
chosen
=
model
.
getChosenContract
();
lastLoaded
=
model
.
getJavaFile
();
}
//model.reload();
abortExecution
();
handleStatePointerUI
(
null
);
model
.
setStatePointer
(
null
);
//reload getInspectionViewsController().getActiveInspectionViewTab().getModel()
InspectionModel
iModel
=
getInspectionViewsController
().
getActiveInspectionViewTab
().
getModel
();
iModel
.
setHighlightedJavaLines
(
null
);
iModel
.
getGoals
().
clear
();
iModel
.
setSelectedGoalNodeToShow
(
null
);
public
void
abortExecution
()
{
statusBar
.
publishMessage
(
"Aborting Execution..."
);
if
(
model
.
getDebuggerFramework
()
!=
null
)
{
try
{
// try to friendly
Future
future
=
executorService
.
submit
(()
->
{
model
.
getDebuggerFramework
().
stop
();
model
.
getDebuggerFramework
().
unregister
();
model
.
getDebuggerFramework
().
release
();
});
try
{
FACADE
.
reload
(
lastLoaded
);
if
(
iModel
.
getGoals
().
size
()
>
0
)
{
iModel
.
setSelectedGoalNodeToShow
(
iModel
.
getGoals
().
get
(
0
));
// wait a second!
future
.
get
(
1
,
TimeUnit
.
SECONDS
);
// urgently stop
model
.
getDebuggerFramework
().
hardStop
();
}
catch
(
InterruptedException
|
ExecutionException
|
TimeoutException
e
)
{
e
.
printStackTrace
();
}
finally
{
model
.
setDebuggerFramework
(
null
);
statusBar
.
publishMessage
(
"Execution aborted."
);
}
}
catch
(
ProofInputException
e
)
{
e
.
printStackTrace
();
}
catch
(
ProblemLoaderException
e
)
{
e
.
printStackTrace
();
}
else
{
LOGGER
.
info
(
"no interpreter running"
);
}
assert
model
.
getDebuggerFramework
()
==
null
;
}
@FXML
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java
View file @
7924590f
...
...
@@ -9,6 +9,7 @@ import de.uka.ilkd.key.logic.SequentFormula;
import
de.uka.ilkd.key.macros.scripts.EngineState
;
import
de.uka.ilkd.key.macros.scripts.RuleCommand
;
import
de.uka.ilkd.key.macros.scripts.ScriptException
;
import
de.uka.ilkd.key.pp.LogicPrinter
;
import
de.uka.ilkd.key.proof.Goal
;
import
de.uka.ilkd.key.proof.Node
;
import
de.uka.ilkd.key.proof.Proof
;
...
...
@@ -54,6 +55,7 @@ public class InteractiveModeController {
private
static
final
Logger
LOGGER
=
LogManager
.
getLogger
(
InteractiveModeController
.
class
);
private
final
Map
<
Node
,
Statements
>
cases
=
new
HashMap
<>();
private
final
ScriptController
scriptController
;
private
BooleanProperty
activated
=
new
SimpleBooleanProperty
();
private
ScriptArea
scriptArea
;
...
...
@@ -147,19 +149,9 @@ public class InteractiveModeController {
SequentFormula
seqForm
=
tap
.
getPio
().
sequentFormula
();
//transform term to parsable string representation
Sequent
seq
=
g
.
sequent
();
String
sfTerm
=
edu
.
kit
.
iti
.
formal
.
psdbg
.
termmatcher
.
Utils
.
toPrettyTerm
(
seqForm
.
formula
());
String
onTerm
=
edu
.
kit
.
iti
.
formal
.
psdbg
.
termmatcher
.
Utils
.
toPrettyTerm
(
tap
.
getPio
().
subTerm
());
//check whether more than one possibility for match
//Matchings matches = MatcherFacade.matches(term, seq, true, keYServices);
String
sfTerm
=
LogicPrinter
.
quickPrintTerm
(
seqForm
.
formula
(),
keYServices
,
false
,
false
);
String
onTerm
=
LogicPrinter
.
quickPrintTerm
(
tap
.
getPio
().
subTerm
(),
keYServices
,
false
,
false
);
/*Parameters params = new Parameters();
params.put(new Variable("formula"), new TermLiteral(term));
if (matches.size() > 1) {
moreThanOneMatch = true;
params.put(new Variable("occ"), new StringLiteral("0"));
}*/
RuleCommand
.
Parameters
params
=
new
RuleCommand
.
Parameters
();
params
.
formula
=
seqForm
.
formula
();
...
...
@@ -170,7 +162,6 @@ public class InteractiveModeController {
int
occ
=
rch
.
getOccurence
(
tap
.
getApp
());
Parameters
callp
=
new
Parameters
();
// callp.put(new Variable("formula"), new TermLiteral(sfTerm));
callp
.
put
(
new
Variable
(
"formula"
),
new
TermLiteral
(
sfTerm
));
callp
.
put
(
new
Variable
(
"occ"
),
new
IntegerLiteral
(
BigInteger
.
valueOf
(
occ
)));
callp
.
put
(
new
Variable
(
"on"
),
new
TermLiteral
(
onTerm
));
...
...
@@ -191,8 +182,8 @@ public class InteractiveModeController {
applyRule
(
call
,
g
);
// Insert into the right cases
Node
currentNode
=
g
.
node
();
cases
.
get
(
findRoot
(
currentNode
)).
add
(
call
);
//
Node currentNode = g.node();
//
cases.get(findRoot(currentNode)).add(call);
// How to Play this on the Proof?
// How to Build a new StatePointer? Is it still possible?
...
...
@@ -245,18 +236,6 @@ public class InteractiveModeController {
return
pp
.
toString
();
}
private
String
format
(
String
branchingLabel
)
{
System
.
out
.
println
(
"branchingLabel = "
+
branchingLabel
);
String
newLabel
=
branchingLabel
;
if
(
branchingLabel
.
endsWith
(
"$$"
))
{
newLabel
=
branchingLabel
.
substring
(
0
,
branchingLabel
.
length
()
-
2
);
newLabel
+=
".*"
;
System
.
out
.
println
(
"newLabel = "
+
newLabel
);
}
return
newLabel
;
}
private
void
applyRule
(
CallStatement
call
,
Goal
g
)
throws
ScriptCommandNotApplicableException
{
savepointslist
.
add
(
g
.
node
());
savepointsstatement
.
add
(
call
);
...
...
@@ -297,13 +276,28 @@ public class InteractiveModeController {
AbstractUserInterfaceControl
uiControl
=
new
DefaultUserInterfaceControl
();
c
.
execute
(
uiControl
,
cc
,
estate
);
ImmutableList
<
Goal
>
ngoals
=
g
.
proof
().
getSubtreeGoals
(
g
.
n
ode
());
ImmutableList
<
Goal
>
ngoals
=
g
.
proof
().
getSubtreeGoals
(
expandedNode
.
getData
().
getN
ode
());
goals
.
remove
(
expandedNode
);
GoalNode
<
KeyData
>
last
=
null
;
for
(
Goal
newGoalNode
:
ngoals
)
{
KeyData
kdn
=
new
KeyData
(
kd
,
newGoalNode
.
node
());
if
(
ngoals
.
size
()
>
1
)
{
cases
.
get
(
findRoot
(
ngoals
.
get
(
0
).
node
())).
add
(
call
);
cases
.
get
(
findRoot
(
ngoals
.
get
(
0
).
node
())).
add
(
new
CasesStatement
());
for
(
Goal
newGoalNode
:
ngoals
)
{
KeyData
kdn
=
new
KeyData
(
kd
,
newGoalNode
.
node
());
goals
.
add
(
last
=
new
GoalNode
<>(
expandedNode
,
kdn
,
kdn
.
getNode
().
isClosed
()));
cases
.
put
(
last
.
getData
().
getNode
(),
new
Statements
());
}
}
else
{
KeyData
kdn
=
new
KeyData
(
kd
,
ngoals
.
get
(
0
).
node
());
goals
.
add
(
last
=
new
GoalNode
<>(
expandedNode
,
kdn
,
kdn
.
getNode
().
isClosed
()));
Node
currentNode
=
last
.
getData
().
getNode
();
cases
.
get
(
findRoot
(
currentNode
)).
add
(
call
);
}
if
(
last
!=
null
)
model
.
setSelectedGoalNodeToShow
(
last
);
...
...
@@ -319,6 +313,17 @@ public class InteractiveModeController {
}
private
String
format
(
String
branchingLabel
)
{
// System.out.println("branchingLabel = " + branchingLabel);
String
newLabel
=
branchingLabel
;
if
(
branchingLabel
.
endsWith
(
"$$"
))
{
newLabel
=
branchingLabel
.
substring
(
0
,
branchingLabel
.
length
()
-
2
);
newLabel
+=
".*"
;
// System.out.println("newLabel = " + newLabel);
}
return
newLabel
;
}
public
boolean
isActivated
()
{
return
activated
.
get
();
}
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/JavaArea.java
View file @
7924590f
...
...
@@ -56,10 +56,12 @@ public class JavaArea extends BaseCodeArea {
* highlight new lines
*/
private
void
highlightLineSet
()
{
linesToHighlightProperty
().
get
().
forEach
(
integer
->
{
lineToClassProperty
().
get
().
put
(
integer
-
1
,
"line-highlight"
);
});
highlightLines
();
if
(!
linesToHighlight
.
get
().
isEmpty
())
{
linesToHighlightProperty
().
get
().
forEach
(
integer
->
{
lineToClassProperty
().
get
().
put
(
integer
-
1
,
"line-highlight"
);
});
highlightLines
();
}
}
private
void
updateView
()
{
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java
View file @
7924590f
...
...
@@ -119,7 +119,6 @@ public class TacletContextMenu extends ContextMenu {
try
{
ImmutableList
<
TacletApp
>
findTaclet
=
c
.
getFindTaclet
(
goal
,
occ
);
createTacletMenu
(
removeRewrites
(
findTaclet
)
.
prepend
(
c
.
getRewriteTaclet
(
goal
,
occ
)),
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java
View file @
7924590f
...
...
@@ -162,6 +162,9 @@ public class InspectionModel {
return
isInterpreterTab
;
}
public
void
clearHighlightLines
()
{
highlightedJavaLinesProperty
().
clear
();
}
enum
Mode
{
LIVING
,
DEAD
,
POSTMORTEM
,
...
...
ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example
View file @
7924590f
...
...
@@ -9,4 +9,5 @@ edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample
edu.kit.iti.formal.psdbg.examples.java.sumAndMax.SumAndMaxExample
edu.kit.iti.formal.psdbg.examples.lulu.LuLuDoubleLinkedList
edu.kit.iti.formal.psdbg.examples.lulu.LuLuQuickSort
edu.kit.iti.formal.psdbg.examples.lulu.LuLuSumAndMax
\ No newline at end of file
edu.kit.iti.formal.psdbg.examples.lulu.LuLuSumAndMax
#edu.kit.iti.formal.psdbg.examples.lulu.bigIntProof.BigIntExample
\ No newline at end of file
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
View file @
7924590f
...
...
@@ -2,7 +2,7 @@
//
script autoScript(){
auto;
//
auto;
}
script interactive(){
...
...
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