Commit defba7b3 authored by Sarah Grebing's avatar Sarah Grebing

corrected handling of match results concerning varaible assignment and added...

corrected handling of match results concerning varaible assignment and added number of nodes and progress to status bar
parent a0ff0420
Pipeline #13507 failed with stage
in 2 minutes and 56 seconds
...@@ -207,7 +207,9 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -207,7 +207,9 @@ public class KeYMatcher implements MatcherApi<KeyData> {
public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, String data, Signature sig) { public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, String data, Signature sig) {
System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data); System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
System.out.println("Signature " + sig.toString()); System.out.println("Signature " + sig.toString());
Matchings m = MatcherFacade.matches(data, currentState.getData().getNode().sequent()); Matchings m = MatcherFacade.matches(data, currentState.getData().getNode().sequent());
if (m.isEmpty()) { if (m.isEmpty()) {
return Collections.emptyList(); return Collections.emptyList();
} else { } else {
...@@ -217,8 +219,13 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -217,8 +219,13 @@ public class KeYMatcher implements MatcherApi<KeyData> {
MatchPath matchPath = firstMatch.get(s); MatchPath matchPath = firstMatch.get(s);
if (!s.equals("EMPTY_MATCH")) { if (!s.equals("EMPTY_MATCH")) {
Term matched = (Term) matchPath.getUnit(); Term matched = (Term) matchPath.getUnit();
if (s.startsWith("?")) {
s = s.replaceFirst("\\?", "");
}
va.declare(s, new TermType()); va.declare(s, new TermType());
va.assign(s, Value.from(from(matched))); va.assign(s, Value.from(from(matched)));
System.out.println("Variable " + s + " : " + Value.from(from(matched)));
} }
} }
List<VariableAssignment> retList = new LinkedList(); List<VariableAssignment> retList = new LinkedList();
......
script cutTest(){ script cutTest(){
cut #2=`p`; cases{
case match `==>?X -> ?Y`:
}
//cut #2=`p`;
//auto steps=100;
} }
\ No newline at end of file
...@@ -52,7 +52,13 @@ public class DefaultLookup implements CommandLookup { ...@@ -52,7 +52,13 @@ public class DefaultLookup implements CommandLookup {
if (found == null) { if (found == null) {
found = b; found = b;
} else { } else {
throw new IllegalStateException("Call on line" + callStatement + " is ambigue."); found = b; //CUTCommand
System.out.println(b.getClass());
System.out.println(found.getClass());
if (callStatement.getCommand().equals("cut")) {
System.out.println("Cut Case");
}
//throw new IllegalStateException("Call on line" + callStatement + " is ambigue.");
} }
} }
} }
......
package edu.kit.iti.formal.psdbg; package edu.kit.iti.formal.psdbg;
import edu.kit.iti.formal.psdbg.gui.controller.PuppetMaster; import edu.kit.iti.formal.psdbg.gui.controller.PuppetMaster;
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.controls.Utils;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter; import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
...@@ -17,11 +18,11 @@ import javafx.concurrent.Task; ...@@ -17,11 +18,11 @@ import javafx.concurrent.Task;
* @author A. Weigl * @author A. Weigl
*/ */
public class InterpretingService extends Service<State<KeyData>> { public class InterpretingService extends Service<State<KeyData>> {
/** /**
* The interpreter (with teh appropriate KeY state) that is used to traverse and execute the script * The interpreter (with the appropriate KeY state) that is used to traverse and execute the script
*/ */
private final SimpleObjectProperty<Interpreter<KeyData>> interpreter = new SimpleObjectProperty<>(); private final SimpleObjectProperty<Interpreter<KeyData>> interpreter = new SimpleObjectProperty<>();
private DebuggerStatusBar statusBar;
/** /**
* The main script that is traversed * The main script that is traversed
...@@ -41,6 +42,12 @@ public class InterpretingService extends Service<State<KeyData>> { ...@@ -41,6 +42,12 @@ public class InterpretingService extends Service<State<KeyData>> {
this.blocker = blocker; this.blocker = blocker;
} }
public InterpretingService(PuppetMaster blocker, DebuggerStatusBar statusBar) {
this.blocker = blocker;
this.statusBar = statusBar;
}
public SimpleBooleanProperty hasRunSucessfullyProperty() { public SimpleBooleanProperty hasRunSucessfullyProperty() {
return hasRunSucessfully; return hasRunSucessfully;
} }
...@@ -70,6 +77,9 @@ public class InterpretingService extends Service<State<KeyData>> { ...@@ -70,6 +77,9 @@ public class InterpretingService extends Service<State<KeyData>> {
//currentGoals.set(state.getGoals()); //currentGoals.set(state.getGoals());
//currentSelectedGoal.set(state.getSelectedGoalNode()); //currentSelectedGoal.set(state.getSelectedGoalNode());
System.out.println("Updating View"); System.out.println("Updating View");
if (statusBar != null) {
statusBar.stopProgress();
}
blocker.publishState(); blocker.publishState();
} }
...@@ -87,6 +97,9 @@ public class InterpretingService extends Service<State<KeyData>> { ...@@ -87,6 +97,9 @@ public class InterpretingService extends Service<State<KeyData>> {
*/ */
@Override @Override
protected edu.kit.iti.formal.psdbg.interpreter.data.State<KeyData> call() throws Exception { protected edu.kit.iti.formal.psdbg.interpreter.data.State<KeyData> call() throws Exception {
if (statusBar != null) {
statusBar.indicateProgress();
}
i.interpret(ast); i.interpret(ast);
return i.peekState(); return i.peekState();
} }
......
...@@ -159,6 +159,7 @@ public class DebuggerMain implements Initializable { ...@@ -159,6 +159,7 @@ public class DebuggerMain implements Initializable {
* If the mouse moves other toolbar button, the help text should display in the status bar * If the mouse moves other toolbar button, the help text should display in the status bar
*/ */
private void registerToolbarToStatusBar() { private void registerToolbarToStatusBar() {
/*toolbar.getChildrenUnmodifiable().forEach( /*toolbar.getChildrenUnmodifiable().forEach(
n -> n.setOnMouseEntered(statusBar.getTooltipHandler())); n -> n.setOnMouseEntered(statusBar.getTooltipHandler()));
...@@ -176,6 +177,7 @@ public class DebuggerMain implements Initializable { ...@@ -176,6 +177,7 @@ public class DebuggerMain implements Initializable {
proofTreeController.currentGoalsProperty().addListener((o, old, fresh) -> { proofTreeController.currentGoalsProperty().addListener((o, old, fresh) -> {
if (fresh != null) { if (fresh != null) {
imodel.setGoals(fresh); imodel.setGoals(fresh);
} else { } else {
// no goals, set an empty list // no goals, set an empty list
imodel.setGoals(FXCollections.observableArrayList()); imodel.setGoals(FXCollections.observableArrayList());
...@@ -198,6 +200,11 @@ public class DebuggerMain implements Initializable { ...@@ -198,6 +200,11 @@ public class DebuggerMain implements Initializable {
}); });
imodel.goalsProperty().addListener((observable, oldValue, newValue) -> statusBar.setNumberOfGoals(newValue.size()));
/*proofTreeController.currentExecutionEndProperty().addListener((observable, oldValue, newValue) -> { /*proofTreeController.currentExecutionEndProperty().addListener((observable, oldValue, newValue) -> {
scriptController.getMainScript().getScriptArea().removeExecutionMarker(); scriptController.getMainScript().getScriptArea().removeExecutionMarker();
LineMapping lm = new LineMapping(scriptController.getMainScript().getScriptArea().getText()); LineMapping lm = new LineMapping(scriptController.getMainScript().getScriptArea().getText());
......
...@@ -280,7 +280,7 @@ public class ProofTreeController { ...@@ -280,7 +280,7 @@ public class ProofTreeController {
this.stateGraphWrapper.install(currentInterpreter); this.stateGraphWrapper.install(currentInterpreter);
this.stateGraphWrapper.addChangeListener(graphChangedListener); this.stateGraphWrapper.addChangeListener(graphChangedListener);
statusBar.stopProgress();
blocker.getStepUntilBlock().set(1); blocker.getStepUntilBlock().set(1);
} }
...@@ -292,9 +292,10 @@ public class ProofTreeController { ...@@ -292,9 +292,10 @@ public class ProofTreeController {
interpreterService.interpreterProperty().set(currentInterpreter); interpreterService.interpreterProperty().set(currentInterpreter);
interpreterService.mainScriptProperty().set(mainScript.get()); interpreterService.mainScriptProperty().set(mainScript.get());
interpreterService.start(); interpreterService.start();
interpreterService.setOnSucceeded(event -> { interpreterService.setOnSucceeded(event -> {
statusBar.setText("Executed script until end of script."); statusBar.setText("Executed until end of script.");
statusBar.stopProgress(); statusBar.stopProgress();
}); });
interpreterService.setOnFailed(event -> { interpreterService.setOnFailed(event -> {
......
...@@ -2,7 +2,9 @@ package edu.kit.iti.formal.psdbg.gui.controls; ...@@ -2,7 +2,9 @@ package edu.kit.iti.formal.psdbg.gui.controls;
import edu.kit.iti.formal.psdbg.gui.controller.Events; import edu.kit.iti.formal.psdbg.gui.controller.Events;
import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier; import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
import javafx.beans.property.IntegerProperty;
import javafx.beans.property.ObjectProperty; import javafx.beans.property.ObjectProperty;
import javafx.beans.property.SimpleIntegerProperty;
import javafx.beans.property.SimpleObjectProperty; import javafx.beans.property.SimpleObjectProperty;
import javafx.event.EventHandler; import javafx.event.EventHandler;
import javafx.scene.control.Control; import javafx.scene.control.Control;
...@@ -26,12 +28,8 @@ public class DebuggerStatusBar extends StatusBar { ...@@ -26,12 +28,8 @@ public class DebuggerStatusBar extends StatusBar {
//private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX(); //private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX();
private ObjectProperty<MainScriptIdentifier> mainScriptIdentifier = new SimpleObjectProperty<>(); private ObjectProperty<MainScriptIdentifier> mainScriptIdentifier = new SimpleObjectProperty<>();
private Label lblCurrentNodes = new Label("#nodes: %s");
private Label lblMainscript = new Label(); private IntegerProperty numberOfGoals = new SimpleIntegerProperty(0);
private ProgressIndicator progressIndicator = new ProgressIndicator();
private EventHandler<MouseEvent> toolTipHandler = event -> {
publishMessage(((Control) event.getTarget()).getTooltip().getText());
};
public DebuggerStatusBar() { public DebuggerStatusBar() {
//listenOnField("psdbg"); //listenOnField("psdbg");
...@@ -47,7 +45,9 @@ public class DebuggerStatusBar extends StatusBar { ...@@ -47,7 +45,9 @@ public class DebuggerStatusBar extends StatusBar {
contextMenu.show(this, event.getScreenX(), event.getScreenY()); contextMenu.show(this, event.getScreenX(), event.getScreenY());
} }
});*/ });*/
numberOfGoals.addListener((observable, oldValue, newValue) -> {
lblCurrentNodes.setText("#nodes: " + newValue);
});
mainScriptIdentifier.addListener((ov, o, n) -> { mainScriptIdentifier.addListener((ov, o, n) -> {
if (n != null) { if (n != null) {
...@@ -75,6 +75,25 @@ public class DebuggerStatusBar extends StatusBar { ...@@ -75,6 +75,25 @@ public class DebuggerStatusBar extends StatusBar {
}); });
} }
public int getNumberOfGoals() {
return numberOfGoals.get();
}
public void setNumberOfGoals(int numberOfGoals) {
this.numberOfGoals.set(numberOfGoals);
}
private Label lblCurrentNodes = new Label("#nodes: %s");
private Label lblMainscript = new Label();
private ProgressIndicator progressIndicator = new ProgressIndicator();
private EventHandler<MouseEvent> toolTipHandler = event -> {
publishMessage(((Control) event.getTarget()).getTooltip().getText());
};
public IntegerProperty numberOfGoalsProperty() {
return numberOfGoals;
}
/* /*
private Appender createAppender() { private Appender createAppender() {
PatternLayout layout = PatternLayout.createDefaultLayout(); PatternLayout layout = PatternLayout.createDefaultLayout();
......
...@@ -158,6 +158,7 @@ public class InspectionView extends BorderPane { ...@@ -158,6 +158,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;");
setText(text); setText(text);
} }
} }
......
...@@ -138,7 +138,6 @@ ...@@ -138,7 +138,6 @@
-fx-background-color: @basenavy; -fx-background-color: @basenavy;
// -fx-background-color: @base3; // -fx-background-color: @base3;
-fx-font-family: "Inconsolata", monospace; -fx-font-family: "Inconsolata", monospace;
//-fx-font-family: "Fira Code Medium", monospace;
-fx-font-size: 12pt; -fx-font-size: 12pt;
-fx-fill: @base01; -fx-fill: @base01;
...@@ -181,8 +180,6 @@ ...@@ -181,8 +180,6 @@
.LINE_COMMENT, .COMMENT { .LINE_COMMENT, .COMMENT {
-fx-fill: @base01; -fx-fill: @base01;
//-fx-font-family: "Fira Code Light", monospace;
-fx-font-family: "Inconsolata", monospace;
} }
.Identifier { .Identifier {
......
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