Commit 8f73f020 authored by Sarah Grebing's avatar Sarah Grebing

demo/loading stuff

parent 874c5365
Pipeline #21104 failed with stages
...@@ -13,6 +13,7 @@ import de.uka.ilkd.key.speclang.Contract; ...@@ -13,6 +13,7 @@ import de.uka.ilkd.key.speclang.Contract;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import javafx.beans.binding.BooleanBinding; import javafx.beans.binding.BooleanBinding;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleObjectProperty; import javafx.beans.property.SimpleObjectProperty;
import javafx.concurrent.Task; import javafx.concurrent.Task;
import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.LogManager;
...@@ -33,6 +34,19 @@ import java.util.stream.Collectors; ...@@ -33,6 +34,19 @@ import java.util.stream.Collectors;
public class KeYProofFacade { public class KeYProofFacade {
private static final Logger LOGGER = LogManager.getLogger(KeYProofFacade.class); private static final Logger LOGGER = LogManager.getLogger(KeYProofFacade.class);
public boolean isLoading() {
return loading.get();
}
public SimpleBooleanProperty loadingProperty() {
return loading;
}
public void setLoading(boolean loading) {
this.loading.set(loading);
}
private SimpleBooleanProperty loading = new SimpleBooleanProperty(false);
/** /**
* Current Proof * Current Proof
*/ */
...@@ -87,6 +101,7 @@ public class KeYProofFacade { ...@@ -87,6 +101,7 @@ public class KeYProofFacade {
Task<ProofApi> task = new Task<ProofApi>() { Task<ProofApi> task = new Task<ProofApi>() {
@Override @Override
protected ProofApi call() throws Exception { protected ProofApi call() throws Exception {
setLoading(true);
ProofApi pa = loadKeyFile(keYFile); ProofApi pa = loadKeyFile(keYFile);
return pa; return pa;
} }
...@@ -97,6 +112,7 @@ public class KeYProofFacade { ...@@ -97,6 +112,7 @@ public class KeYProofFacade {
environment.set(getValue().getEnv()); environment.set(getValue().getEnv());
proof.set(getValue().getProof()); proof.set(getValue().getProof());
contract.set(null); contract.set(null);
setLoading(false);
} }
}; };
...@@ -111,16 +127,20 @@ public class KeYProofFacade { ...@@ -111,16 +127,20 @@ public class KeYProofFacade {
* @throws ProblemLoaderException * @throws ProblemLoaderException
*/ */
ProofApi loadKeyFile(File keYFile) throws ProblemLoaderException { ProofApi loadKeyFile(File keYFile) throws ProblemLoaderException {
setLoading(true);
ProofManagementApi pma = KeYApi.loadFromKeyFile(keYFile); ProofManagementApi pma = KeYApi.loadFromKeyFile(keYFile);
ProofApi pa = pma.getLoadedProof(); ProofApi pa = pma.getLoadedProof();
setLoading(false);
return pa; return pa;
} }
public ProofApi loadKeyFileSync(File keyFile) throws ProblemLoaderException { public ProofApi loadKeyFileSync(File keyFile) throws ProblemLoaderException {
setLoading(true);
ProofApi pa = loadKeyFile(keyFile); ProofApi pa = loadKeyFile(keyFile);
environment.set(pa.getEnv()); environment.set(pa.getEnv());
proof.set(pa.getProof()); proof.set(pa.getProof());
contract.set(null); contract.set(null);
setLoading(false);
return pa; return pa;
} }
......
...@@ -36,6 +36,8 @@ import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; ...@@ -36,6 +36,8 @@ import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import javafx.application.Platform; import javafx.application.Platform;
import javafx.beans.InvalidationListener; import javafx.beans.InvalidationListener;
import javafx.beans.binding.BooleanBinding; import javafx.beans.binding.BooleanBinding;
import javafx.beans.property.BooleanProperty;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.collections.FXCollections; import javafx.collections.FXCollections;
import javafx.collections.ObservableList; import javafx.collections.ObservableList;
import javafx.concurrent.Service; import javafx.concurrent.Service;
...@@ -132,6 +134,7 @@ public class DebuggerMain implements Initializable { ...@@ -132,6 +134,7 @@ public class DebuggerMain implements Initializable {
@FXML @FXML
private Button interactive_undo; private Button interactive_undo;
private JavaArea javaArea = new JavaArea(); private JavaArea javaArea = new JavaArea();
private DockNode javaAreaDock = new DockNode(javaArea, "Java Source", private DockNode javaAreaDock = new DockNode(javaArea, "Java Source",
new MaterialDesignIconView(MaterialDesignIcon.CODEPEN) new MaterialDesignIconView(MaterialDesignIcon.CODEPEN)
...@@ -191,7 +194,7 @@ public class DebuggerMain implements Initializable { ...@@ -191,7 +194,7 @@ public class DebuggerMain implements Initializable {
private void init() { private void init() {
Events.register(this); Events.register(this);
model.setDebugMode(false); // model.setDebugMode(false);
scriptController = new ScriptController(dockStation); scriptController = new ScriptController(dockStation);
interactiveModeController = new InteractiveModeController(scriptController); interactiveModeController = new InteractiveModeController(scriptController);
btnInteractiveMode.setSelected(false); btnInteractiveMode.setSelected(false);
...@@ -278,6 +281,36 @@ public class DebuggerMain implements Initializable { ...@@ -278,6 +281,36 @@ public class DebuggerMain implements Initializable {
proofTreeDock, proofTreeDock,
DockPos.LEFT); DockPos.LEFT);
//if threadstate finished, stepping should still be possible
BooleanBinding disableStepping = FACADE.loadingProperty().
or(FACADE.proofProperty().isNull()).
or(model.interpreterStateProperty().isNotEqualTo(InterpreterThreadState.WAIT));
/* model.statePointerProperty().addListener((observable, oldValue, newValue) -> {
//set all steppings -> remove binding
if(newValue.getStepInvOver() != null)
model.setStepReturnPossible(true);
if(newValue.getStepOver() != null)
model.setStepOverPossible(true);
if(newValue.getStepInvInto() != null)
model.setStepBackPossible(true);
if(newValue.getStepInto() != null)
model.setStepIntoPossible(true);
});*/
model.stepBackPossibleProperty().bind(disableStepping);
model.stepIntoPossibleProperty().bind(disableStepping);
model.stepOverPossibleProperty().bind(disableStepping);
model.stepReturnPossibleProperty().bind(disableStepping);
model.executeNotPossibleProperty().bind(FACADE.loadingProperty().or(FACADE.proofProperty().isNull()));
statusBar.interpreterStatusModelProperty().bind(model.interpreterStateProperty()); statusBar.interpreterStatusModelProperty().bind(model.interpreterStateProperty());
renewThreadStateTimer(); renewThreadStateTimer();
} }
...@@ -320,6 +353,9 @@ public class DebuggerMain implements Initializable { ...@@ -320,6 +353,9 @@ public class DebuggerMain implements Initializable {
} }
/**
* Connect the Javacode area with the model and the rest of the GUI
*/
private void marriageJavaCode() { private void marriageJavaCode() {
//Listener on chosenContract from //Listener on chosenContract from
model.chosenContractProperty().addListener(o -> { model.chosenContractProperty().addListener(o -> {
...@@ -428,7 +464,7 @@ public class DebuggerMain implements Initializable { ...@@ -428,7 +464,7 @@ public class DebuggerMain implements Initializable {
assert model.getDebuggerFramework() == null : "There should not be any interpreter running."; assert model.getDebuggerFramework() == null : "There should not be any interpreter running.";
if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) { if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) {
Alert alert = new Alert(Alert.AlertType.ERROR, "No proof loaded!", ButtonType.OK); Alert alert = new Alert(Alert.AlertType.INFORMATION, "No proof loaded is loaded yet. If proof loading was onvoked, please wait. Loading may take a while.", ButtonType.OK);
alert.showAndWait(); alert.showAndWait();
return; return;
} }
...@@ -711,10 +747,13 @@ public class DebuggerMain implements Initializable { ...@@ -711,10 +747,13 @@ public class DebuggerMain implements Initializable {
if (keyFile != null) { if (keyFile != null) {
model.setKeyFile(keyFile); model.setKeyFile(keyFile);
model.setInitialDirectory(keyFile.getParentFile()); model.setInitialDirectory(keyFile.getParentFile());
Task<ProofApi> task = FACADE.loadKeyFileTask(keyFile); Task<ProofApi> task = FACADE.loadKeyFileTask(keyFile);
task.setOnSucceeded(event -> { task.setOnSucceeded(event -> {
statusBar.publishMessage("Loaded key sourceName: %s", keyFile); statusBar.publishMessage("Loaded key sourceName: %s", keyFile);
statusBar.stopProgress(); statusBar.stopProgress();
}); });
task.setOnFailed(event -> { task.setOnFailed(event -> {
...@@ -1182,7 +1221,7 @@ public class DebuggerMain implements Initializable { ...@@ -1182,7 +1221,7 @@ public class DebuggerMain implements Initializable {
public void openInKey(@Nullable ActionEvent event) { public void openInKey(@Nullable ActionEvent event) {
if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) { if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) {
Alert alert = new Alert(Alert.AlertType.ERROR, "No proof is loaded", ButtonType.OK); Alert alert = new Alert(Alert.AlertType.INFORMATION, "No proof is loaded yet. If laoding a proof was invoked, proof state loading may take a while.", ButtonType.OK);
alert.show(); alert.show();
return; return;
} }
......
...@@ -217,7 +217,7 @@ public class InspectionView extends BorderPane { ...@@ -217,7 +217,7 @@ public class InspectionView extends BorderPane {
if (goalOptionsMenu.getSelectedViewOption() != null) { if (goalOptionsMenu.getSelectedViewOption() != null) {
text = goalOptionsMenu.getSelectedViewOption().getText(item); text = goalOptionsMenu.getSelectedViewOption().getText(item);
} }
//setStyle("-fx-font-size: 12pt;"); //TODO for ScreenshotsetStyle("-fx-font-size: 18pt;");
setText(text); setText(text);
} }
} }
......
...@@ -434,6 +434,7 @@ public class ProofTree extends BorderPane { ...@@ -434,6 +434,7 @@ public class ProofTree extends BorderPane {
tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";"); tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";");
} }
} }
//TODO for Screenshot tftc.setStyle("-fx-font-size: 18pt");
/* if (colorOfNodes.containsKey(n)) { /* if (colorOfNodes.containsKey(n)) {
tftc.setStyle("-fx-border-color: "+colorOfNodes.get(n)+";"); tftc.setStyle("-fx-border-color: "+colorOfNodes.get(n)+";");
}*/ }*/
......
...@@ -130,7 +130,8 @@ public class ScriptArea extends BorderPane { ...@@ -130,7 +130,8 @@ public class ScriptArea extends BorderPane {
private ListProperty<LintProblem> problems = new SimpleListProperty<>(FXCollections.observableArrayList()); private ListProperty<LintProblem> problems = new SimpleListProperty<>(FXCollections.observableArrayList());
private SimpleObjectProperty<CharacterHit> currentMouseOver = new SimpleObjectProperty<>(); private SimpleObjectProperty<CharacterHit> currentMouseOver = new SimpleObjectProperty<>();
private ScriptAreaContextMenu contextMenu = new ScriptAreaContextMenu(); private ScriptAreaContextMenu contextMenu = new ScriptAreaContextMenu();
private Consumer<Token> onPostMortem = token -> { private Consumer<Token> onPostMortem = token -> {
}; };
@Getter @Getter
@Setter @Setter
......
...@@ -25,6 +25,9 @@ public class DebuggerMainModel { ...@@ -25,6 +25,9 @@ public class DebuggerMainModel {
*/ */
private final ObjectProperty<Contract> chosenContract = new SimpleObjectProperty<>(this, "chosenContract"); private final ObjectProperty<Contract> chosenContract = new SimpleObjectProperty<>(this, "chosenContract");
/**
* Properties for stepping enabling and disabling
*/
private ObjectProperty<DebuggerFramework<KeyData>> debuggerFramework = new SimpleObjectProperty<>(); private ObjectProperty<DebuggerFramework<KeyData>> debuggerFramework = new SimpleObjectProperty<>();
private ObjectProperty<PTreeNode<KeyData>> statePointer = new SimpleObjectProperty<>(); private ObjectProperty<PTreeNode<KeyData>> statePointer = new SimpleObjectProperty<>();
...@@ -41,9 +44,9 @@ public class DebuggerMainModel { ...@@ -41,9 +44,9 @@ public class DebuggerMainModel {
InterpreterThreadState.NO_THREAD); InterpreterThreadState.NO_THREAD);
/** /**
* True, iff the execution is not possible * True, iff the execution of script is not possible
*/ */
private ObservableBooleanValue executeNotPossible = new SimpleBooleanProperty();//proofTreeController.executeNotPossibleProperty().or(FACADE.readyToExecuteProperty().not()); private BooleanProperty executeNotPossible = new SimpleBooleanProperty(true);//proofTreeController.executeNotPossibleProperty().or(FACADE.readyToExecuteProperty().not());
/** /**
* *
...@@ -56,7 +59,7 @@ public class DebuggerMainModel { ...@@ -56,7 +59,7 @@ public class DebuggerMainModel {
private StringProperty javaCode = new SimpleStringProperty(this, "javaCode"); private StringProperty javaCode = new SimpleStringProperty(this, "javaCode");
private BooleanProperty debugMode = new SimpleBooleanProperty(this, "debugMode", false); //private BooleanProperty debugMode = new SimpleBooleanProperty(this, "debugMode", false);
public DebuggerFramework<KeyData> getDebuggerFramework() { public DebuggerFramework<KeyData> getDebuggerFramework() {
return debuggerFramework.get(); return debuggerFramework.get();
...@@ -170,7 +173,7 @@ public class DebuggerMainModel { ...@@ -170,7 +173,7 @@ public class DebuggerMainModel {
return executeNotPossible.get(); return executeNotPossible.get();
} }
public ObservableBooleanValue executeNotPossibleProperty() { public BooleanProperty executeNotPossibleProperty() {
return executeNotPossible; return executeNotPossible;
} }
...@@ -198,6 +201,7 @@ public class DebuggerMainModel { ...@@ -198,6 +201,7 @@ public class DebuggerMainModel {
return javaCode; return javaCode;
} }
/*
public boolean isDebugMode() { public boolean isDebugMode() {
return debugMode.get(); return debugMode.get();
} }
...@@ -210,6 +214,7 @@ public class DebuggerMainModel { ...@@ -210,6 +214,7 @@ public class DebuggerMainModel {
return debugMode; return debugMode;
} }
*/
public InterpreterThreadState getInterpreterState() { public InterpreterThreadState getInterpreterState() {
return interpreterState.get(); return interpreterState.get();
} }
......
@base03: rgb(0, 43, 54); @base03: rgb(0, 43, 54);
@base02: rgb(7, 54, 66); @base02: rgb(7, 54, 66);
@base01: rgb(88, 110, 117); @base01: #000000;
//@base01: rgb(88, 110, 117);
@base00: rgb(101, 123, 131); @base00: rgb(101, 123, 131);
@base0: rgb(131, 148, 150); @base0: rgb(131, 148, 150);
@base1: rgb(147, 161, 161); @base1: rgb(147, 161, 161);
...@@ -15,9 +17,11 @@ ...@@ -15,9 +17,11 @@
@cyan: rgb(42, 161, 152); @cyan: rgb(42, 161, 152);
@green: rgb(38, 187, 108); @green: rgb(38, 187, 108);
@basenavy: #f6f8ff; @basenavy: #f6f8ff;
//screenshot @basenavy: #ffffff;
@keywordColor: #200080; @keywordColor: #200080;
@stringliteralColor: #6679aa; @stringliteralColor: #6679aa;
@integerLiteralColor: #008c00; @integerLiteralColor: #008c00;
@screenShotMarkerBase: #97ffc6;
.solarized-dark() { .solarized-dark() {
background-color: @base03; background-color: @base03;
...@@ -35,7 +39,7 @@ ...@@ -35,7 +39,7 @@
-fx-font-family: "Inconsolata", monospace; -fx-font-family: "Inconsolata", monospace;
//-fx-font-family: "Fira Code Medium", monospace; //-fx-font-family: "Fira Code Medium", monospace;
-fx-font-size: 12pt; -fx-font-size: 12pt;
//-fx-font-size: 18pt; // -fx-font-size: 20pt;
-fx-fill: @base00; -fx-fill: @base00;
.lineno { .lineno {
...@@ -112,7 +116,9 @@ ...@@ -112,7 +116,9 @@
} }
.line-highlight-postmortem { .line-highlight-postmortem {
-rtfx-background-color: @cyan; // -rtfx-background-color: @cyan;
-rtfx-background-color: @screenShotMarkerBase;
} }
.line-unhighlight { .line-unhighlight {
...@@ -120,7 +126,8 @@ ...@@ -120,7 +126,8 @@
} }
.line-highlight-mainScript { .line-highlight-mainScript {
-rtfx-background-color: @green; // -rtfx-background-color: @green;
-rtfx-background-color: @screenShotMarkerBase;
} }
} }
...@@ -139,7 +146,7 @@ ...@@ -139,7 +146,7 @@
// -fx-background-color: @base3; // -fx-background-color: @base3;
-fx-font-family: "Inconsolata", monospace; -fx-font-family: "Inconsolata", monospace;
-fx-font-size: 12pt; -fx-font-size: 12pt;
//-fx-font-size: 18pt; //-fx-font-size: 20pt;
-fx-fill: @base01; -fx-fill: @base01;
.ABSTRACT, .ASSERT, .BOOLEAN, .BREAK, .BYTE, .CASE, .CATCH, .CHAR, .CLASS, .CONST, .ABSTRACT, .ASSERT, .BOOLEAN, .BREAK, .BYTE, .CASE, .CATCH, .CHAR, .CLASS, .CONST,
...@@ -192,7 +199,9 @@ ...@@ -192,7 +199,9 @@
-fx-underline: true; -fx-underline: true;
} }
.line-highlight { .line-highlight {
-rtfx-background-color: @cyan; // -rtfx-background-color: @cyan;
-rtfx-background-color: @screenShotMarkerBase;
} }
.line-un-highlight { .line-un-highlight {
-rtfx-background-color: @basenavy; -rtfx-background-color: @basenavy;
...@@ -234,7 +243,7 @@ ...@@ -234,7 +243,7 @@
.sequent-view { .sequent-view {
-fx-font-size: 14pt; -fx-font-size: 14pt;
//-fx-font-size: 18pt; // -fx-font-size: 20pt;
-fx-background-color: @basenavy; -fx-background-color: @basenavy;
-fx-fill: black; -fx-fill: black;
......
...@@ -56,10 +56,9 @@ The main features of the language are: ...@@ -56,10 +56,9 @@ The main features of the language are:
1. integration of domain specific entities like goal, formula, term and rule as 1. integration of domain specific entities like goal, formula, term and rule as
first-class citizens into the language;</li> first-class citizens into the language;</li>
1. an expressive proof goal selection mechanism 1. an expressive proof goal selection mechanism
* to identify and select individual proof branches, - to identify and select individual proof branches,
* to easily switch between proof branches, - to easily switch between proof branches,
* to select multiple branches for uniform treatment (multi-matching); - to select multiple branches for uniform treatment (multi-matching); that is resilient to small changes in the proof
that is resilient to small changes in the proof
1. a repetition construct which allows repeated application of proof strategies;</li> 1. a repetition construct which allows repeated application of proof strategies;</li>
1. support for proof exploration within the language.</li> 1. support for proof exploration within the language.</li>
...@@ -71,7 +70,9 @@ the analysis of failed proof attempts. ...@@ -71,7 +70,9 @@ the analysis of failed proof attempts.
## Publications ## Publications
A full description of the language and debugging-concept A full description of the language and debugging-concept
is published at [HVC 2017](http://rdcu.be/E4fF) is published at [HVC 2017](http://rdcu.be/E4fF).
A short tool description is also [available](
http://arxiv.org/abs/1804.04402).
## Debugging Script for Quicksort's `split` method. ## Debugging Script for Quicksort's `split` method.
...@@ -208,18 +209,17 @@ interactive rule applications. ...@@ -208,18 +209,17 @@ interactive rule applications.
<h2>Downloads</h2> <h2>Downloads</h2>
<ul> <ul>
<li>PSDBG - <strong>Version 1.0.1c-FM</strong> <li>PSDBG - <strong>Version 1.0.2c-FM</strong>
<a href="../psdbg_releases/psdbg-1.0.1c-fm.jar">psdbg-1.0.1c-fm.jar</a> <a href="../psdbg_releases/psdbg-1.0.2c-fm.jar">psdbg-1.0.2c-fm.jar</a>
<br> <br>
Special Version for the tool paper at Formal Methods 2018. First implementation of PSDBG, including examples.
Including examples and all dependencies.
<br> <br>
Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of depdendencies. Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of depdendencies.
<br> <br>
<a href="https://www.gnu.org/licenses/gpl-3.0.txt">License: GPLv3</a> <a href="https://www.gnu.org/licenses/gpl-3.0.txt">License: GPLv3</a>
<a href="thirdparty.txt">Third Party Licenses</a> <a href="thirdparty.txt">Third Party Licenses</a>
<br> <br>
Executable with <code>java -jar psdbg-1.0.1c-fm.jar</code> Executable with <code>java -jar psdbg-1.0.2c-fm.jar</code>
</li> </li>
</ul> </ul>
......
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