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
03be4306
Commit
03be4306
authored
Jan 31, 2018
by
Sarah Grebing
Browse files
minor bugfix concerning services
parent
2bbd89d2
Pipeline
#17628
failed with stages
Changes
10
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java
View file @
03be4306
...
...
@@ -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 @
03be4306
...
...
@@ -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 @
03be4306
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 @
03be4306
...
...
@@ -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 @
03be4306
...
...
@@ -55,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
;
...
...
@@ -151,19 +152,6 @@ public class InteractiveModeController {
String
sfTerm
=
LogicPrinter
.
quickPrintTerm
(
seqForm
.
formula
(),
keYServices
,
false
,
false
);
String
onTerm
=
LogicPrinter
.
quickPrintTerm
(
tap
.
getPio
().
subTerm
(),
keYServices
,
false
,
false
);
//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);
/*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
();
...
...
@@ -174,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
));
...
...
@@ -297,6 +284,8 @@ public class InteractiveModeController {
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
()));
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/JavaArea.java
View file @
03be4306
...
...
@@ -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 @
03be4306
...
...
@@ -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 @
03be4306
...
...
@@ -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 @
03be4306
...
...
@@ -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 @
03be4306
...
...
@@ -2,7 +2,7 @@
//
script autoScript(){
auto;
//
auto;
}
script interactive(){
...
...
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