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 07a86b19e6518bdc58060e22a710135d7c4d9f55..2b07c49ed0dda8288ec83e0794097a486adc8b14 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 @@ -136,7 +136,7 @@ public class DebuggerMain implements Initializable { //----------------------------------------------------------------------------------------------------------------- private ProofTree proofTree = new ProofTree(); private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree"); - private WelcomePane welcomePane = new WelcomePane(this); + private WelcomePaneFMEdition welcomePane = new WelcomePaneFMEdition(this); private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT)); private DockNode activeInspectorDock; private CommandHelp commandHelp = new CommandHelp(); @@ -442,9 +442,8 @@ public class DebuggerMain implements Initializable { // wait a second! future.get(1, TimeUnit.SECONDS); - // ungently stop + // urgently stop model.getDebuggerFramework().hardStop(); - } catch (InterruptedException | ExecutionException | TimeoutException e) { e.printStackTrace(); } finally { @@ -453,6 +452,7 @@ public class DebuggerMain implements Initializable { } else { LOGGER.info("no interpreter running"); } + assert model.getDebuggerFramework() == null; } @FXML diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java index 91669da10859a6ac0162b72378465655f70b01b3..23c23fbc06aa9bd3df27e85fc62d0d37fac80adb 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java @@ -17,6 +17,7 @@ import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea; import edu.kit.iti.formal.psdbg.gui.controls.ScriptController; import edu.kit.iti.formal.psdbg.gui.controls.Utils; import edu.kit.iti.formal.psdbg.gui.model.InspectionModel; +import edu.kit.iti.formal.psdbg.interpreter.Evaluator; 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.VariableAssignment; @@ -25,6 +26,7 @@ import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode; import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException; import edu.kit.iti.formal.psdbg.parser.PrettyPrinter; import edu.kit.iti.formal.psdbg.parser.ast.*; +import edu.kit.iti.formal.psdbg.parser.data.Value; import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade; import edu.kit.iti.formal.psdbg.termmatcher.Matchings; import javafx.beans.property.BooleanProperty; @@ -68,6 +70,8 @@ public class InteractiveModeController { private Proof currentProof; private Services keYServices; + private boolean moreThanOneMatch = false; + public void start(Proof currentProof, InspectionModel model) { Events.register(this); cases.clear(); @@ -134,7 +138,9 @@ public class InteractiveModeController { @Subscribe public void handle(Events.TacletApplicationEvent tap) { + LOGGER.debug("Handling {}", tap); + moreThanOneMatch = false; String tapName = tap.getApp().taclet().displayName(); Goal g = tap.getCurrentGoal(); @@ -147,18 +153,16 @@ public class InteractiveModeController { Parameters params = new Parameters(); params.put(new Variable("formula"), new TermLiteral(term)); - /* if(matches.size() > 1) { - System.out.println("matches = " + matches); + if (matches.size() > 1) { + moreThanOneMatch = true; + params.put(new Variable("occ"), new StringLiteral("0")); - Integer integ = new Integer(tap.getPio().sequentFormula().formula().serialNumber()); - System.out.println("integ = " + integ); - params.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(integ))); - - }*/ + } VariableAssignment va = new VariableAssignment(null); CallStatement call = new CallStatement(tapName, params); try { + applyRule(call, g); // Insert into the right cases Node currentNode = g.node(); @@ -182,6 +186,7 @@ public class InteractiveModeController { } + private Node findRoot(Node cur) { while (cur != null) { if (cases.keySet().contains(cur)) @@ -237,8 +242,16 @@ public class InteractiveModeController { } RuleCommand c = new RuleCommand(); // KeyData kd = g.getData(); + Evaluator eval = new Evaluator(expandedNode.getAssignments(), expandedNode); + Map map = new HashMap<>(); - // call.getParameters().forEach((k, v) -> map.put(k.getIdentifier(), v.getData().toString())); + call.getParameters().forEach((variable, expression) -> { + + Value exp = eval.eval(expression); + map.put(variable.getIdentifier(), exp.getData().toString()); + }); + +// call.getParameters().forEach((k, v) -> map.put(k.getIdentifier(),)); LOGGER.info("Execute {} with {}", call, map); try { KeyData kd = expandedNode.getData(); @@ -246,6 +259,7 @@ public class InteractiveModeController { EngineState estate = new EngineState(g.proof()); estate.setGoal(g); RuleCommand.Parameters cc = c.evaluateArguments(estate, map); //reflection exception + AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl(); c.execute(uiControl, cc, estate); @@ -286,4 +300,6 @@ public class InteractiveModeController { public void setKeYServices(Services keYServices) { this.keYServices = keYServices; } + + } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePaneFMEdition.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePaneFMEdition.java index 6a91a47d68de34d03cd116942a1ea5ed0d6f54a4..f8b97240cea158c31e934ba3a2c8501fef992ab3 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePaneFMEdition.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePaneFMEdition.java @@ -45,13 +45,18 @@ public class WelcomePaneFMEdition extends AnchorPane { * Load a test example * @param event */ - public void loadJavaTest(ActionEvent event) { + public void loadQuicksort(ActionEvent event) { proofScriptDebugger.getWelcomePaneDock().close(); proofScriptDebugger.showActiveInspector(null); + Examples.loadExamples().forEach(example -> { + if (example.getName().equals("Quicksort example")) { + example.open(proofScriptDebugger); + } + }); } /** - * Load teh help page documentation + * Load the help page documentation * @param event */ public void loadHelpPage(ActionEvent event) { diff --git a/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example b/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example index 083208ea36703ba3935b9f1eeb83e9439e09f44d..8d2d49e1d4e36d945b71a5215bdffe59423401f7 100644 --- a/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example +++ b/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example @@ -1,12 +1,6 @@ edu.kit.iti.formal.psdbg.examples.contraposition.ContrapositionExample edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample -edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample -edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample -edu.kit.iti.formal.psdbg.examples.java.dpqs.DualPivotExample edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample -edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample -edu.kit.iti.formal.psdbg.examples.java.sumAndMax.SumAndMaxExample -edu.kit.iti.formal.psdbg.examples.lulu.LuLuDoubleLinkedList -edu.kit.iti.formal.psdbg.examples.lulu.LuLuQuickSort -edu.kit.iti.formal.psdbg.examples.lulu.LuLuSumAndMax +edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample + diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps index dc126d6d558931c16cc01be62d9797b4589cdfbc..bbf483791605a2e9a174306ad885a64dbb905168 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps @@ -14,8 +14,8 @@ script split_from_quicksort() { case match `==> seqDef(_,_,_) = seqDef(_, _, _)`: auto; case match `==> (\exists ?X (\exists ?Y _))`: - instantiate var=`?X`[?X \ X] with=`i_0`; - instantiate var=`?Y`[?Y \ Y] with=`j_0`; + instantiate var=X with=`i_0`; + instantiate var=Y with=`j_0`; auto; } } diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/Test.java b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/Test.java index c2eeb1e23ede3ea42587e0eb08c4d9382db1e724..6e0dc98fc4f4f004b05249c4bcd29f42058d5876 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/Test.java +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/Test.java @@ -12,6 +12,6 @@ public class Test{ }else{ x++; } - return x++; + return ++x; } } \ No newline at end of file diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps index 395b1ea3c8085f51329f59a9823701b965d4a413..9508c7793009326b1b343ff02d98702fc4b368f7 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps @@ -1,10 +1,17 @@ script t1(){ symbex; - cases{ - case match `?X >= 0,?X > 0 ==>`: - cut `?X = 0`[?X \ X]; - foreach{ - auto; - } + foreach{ + onestep; + andRight; + foreach{ + tryclose; + } } +// cases{ +// case match `?X >= 0,?X > 0 ==>`: +// cut `?X = 0`[?X \ X]; +// foreach{ +// auto; +// } +// } } diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/WelcomePaneFMEdition.fxml b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/WelcomePaneFMEdition.fxml index ac322fd7722d71412ad8e64c41321ef32416f520..1741624aed86184aa904312b628a16319e95c224 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/WelcomePaneFMEdition.fxml +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/WelcomePaneFMEdition.fxml @@ -7,18 +7,23 @@ - - - + + + + + + + +