diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java index 2270dc2d7b930634c06945c154f491c05adfec0e..8921c211d07660d93f00908d14b25c73a7fe7328 100644 --- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java +++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java @@ -134,31 +134,43 @@ public class DisproverReasoner implements IReasoner { IAntecedent ante = ProverFactory.makeAntecedent(goal); - if (counterExample.timeoutOccured()) + if (counterExample.timeoutOccured()) { + System.out.println(sequent.toString() + ": Timeout occured."); return ProverFactory.reasonerFailure(this, input, "ProB: Timeout occurred."); + } - if (!counterExample.counterExampleFound() && counterExample.isProof()) + if (!counterExample.counterExampleFound() && counterExample.isProof()) { + System.out.println(sequent.toString() + ": Proof."); return ProverFactory.makeProofRule(this, input, sequent.goal(), null, IConfidence.DISCHARGED_MAX, "ProB (no enumeration / all cases checked)"); + } + + if (!counterExample.counterExampleFound()) { + System.out.println(sequent.toString() + ": Unsure."); - if (!counterExample.counterExampleFound()) return ProverFactory.reasonerFailure( this, input, "ProB: No Counter-Example found due to " + counterExample.getReason() + ", but there might exist one."); + } if (counterExample.counterExampleFound() - && counterExample.onlySelectedHypotheses()) + && counterExample.onlySelectedHypotheses()) { + System.out.println(sequent.toString() + + ": Counter-Example for selected hypotheses found."); + return ProverFactory .reasonerFailure( this, input, "ProB: Counter-Example for selected Hypotheses found, Goal not provable from selected Hypotheses (may be provable with all Hypotheses)"); + } + System.out.println(sequent.toString() + ": Counter-Example found."); return ProverFactory.makeProofRule(this, input, null, null, IConfidence.PENDING, counterExample.toString(), ante); } diff --git a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverPreferences.java b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverPreferences.java index 6e32ed679ff21cbb8c92d9bfb4625100ba2da458..f2f8e38d7705276fa88e8d607295f8b5e142bc27 100644 --- a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverPreferences.java +++ b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverPreferences.java @@ -66,6 +66,7 @@ public class DisproverPreferences extends PreferencePage implements timeoutTextField = new Text(pageComponent, SWT.NONE); int timeout = prefNode.getInt("timeout", 1000); timeoutTextField.setText(Integer.toString(timeout)); + timeoutTextField.setSize(100, timeoutTextField.getSize().y); timeoutTextField.addVerifyListener(new VerifyListener() { @Override public void verifyText(VerifyEvent e) {