Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
sarah.grebing
ProofScriptParser
Commits
cd3bba8c
Commit
cd3bba8c
authored
Aug 15, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
minor enhancement for progressbar+ dummy grammar for matchpattern (not finished)
parent
4efda617
Pipeline
#12866
failed with stage
in 4 minutes and 43 seconds
Changes
5
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
70 additions
and
5 deletions
+70
-5
src/main/antlr4/edu/kit/formal/termmatcher/MatchPattern.g4
src/main/antlr4/edu/kit/formal/termmatcher/MatchPattern.g4
+30
-0
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
...t/formal/gui/controller/DebuggerMainWindowController.java
+4
-1
src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java
src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java
+17
-0
src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java
...du/kit/formal/interpreter/graphs/ProofTreeController.java
+18
-3
src/test/resources/edu/kit/formal/interpreter/javaExample/testIsClosable.kps
...edu/kit/formal/interpreter/javaExample/testIsClosable.kps
+1
-1
No files found.
src/main/antlr4/edu/kit/formal/termmatcher/MatchPattern.g4
0 → 100644
View file @
cd3bba8c
grammar MatchPattern;
schemaTerm :
'_'
|'...'
| schemaVar
| logicalVar
| functionSymbol ('('schemaTerm (',' schemaTerm)? ')')?
;
termHelper :
schemaTerm
| functionSymbol '('termHelper (',' termHelper)? ')'
;
functionSymbol :
ID+
;
schemaVar:
'?'ID+
;
logicalVar:
ID+
;
DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ;
ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' | '[]' | '-')* ;
\ No newline at end of file
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
View file @
cd3bba8c
...
...
@@ -310,7 +310,8 @@ public class DebuggerMainWindowController implements Initializable {
proofTreeController
.
setCurrentInterpreter
(
currentInterpreter
);
proofTreeController
.
setMainScript
(
scripts
.
get
(
0
));
proofTreeController
.
executeScript
(
this
.
debugMode
.
get
());
statusBar
.
publishMessage
(
"Executing script "
+
scripts
.
get
(
0
).
getName
());
proofTreeController
.
executeScript
(
this
.
debugMode
.
get
(),
statusBar
);
//highlight signature of main script
//scriptController.setDebugMark(scripts.get(0).getStartPosition().getLineNumber());
}
catch
(
RecognitionException
e
)
{
...
...
@@ -388,10 +389,12 @@ public class DebuggerMainWindowController implements Initializable {
Task
<
Void
>
task
=
FACADE
.
loadKeyFileTask
(
keyFile
);
task
.
setOnSucceeded
(
event
->
{
statusBar
.
publishMessage
(
"Loaded key sourceName: %s"
,
keyFile
);
statusBar
.
stopProgress
();
getInspectionViewsController
().
getActiveInspectionViewTab
().
getModel
().
getGoals
().
setAll
(
FACADE
.
getPseudoGoals
());
});
task
.
setOnFailed
(
event
->
{
statusBar
.
stopProgress
();
event
.
getSource
().
exceptionProperty
().
get
();
Utils
.
showExceptionDialog
(
"Could not load sourceName"
,
"Key sourceName loading error"
,
""
,
(
Throwable
)
event
.
getSource
().
exceptionProperty
().
get
()
...
...
src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java
View file @
cd3bba8c
...
...
@@ -14,6 +14,8 @@ import edu.kit.formal.interpreter.data.KeyData;
import
javafx.beans.binding.BooleanBinding
;
import
javafx.beans.property.SimpleObjectProperty
;
import
javafx.concurrent.Task
;
import
org.apache.logging.log4j.LogManager
;
import
org.apache.logging.log4j.Logger
;
import
java.io.File
;
import
java.util.Collection
;
...
...
@@ -26,11 +28,26 @@ import java.util.List;
* @author A. Weigl
*/
public
class
KeYProofFacade
{
private
static
final
Logger
LOGGER
=
LogManager
.
getLogger
(
KeYProofFacade
.
class
);
/**
* Current Proof
*/
private
SimpleObjectProperty
<
Proof
>
proof
=
new
SimpleObjectProperty
<>();
/**
* Current KeYEnvironment
*/
private
SimpleObjectProperty
<
KeYEnvironment
>
environment
=
new
SimpleObjectProperty
<>();
/**
* Chosen Contract; Null if only key file was loaded
*/
private
SimpleObjectProperty
<
Contract
>
contract
=
new
SimpleObjectProperty
<>();
/**
* BooleanProperty inidcating whether KeY finished loading
*/
private
BooleanBinding
readyToExecute
=
proof
.
isNotNull
();
//Workaround until api is relaxed
private
ProofManagementApi
pma
;
...
...
src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java
View file @
cd3bba8c
...
...
@@ -3,6 +3,7 @@ package edu.kit.formal.interpreter.graphs;
import
com.google.common.eventbus.Subscribe
;
import
edu.kit.formal.gui.controller.Events
;
import
edu.kit.formal.gui.controller.PuppetMaster
;
import
edu.kit.formal.gui.controls.DebuggerStatusBar
;
import
edu.kit.formal.interpreter.Interpreter
;
import
edu.kit.formal.interpreter.InterpretingService
;
import
edu.kit.formal.interpreter.data.GoalNode
;
...
...
@@ -108,7 +109,8 @@ public class ProofTreeController {
};
/**
*
* Create a new ProofTreeController
* and bind properties
*/
public
ProofTreeController
()
{
...
...
@@ -217,15 +219,21 @@ public class ProofTreeController {
* If this method is executed with debug mode true, it executes only statements after invoking the methods stepOver() and stepInto()
*
* @param debugMode
* @param statusBar
*/
public
void
executeScript
(
boolean
debugMode
)
{
public
void
executeScript
(
boolean
debugMode
,
DebuggerStatusBar
statusBar
)
{
Events
.
register
(
this
);
blocker
.
deinstall
();
blocker
.
install
(
currentInterpreter
);
if
(!
debugMode
)
{
statusBar
.
setText
(
"Starting in execution mode for script "
+
mainScript
.
getName
());
statusBar
.
indicateProgress
();
blocker
.
getStepUntilBlock
().
set
(-
1
);
}
else
{
statusBar
.
setText
(
"Starting in debug mode for script "
+
mainScript
.
getName
());
statusBar
.
indicateProgress
();
setCurrentHighlightNode
(
mainScript
.
getSignature
());
//build CFG
...
...
@@ -245,7 +253,14 @@ public class ProofTreeController {
interpreterService
.
interpreterProperty
().
set
(
currentInterpreter
);
interpreterService
.
mainScriptProperty
().
set
(
mainScript
);
interpreterService
.
start
();
interpreterService
.
setOnSucceeded
(
event
->
{
statusBar
.
setText
(
"Executed script until end of script."
);
statusBar
.
stopProgress
();
});
interpreterService
.
setOnFailed
(
event
->
{
statusBar
.
setText
(
"Failed to execute script"
);
statusBar
.
stopProgress
();
});
}
...
...
src/test/resources/edu/kit/formal/interpreter/javaExample/testIsClosable.kps
View file @
cd3bba8c
script t1(){
symbex;
cases{
case
match
isCloseable:{
case isCloseable:{
andRight; //should not close proof
}
...
...
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