From 50bf82f868e5358a61a371f140f7669c933fb90b Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Sun, 29 Nov 2020 09:30:53 +0100
Subject: [PATCH] add Disprover counter-example output
---
.../de/prob/eventb/disprover/core/DisproverReasoner.java | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
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 11473462..eb881e5f 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
@@ -122,7 +122,7 @@ public class DisproverReasoner implements IReasoner {
ICounterExample counterExample = DisproverCommand.disprove(
Animator.getAuxAnimator(), evbProject, allHypotheses,
selectedHypotheses, goal, timeoutFactor, context, pm);
- // Logger.info("Disprover: Result: " + counterExample.toString());
+ Logger.info("Disprover: Result: " + counterExample.toString());
return counterExample;
}
@@ -197,12 +197,12 @@ public class DisproverReasoner implements IReasoner {
&& counterExample.onlySelectedHypotheses()) {
System.out.println(sequent.toString()
+ ": Counter-Example for selected hypotheses found.");
-
+ Sysemt.out.println(counterExample.toString());
return ProverFactory
.reasonerFailure(
this,
input,
- "ProB: Counter-Example for selected Hypotheses found, Goal not provable from selected Hypotheses (may be provable with all Hypotheses)");
+ "ProB: Counter-Example to Goal for selected Hypotheses found (may be provable with all Hypotheses): " + counterExample.toString()); // use abbreviate or substring(0, Math.min(s.length(), 100));
}
System.out.println(sequent.toString() + ": Counter-Example found.");
--
GitLab