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
45f9a7ad
Commit
45f9a7ad
authored
Oct 10, 2017
by
Sarah Grebing
Browse files
Added functionality that it is now possible to also step when already executed whole script
parent
ceaa63c1
Pipeline
#14460
failed with stage
in 3 minutes and 36 seconds
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @
45f9a7ad
...
...
@@ -145,7 +145,6 @@ public class DebuggerMain implements Initializable {
}
);
//Debugging
Utils
.
addDebugListener
(
javaCode
);
Utils
.
addDebugListener
(
executeNotPossible
,
"executeNotPossible"
);
...
...
@@ -203,9 +202,6 @@ public class DebuggerMain implements Initializable {
imodel
.
goalsProperty
().
addListener
((
observable
,
oldValue
,
newValue
)
->
statusBar
.
setNumberOfGoals
(
newValue
.
size
()));
/*proofTreeController.currentExecutionEndProperty().addListener((observable, oldValue, newValue) -> {
scriptController.getMainScript().getScriptArea().removeExecutionMarker();
LineMapping lm = new LineMapping(scriptController.getMainScript().getScriptArea().getText());
...
...
@@ -281,90 +277,21 @@ public class DebuggerMain implements Initializable {
}
/* public InspectionViewsController getInspectionViewsController() {
return inspectionViewsController;
}
public KeYProofFacade getFacade() {
return FACADE;
}
*/
//region Actions: Execution
/**
* When play button is used
*/
@FXML
public
void
executeScript
()
{
executorHelper
();
}
private
void
executorHelper
()
{
if
(
proofTreeController
.
isAlreadyExecuted
())
{
File
file
;
boolean
isKeyfile
=
false
;
if
(
getJavaFile
()
!=
null
)
{
file
=
getJavaFile
();
}
else
{
isKeyfile
=
true
;
file
=
getKeyFile
();
}
Task
<
Void
>
reloading
=
reloadEnvironment
(
file
,
isKeyfile
);
reloading
.
setOnSucceeded
(
event
->
{
statusBar
.
publishMessage
(
"Cleared and Reloaded Environment"
);
executeScript
(
FACADE
.
buildInterpreter
(),
false
);
});
reloading
.
setOnFailed
(
event
->
{
event
.
getSource
().
exceptionProperty
().
get
();
Utils
.
showExceptionDialog
(
"Loading Error"
,
"Could not clear Environment"
,
"There was an error when clearing old environment"
,
(
Throwable
)
event
.
getSource
().
exceptionProperty
().
get
()
);
});
ProgressBar
bar
=
new
ProgressBar
();
bar
.
progressProperty
().
bind
(
reloading
.
progressProperty
());
executorService
.
execute
(
reloading
);
}
else
{
executeScript
(
FACADE
.
buildInterpreter
(),
false
);
}
}
public
File
getJavaFile
()
{
return
javaFile
.
get
();
}
//region Actions: Menu
/* @FXML
public void closeProgram() {
System.exit(0);
}*/
/* @FXML
public void openScript() {
File scriptFile = openFileChooserOpenDialog("Select Script File",
"Proof Script File", "kps");
if (scriptFile != null) {
openScript(scriptFile);
}
}*/
/* private void saveScript(File scriptFile) {
try {
scriptController.saveCurrentScriptAs(scriptFile);
} catch (IOException e) {
Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save to file " + scriptFile.getName(), e);
}
}
@FXML
/*
@FXML
public void saveAsScript() throws IOException {
File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps");
if (f != null) {
...
...
@@ -375,17 +302,7 @@ public class DebuggerMain implements Initializable {
}
}*/
/* public void openScript(File scriptFile) {
assert scriptFile != null;
setInitialDirectory(scriptFile.getParentFile());
try {
String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset());
ScriptArea area = scriptController.createNewTab(scriptFile);
} catch (IOException e) {
Utils.showExceptionDialog("Exception occured", "",
"Could not load sourceName " + scriptFile, e);
}
}*/
public
void
setJavaFile
(
File
javaFile
)
{
this
.
javaFile
.
set
(
javaFile
);
...
...
@@ -423,20 +340,62 @@ public class DebuggerMain implements Initializable {
return
task
;
}
@FXML
public
void
executeScript
()
{
executorHelper
(
false
);
}
private
void
executorHelper
(
boolean
addInitBreakpoint
)
{
if
(
proofTreeController
.
isAlreadyExecuted
())
{
File
file
;
boolean
isKeyfile
=
false
;
if
(
getJavaFile
()
!=
null
)
{
file
=
getJavaFile
();
}
else
{
isKeyfile
=
true
;
file
=
getKeyFile
();
}
Task
<
Void
>
reloading
=
reloadEnvironment
(
file
,
isKeyfile
);
reloading
.
setOnSucceeded
(
event
->
{
statusBar
.
publishMessage
(
"Cleared and Reloaded Environment"
);
executeScript
(
FACADE
.
buildInterpreter
(),
addInitBreakpoint
);
});
reloading
.
setOnFailed
(
event
->
{
event
.
getSource
().
exceptionProperty
().
get
();
Utils
.
showExceptionDialog
(
"Loading Error"
,
"Could not clear Environment"
,
"There was an error when clearing old environment"
,
(
Throwable
)
event
.
getSource
().
exceptionProperty
().
get
()
);
});
ProgressBar
bar
=
new
ProgressBar
();
bar
.
progressProperty
().
bind
(
reloading
.
progressProperty
());
executorService
.
execute
(
reloading
);
}
else
{
executeScript
(
FACADE
.
buildInterpreter
(),
addInitBreakpoint
);
}
}
/**
* Execute the script that with using the interpreter that is build using the interpreterbuilder
*
* @param ib
* @param
debugMode
* @param
*/
private
void
executeScript
(
InterpreterBuilder
ib
,
boolean
debugMode
)
{
private
void
executeScript
(
InterpreterBuilder
ib
,
boolean
addInitBreakpoint
)
{
Set
<
Breakpoint
>
breakpoints
=
scriptController
.
getBreakpoints
();
if
(
proofTreeController
.
isAlreadyExecuted
())
{
proofTreeController
.
saveGraphs
();
}
this
.
debugMode
.
set
(
debugMode
);
this
.
debugMode
.
set
(
addInitBreakpoint
);
statusBar
.
publishMessage
(
"Parse ..."
);
try
{
...
...
@@ -460,6 +419,7 @@ public class DebuggerMain implements Initializable {
}
}
statusBar
.
publishMessage
(
"Creating new Interpreter instance ..."
);
ib
.
setScripts
(
scripts
);
KeyInterpreter
currentInterpreter
=
ib
.
build
();
...
...
@@ -468,7 +428,9 @@ public class DebuggerMain implements Initializable {
proofTreeController
.
setMainScript
(
scripts
.
get
(
n
));
statusBar
.
publishMessage
(
"Executing script "
+
scripts
.
get
(
n
).
getName
());
if
(
addInitBreakpoint
)
{
breakpoints
.
add
(
new
Breakpoint
(
scriptController
.
getMainScript
().
getScriptArea
().
getFilePath
(),
scriptController
.
getMainScript
().
getLineNumber
()));
}
proofTreeController
.
executeScript
(
this
.
debugMode
.
get
(),
statusBar
,
breakpoints
);
//highlight signature of main script
//scriptController.setDebugMark(scripts.get(0).getStartPosition().getLineNumber());
...
...
@@ -477,6 +439,22 @@ public class DebuggerMain implements Initializable {
}
}
@FXML
public
void
executeStepwise
()
{
executorHelper
(
true
);
//executeScript(FACADE.buildInterpreter(), true);
}
@FXML
public
void
executeToBreakpoint
()
{
Set
<
Breakpoint
>
breakpoints
=
scriptController
.
getBreakpoints
();
if
(
breakpoints
.
size
()
==
0
)
{
System
.
out
.
println
(
scriptController
.
mainScriptProperty
().
get
().
getLineNumber
());
//we need to add breakpoint at end if no breakpoint exists
}
executorHelper
(
false
);
}
public
void
openKeyFile
(
File
keyFile
)
{
if
(
keyFile
!=
null
)
{
setKeyFile
(
keyFile
);
...
...
@@ -510,41 +488,21 @@ public class DebuggerMain implements Initializable {
}
}
/* @FXML
protected void loadKeYFile() {
File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps");
openKeyFile(keyFile);
}
*/
@FXML
public
void
executeToBreakpoint
()
{
Set
<
Breakpoint
>
breakpoints
=
scriptController
.
getBreakpoints
();
if
(
breakpoints
.
size
()
==
0
)
{
//we need to add breakpoint at end if no breakpoint exists
}
executorHelper
();
protected
void
loadKeYFile
()
{
File
keyFile
=
openFileChooserOpenDialog
(
"Select KeY File"
,
"KeY Files"
,
"key"
,
"kps"
);
openKeyFile
(
keyFile
);
}
//endregion
//region Santa's Little Helper
@FXML
public
void
executeInDebugMode
()
{
executeScript
(
FACADE
.
buildInterpreter
(),
true
);
}
@FXML
public
void
saveScript
()
{
try
{
scriptController
.
saveCurrentScript
();
}
catch
(
IOException
e
)
{
Utils
.
showExceptionDialog
(
"Could not save file"
,
"Saving File Error"
,
"Could not save current script"
,
e
);
}
}
public
void
openJavaFile
()
{
loadJavaFile
();
...
...
@@ -629,7 +587,7 @@ public class DebuggerMain implements Initializable {
}
}
/*
@FXML
@FXML
public
void
saveScript
()
{
try
{
scriptController
.
saveCurrentScript
();
...
...
@@ -638,7 +596,7 @@ public class DebuggerMain implements Initializable {
}
}
*/
@FXML
public
void
saveAsScript
()
throws
IOException
{
File
f
=
openFileChooserSaveDialog
(
"Save script"
,
"Save Script files"
,
"kps"
);
...
...
@@ -675,11 +633,6 @@ public class DebuggerMain implements Initializable {
}
}
@FXML
protected
void
loadKeYFile
()
{
File
keyFile
=
openFileChooserOpenDialog
(
"Select KeY File"
,
"KeY Files"
,
"key"
,
"kps"
);
openKeyFile
(
keyFile
);
}
/**
* Save KeY proof as proof file
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
View file @
45f9a7ad
...
...
@@ -4,6 +4,7 @@ import com.google.common.eventbus.Subscribe;
import
com.google.common.graph.MutableValueGraph
;
import
edu.kit.iti.formal.psdbg.InterpretingService
;
import
edu.kit.iti.formal.psdbg.gui.controls.DebuggerStatusBar
;
import
edu.kit.iti.formal.psdbg.gui.controls.Utils
;
import
edu.kit.iti.formal.psdbg.gui.model.Breakpoint
;
import
edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter
;
import
edu.kit.iti.formal.psdbg.interpreter.data.GoalNode
;
...
...
@@ -270,11 +271,11 @@ public class ProofTreeController {
blocker
.
deinstall
();
blocker
.
install
(
currentInterpreter
);
if
(!
debugMode
)
{
/*
if (!debugMode) {
statusBar.setText("Starting in execution mode for script " + mainScript.getName());
statusBar.indicateProgress();
blocker.getStepUntilBlock().set(-1);
}
else
{
} else {
*/
statusBar
.
setText
(
"Starting in debug mode for script "
+
mainScript
.
getName
());
statusBar
.
indicateProgress
();
setCurrentHighlightNode
(
mainScript
.
get
());
...
...
@@ -287,8 +288,7 @@ public class ProofTreeController {
this
.
stateGraphWrapper
.
install
(
currentInterpreter
);
this
.
stateGraphWrapper
.
addChangeListener
(
graphChangedListener
);
statusBar
.
stopProgress
();
blocker
.
getStepUntilBlock
().
set
(
1
);
}
//}
//create interpreter service and start
if
(
interpreterService
.
getState
()
==
Worker
.
State
.
SUCCEEDED
...
...
@@ -302,6 +302,10 @@ public class ProofTreeController {
interpreterService
.
start
();
interpreterService
.
setOnSucceeded
(
event
->
{
statusBar
.
setText
(
"Executed until end of script."
);
//TODO is this the right position??
if
(
currentGoals
.
isEmpty
())
{
Utils
.
showClosedProofDialog
(
mainScript
.
get
().
getName
());
}
statusBar
.
stopProgress
();
});
interpreterService
.
setOnFailed
(
event
->
{
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java
View file @
45f9a7ad
...
...
@@ -58,12 +58,14 @@ public class ScriptController {
@Subscribe
public
void
handle
(
Events
.
NewNodeExecuted
newNode
)
{
logger
.
debug
(
"Handling new node added event!"
);
ASTNode
scriptNode
=
newNode
.
getCorrespondingASTNode
();
ScriptArea
editor
=
findEditor
(
scriptNode
);
editor
.
removeExecutionMarker
();
LineMapping
lm
=
new
LineMapping
(
editor
.
getText
());
int
pos
=
lm
.
getLineEnd
(
scriptNode
.
getStartPosition
().
getLineNumber
()
-
1
);
editor
.
insertExecutionMarker
(
pos
);
System
.
out
.
println
(
pos
);
// editor.insertExecutionMarker(pos);
}
private
ScriptArea
findEditor
(
ASTNode
node
)
{
...
...
ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml
View file @
45f9a7ad
...
...
@@ -99,7 +99,7 @@
<MenuItem
text=
"Execute Script Stepwise From Start"
onAction=
"#execute
InDebugMod
e"
onAction=
"#execute
Stepwis
e"
disable=
"${controller.executeNotPossible}"
>
<graphic>
<MaterialDesignIconView
glyphName=
"PLAY_PAUSE"
size=
"24.0"
/>
...
...
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