From 03be4306f160281e7eda7b90662d6a19922e031a Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Wed, 31 Jan 2018 08:13:52 +0100 Subject: [PATCH] minor bugfix concerning services --- .../formal/psdbg/interpreter/KeYMatcher.java | 23 ++-- .../formal/psdbg/commands/instantiate.html | 1 + .../lulu/bigIntProof/BigIntExample.java | 6 +- .../psdbg/gui/controller/DebuggerMain.java | 117 ++++++++++-------- .../controller/InteractiveModeController.java | 17 +-- .../formal/psdbg/gui/controls/JavaArea.java | 10 +- .../psdbg/gui/controls/TacletContextMenu.java | 1 - .../psdbg/gui/model/InspectionModel.java | 3 + .../edu.kit.iti.formal.psdbg.examples.Example | 3 +- .../psdbg/examples/contraposition/script.kps | 2 +- 10 files changed, 94 insertions(+), 89 deletions(-) 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 85ddd1fd..8c473c6e 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 @@ -160,16 +160,6 @@ public class KeYMatcher implements MatcherApi { return assignments.isEmpty()? null: assignments; } - private Value toValueTerm(KeyData currentState, Term matched) { - String reprTerm = LogicPrinter.quickPrintTerm(matched, currentState.getEnv().getServices()); - //Hack: to avoid newlines - String reprTermReformatted = reprTerm.trim(); - return new Value<>( - new TermType(new SortType(matched.sort())), - reprTermReformatted - ); - } - @Override public List matchSeq(GoalNode currentState, String data, @@ -178,7 +168,7 @@ public class KeYMatcher implements MatcherApi { //System.out.println("Signature " + sig.toString()); Matchings m = MatcherFacade.matches(data, - currentState.getData().getNode().sequent(), false, services); + currentState.getData().getNode().sequent(), false, currentState.getData().getProof().getServices()); if (m.isEmpty()) { LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent()); @@ -208,6 +198,17 @@ public class KeYMatcher implements MatcherApi { } } + private Value toValueTerm(KeyData currentState, Term matched) { + + String reprTerm = LogicPrinter.quickPrintTerm(matched, currentState.getProof().getServices()); + //Hack: to avoid newlines + String reprTermReformatted = reprTerm.trim(); + return new Value<>( + new TermType(new SortType(matched.sort())), + reprTermReformatted + ); + } + //private TermLiteral from(SequentFormula sf) { // return new TermLiteral(sf.toString()); diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html index 49e15256..22235c8c 100644 --- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html @@ -16,5 +16,6 @@
  • occ : INT occurence of the top-level formula
  • with : TERM the term with which variables should be instantiated
    • + \ No newline at end of file diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/lulu/bigIntProof/BigIntExample.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/lulu/bigIntProof/BigIntExample.java index 364f3bb6..f9cbb90e 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/lulu/bigIntProof/BigIntExample.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/lulu/bigIntProof/BigIntExample.java @@ -1,9 +1,11 @@ package edu.kit.iti.formal.psdbg.examples.lulu.bigIntProof; -import edu.kit.iti.formal.psdbg.examples.JavaExample; +import edu.kit.iti.formal.psdbg.examples.Example; -public class BigIntExample extends JavaExample { +public class BigIntExample extends Example { public BigIntExample() { + setName("BigInt"); + defaultInit(getClass()); } } 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 0a3a0a64..891583d9 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 @@ -428,31 +428,50 @@ public class DebuggerMain implements Initializable { executeScript(FACADE.buildInterpreter(), addInitBreakpoint); } + /** + * Reload a problem from the beginning + * + * @param event + */ @FXML - public void abortExecution() { - - if (model.getDebuggerFramework() != null) { - try { - // try to friendly - Future future = executorService.submit(() -> { - model.getDebuggerFramework().stop(); - model.getDebuggerFramework().unregister(); - model.getDebuggerFramework().release(); - }); + public void reloadProblem(ActionEvent event) { + //abort current execution(); + //save old information and refresh models + statusBar.publishMessage("Reloading..."); + File lastLoaded; + if (model.getKeyFile() != null) { + lastLoaded = model.getKeyFile(); + } else { + Contract chosen = model.getChosenContract(); + lastLoaded = model.getJavaFile(); + } + //model.reload(); + abortExecution(); + handleStatePointerUI(null); + model.setStatePointer(null); + //reload getInspectionViewsController().getActiveInspectionViewTab().getModel() + InspectionModel iModel = getInspectionViewsController().getActiveInspectionViewTab().getModel(); + //iModel.setHighlightedJavaLines(FXCollections.emptyObservableSet()); + iModel.clearHighlightLines(); + iModel.getGoals().clear(); + iModel.setSelectedGoalNodeToShow(null); - // wait a second! - future.get(1, TimeUnit.SECONDS); - // urgently stop - model.getDebuggerFramework().hardStop(); - } catch (InterruptedException | ExecutionException | TimeoutException e) { - e.printStackTrace(); - } finally { - model.setDebuggerFramework(null); + try { + FACADE.reload(lastLoaded); + if (iModel.getGoals().size() > 0) { + iModel.setSelectedGoalNodeToShow(iModel.getGoals().get(0)); } - } else { - LOGGER.info("no interpreter running"); + if (FACADE.getReadyToExecute()) { + LOGGER.info("Reloaded Successfully"); + statusBar.publishMessage("Reloaded Sucessfully"); + } + } catch (ProofInputException e) { + e.printStackTrace(); + } catch (ProblemLoaderException e) { + e.printStackTrace(); } - assert model.getDebuggerFramework() == null; + + } @FXML @@ -768,44 +787,32 @@ public class DebuggerMain implements Initializable { } } - /** - * Reload a problem from the beginning - * - * @param event - */ @FXML - public void reloadProblem(ActionEvent event) { - //abort current execution(); - //save old information and refresh models - File lastLoaded; - if (model.getKeyFile() != null) { - lastLoaded = model.getKeyFile(); - } else { - Contract chosen = model.getChosenContract(); - lastLoaded = model.getJavaFile(); - } - //model.reload(); - abortExecution(); - handleStatePointerUI(null); - model.setStatePointer(null); - //reload getInspectionViewsController().getActiveInspectionViewTab().getModel() - InspectionModel iModel = getInspectionViewsController().getActiveInspectionViewTab().getModel(); - iModel.setHighlightedJavaLines(null); - iModel.getGoals().clear(); - iModel.setSelectedGoalNodeToShow(null); + public void abortExecution() { + statusBar.publishMessage("Aborting Execution..."); + if (model.getDebuggerFramework() != null) { + try { + // try to friendly + Future future = executorService.submit(() -> { + model.getDebuggerFramework().stop(); + model.getDebuggerFramework().unregister(); + model.getDebuggerFramework().release(); + }); - try { - FACADE.reload(lastLoaded); - if (iModel.getGoals().size() > 0) { - iModel.setSelectedGoalNodeToShow(iModel.getGoals().get(0)); + // wait a second! + future.get(1, TimeUnit.SECONDS); + // urgently stop + model.getDebuggerFramework().hardStop(); + } catch (InterruptedException | ExecutionException | TimeoutException e) { + e.printStackTrace(); + } finally { + model.setDebuggerFramework(null); + statusBar.publishMessage("Execution aborted."); } - } catch (ProofInputException e) { - e.printStackTrace(); - } catch (ProblemLoaderException e) { - e.printStackTrace(); + } 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 dc68727d..e809d0c8 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 @@ -55,6 +55,7 @@ public class InteractiveModeController { private static final Logger LOGGER = LogManager.getLogger(InteractiveModeController.class); private final Map cases = new HashMap<>(); + private final ScriptController scriptController; private BooleanProperty activated = new SimpleBooleanProperty(); private ScriptArea scriptArea; @@ -151,19 +152,6 @@ public class InteractiveModeController { String sfTerm = LogicPrinter.quickPrintTerm(seqForm.formula(), keYServices, false, false); String onTerm = LogicPrinter.quickPrintTerm(tap.getPio().subTerm(), keYServices, false, false); - //String sfTerm = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(seqForm.formula()); -// String onTerm = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(tap.getPio().subTerm()); - - //check whether more than one possibility for match - //Matchings matches = MatcherFacade.matches(term, seq, true, keYServices); - - /*Parameters params = new Parameters(); - params.put(new Variable("formula"), new TermLiteral(term)); - if (matches.size() > 1) { - moreThanOneMatch = true; - params.put(new Variable("occ"), new StringLiteral("0")); - - }*/ RuleCommand.Parameters params = new RuleCommand.Parameters(); params.formula = seqForm.formula(); @@ -174,7 +162,6 @@ public class InteractiveModeController { int occ = rch.getOccurence(tap.getApp()); Parameters callp = new Parameters(); -// callp.put(new Variable("formula"), new TermLiteral(sfTerm)); callp.put(new Variable("formula"), new TermLiteral(sfTerm)); callp.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(occ))); callp.put(new Variable("on"), new TermLiteral(onTerm)); @@ -297,6 +284,8 @@ public class InteractiveModeController { if (ngoals.size() > 1) { cases.get(findRoot(ngoals.get(0).node())).add(call); + cases.get(findRoot(ngoals.get(0).node())).add(new CasesStatement()); + for (Goal newGoalNode : ngoals) { KeyData kdn = new KeyData(kd, newGoalNode.node()); goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed())); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/JavaArea.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/JavaArea.java index 66a1cde5..80d9d78e 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/JavaArea.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/JavaArea.java @@ -56,10 +56,12 @@ public class JavaArea extends BaseCodeArea { * highlight new lines */ private void highlightLineSet() { - linesToHighlightProperty().get().forEach(integer -> { - lineToClassProperty().get().put(integer - 1, "line-highlight"); - }); - highlightLines(); + if (!linesToHighlight.get().isEmpty()) { + linesToHighlightProperty().get().forEach(integer -> { + lineToClassProperty().get().put(integer - 1, "line-highlight"); + }); + highlightLines(); + } } private void updateView() { diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java index 8570282a..285aae31 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java @@ -119,7 +119,6 @@ public class TacletContextMenu extends ContextMenu { try { ImmutableList findTaclet = c.getFindTaclet(goal, occ); - createTacletMenu( removeRewrites(findTaclet) .prepend(c.getRewriteTaclet(goal, occ)), diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java index 707e4081..907a78f1 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/InspectionModel.java @@ -162,6 +162,9 @@ public class InspectionModel { return isInterpreterTab; } + public void clearHighlightLines() { + highlightedJavaLinesProperty().clear(); + } enum Mode { LIVING, DEAD, POSTMORTEM, 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 3c068a80..b1e6b008 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 @@ -9,4 +9,5 @@ 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 \ No newline at end of file +edu.kit.iti.formal.psdbg.examples.lulu.LuLuSumAndMax +#edu.kit.iti.formal.psdbg.examples.lulu.bigIntProof.BigIntExample \ No newline at end of file diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps index a4c26edc..94214654 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps @@ -2,7 +2,7 @@ // script autoScript(){ - auto; + //auto; } script interactive(){ -- GitLab