diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java index 2f11a4b341314bfb716d26884cd49c74bed766af..841925dff03736a3319982d83616d5c9e92a0bbc 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java @@ -207,7 +207,9 @@ public class KeYMatcher implements MatcherApi { public List matchSeq(GoalNode currentState, String data, Signature sig) { System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data); System.out.println("Signature " + sig.toString()); + Matchings m = MatcherFacade.matches(data, currentState.getData().getNode().sequent()); + if (m.isEmpty()) { return Collections.emptyList(); } else { @@ -217,8 +219,13 @@ public class KeYMatcher implements MatcherApi { MatchPath matchPath = firstMatch.get(s); if (!s.equals("EMPTY_MATCH")) { Term matched = (Term) matchPath.getUnit(); + if (s.startsWith("?")) { + + s = s.replaceFirst("\\?", ""); + } va.declare(s, new TermType()); va.assign(s, Value.from(from(matched))); + System.out.println("Variable " + s + " : " + Value.from(from(matched))); } } List retList = new LinkedList(); diff --git a/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/cutTest.kps b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/cutTest.kps index 70d56ef962708d1e06ca04b350dd8af2fcd755a3..dd94fde7e491128ea2a6ebeb397d80ded01b85ed 100644 --- a/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/cutTest.kps +++ b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/cutTest.kps @@ -1,3 +1,8 @@ script cutTest(){ - cut #2=`p`; + cases{ + case match `==>?X -> ?Y`: + + } + //cut #2=`p`; + //auto steps=100; } \ No newline at end of file diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/DefaultLookup.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/DefaultLookup.java index 5e3b19232edf1743ec937c3bde6d50764aef51ef..56fad40b069f4ec9a395eb17120399dd8ad48ecd 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/DefaultLookup.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/DefaultLookup.java @@ -52,7 +52,13 @@ public class DefaultLookup implements CommandLookup { if (found == null) { found = b; } 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."); } } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/InterpretingService.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/InterpretingService.java index 52476c860c31bbaf6212de646acc38bb7b3decd1..74fa68539c9f510dc65ec05f02bb9d8e12e3c332 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/InterpretingService.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/InterpretingService.java @@ -1,6 +1,7 @@ package edu.kit.iti.formal.psdbg; 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.interpreter.Interpreter; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; @@ -17,11 +18,11 @@ import javafx.concurrent.Task; * @author A. Weigl */ public class InterpretingService extends Service> { - /** - * 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 = new SimpleObjectProperty<>(); + private DebuggerStatusBar statusBar; /** * The main script that is traversed @@ -41,6 +42,12 @@ public class InterpretingService extends Service> { this.blocker = blocker; } + + public InterpretingService(PuppetMaster blocker, DebuggerStatusBar statusBar) { + this.blocker = blocker; + this.statusBar = statusBar; + } + public SimpleBooleanProperty hasRunSucessfullyProperty() { return hasRunSucessfully; } @@ -70,6 +77,9 @@ public class InterpretingService extends Service> { //currentGoals.set(state.getGoals()); //currentSelectedGoal.set(state.getSelectedGoalNode()); System.out.println("Updating View"); + if (statusBar != null) { + statusBar.stopProgress(); + } blocker.publishState(); } @@ -87,6 +97,9 @@ public class InterpretingService extends Service> { */ @Override protected edu.kit.iti.formal.psdbg.interpreter.data.State call() throws Exception { + if (statusBar != null) { + statusBar.indicateProgress(); + } i.interpret(ast); return i.peekState(); } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java index bf74e571b2c1a52f3347cb5c6f85072cdfe9a4ff..3d9bc4f4597dbbbae04da50572ce770d47b40e06 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java @@ -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 */ private void registerToolbarToStatusBar() { + /*toolbar.getChildrenUnmodifiable().forEach( n -> n.setOnMouseEntered(statusBar.getTooltipHandler())); @@ -176,6 +177,7 @@ public class DebuggerMain implements Initializable { proofTreeController.currentGoalsProperty().addListener((o, old, fresh) -> { if (fresh != null) { imodel.setGoals(fresh); + } else { // no goals, set an empty list imodel.setGoals(FXCollections.observableArrayList()); @@ -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) -> { scriptController.getMainScript().getScriptArea().removeExecutionMarker(); LineMapping lm = new LineMapping(scriptController.getMainScript().getScriptArea().getText()); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java index 00cff705e948e0f398400d16cc9e2a4c083667a6..cac2e370cb1f8f0e770330c597c8078bc61d615f 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java @@ -280,7 +280,7 @@ public class ProofTreeController { this.stateGraphWrapper.install(currentInterpreter); this.stateGraphWrapper.addChangeListener(graphChangedListener); - + statusBar.stopProgress(); blocker.getStepUntilBlock().set(1); } @@ -292,9 +292,10 @@ public class ProofTreeController { interpreterService.interpreterProperty().set(currentInterpreter); interpreterService.mainScriptProperty().set(mainScript.get()); + interpreterService.start(); interpreterService.setOnSucceeded(event -> { - statusBar.setText("Executed script until end of script."); + statusBar.setText("Executed until end of script."); statusBar.stopProgress(); }); interpreterService.setOnFailed(event -> { diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/DebuggerStatusBar.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/DebuggerStatusBar.java index 2f55dc3188ac720a76483158329115606826691c..812513531d882df15ca20de992337e911698719f 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/DebuggerStatusBar.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/DebuggerStatusBar.java @@ -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.model.MainScriptIdentifier; +import javafx.beans.property.IntegerProperty; import javafx.beans.property.ObjectProperty; +import javafx.beans.property.SimpleIntegerProperty; import javafx.beans.property.SimpleObjectProperty; import javafx.event.EventHandler; import javafx.scene.control.Control; @@ -26,12 +28,8 @@ public class DebuggerStatusBar extends StatusBar { //private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX(); private ObjectProperty mainScriptIdentifier = new SimpleObjectProperty<>(); - private Label lblCurrentNodes = new Label("#nodes: %s"); - private Label lblMainscript = new Label(); - private ProgressIndicator progressIndicator = new ProgressIndicator(); - private EventHandler toolTipHandler = event -> { - publishMessage(((Control) event.getTarget()).getTooltip().getText()); - }; + + private IntegerProperty numberOfGoals = new SimpleIntegerProperty(0); public DebuggerStatusBar() { //listenOnField("psdbg"); @@ -47,7 +45,9 @@ public class DebuggerStatusBar extends StatusBar { contextMenu.show(this, event.getScreenX(), event.getScreenY()); } });*/ - + numberOfGoals.addListener((observable, oldValue, newValue) -> { + lblCurrentNodes.setText("#nodes: " + newValue); + }); mainScriptIdentifier.addListener((ov, o, n) -> { if (n != null) { @@ -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 toolTipHandler = event -> { + publishMessage(((Control) event.getTarget()).getTooltip().getText()); + }; + + public IntegerProperty numberOfGoalsProperty() { + return numberOfGoals; + } + /* private Appender createAppender() { PatternLayout layout = PatternLayout.createDefaultLayout(); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java index 1e6c882de5e014edb252d108dc52d340f5e92418..c53f20c179186b982fc3d287c1893d574adfeeb3 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java @@ -158,6 +158,7 @@ public class InspectionView extends BorderPane { if (goalOptionsMenu.getSelectedViewOption() != null) { text = goalOptionsMenu.getSelectedViewOption().getText(item); } + //setStyle("-fx-font-size: 12pt;"); setText(text); } } diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less index aa22779391c9f814f3e22255368f8d58d6969ead..f650d2b79347d0ac686c993effe31cde2536b708 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less @@ -138,7 +138,6 @@ -fx-background-color: @basenavy; // -fx-background-color: @base3; -fx-font-family: "Inconsolata", monospace; - //-fx-font-family: "Fira Code Medium", monospace; -fx-font-size: 12pt; -fx-fill: @base01; @@ -181,8 +180,6 @@ .LINE_COMMENT, .COMMENT { -fx-fill: @base01; - //-fx-font-family: "Fira Code Light", monospace; - -fx-font-family: "Inconsolata", monospace; } .Identifier {