Commit b8ec7a67 authored by Alexander Weigl's avatar Alexander Weigl

Merge branch 'master' of git.scc.kit.edu:xt9634/ProofScriptParser

* 'master' of git.scc.kit.edu:xt9634/ProofScriptParser:
  minor enhancement for progressbar+ dummy grammar for matchpattern (not finished)
parents 2b5b35ae cd3bba8c
Pipeline #12867 failed with stage
in 1 minute and 41 seconds
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
......@@ -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()
......
......@@ -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;
......
......@@ -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();
});
}
......
script t1(){
symbex;
cases{
case match isCloseable:{
case isCloseable:{
andRight; //should not close proof
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment