diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/ICounterExample.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/ICounterExample.java index b52efb835f3d41d4170d862bbe820b8aec72253c..b2f3ab9e5f0561850323e0c2d842013954f82860 100644 --- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/ICounterExample.java +++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/ICounterExample.java @@ -6,8 +6,6 @@ public interface ICounterExample { public boolean timeoutOccured(); - public String getMessage(); - public boolean isProof(); } \ No newline at end of file diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/CounterExample.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/CounterExample.java index 5abd50a5324f7ff746bf11810d3fc1ce51f838a2..c7f786b090fb2426fde60f822e064e09fc12875a 100644 --- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/CounterExample.java +++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/CounterExample.java @@ -26,6 +26,7 @@ class CounterExample implements ICounterExample { this.timeoutOccured = timeoutOccured; } + @Override public boolean isProof() { return proof; } @@ -34,29 +35,29 @@ class CounterExample implements ICounterExample { this.proof = proof; } - /* - * (non-Javadoc) - * - * @see de.prob.eventb.disprover.core.internal.ICounterExample#getMessage() - */ - public String getMessage() { - return counterExampleFound ? state.toString() - : "Counter-Example does not exists."; - } - + @Override public boolean counterExampleFound() { return counterExampleFound; } @Override public String toString() { - return getMessage(); + if (counterExampleFound) { + return state.toString(); + } else { + if (isProof()) { + return "No Counter-Example exists."; + } else { + return "No Counter-Example found."; + } + } } void addVar(String name, String value) { state.put(name, value); } + @Override public boolean timeoutOccured() { return timeoutOccured; }