From ae65b9b4767f251b1f4bf68f67a7a8a9ed2f36d2 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Thu, 18 Apr 2013 15:53:44 +0200
Subject: [PATCH] refactored counter example

---
 .../disprover/core/ICounterExample.java       |  2 --
 .../core/internal/CounterExample.java         | 23 ++++++++++---------
 2 files changed, 12 insertions(+), 13 deletions(-)

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 b52efb83..b2f3ab9e 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 5abd50a5..c7f786b0 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;
 	}
-- 
GitLab