From 86727c0511e2c297c9df2c4bd07b89772693bc17 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Fri, 14 Mar 2014 09:59:52 +0100
Subject: [PATCH] add output to disprover
---
.../core/internal/DisproverReasoner.java | 20 +++++++++++++++----
1 file changed, 16 insertions(+), 4 deletions(-)
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java
index dac3f05e..d8a105cc 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java
@@ -133,31 +133,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);
}
--
GitLab