From 25a82e39620de1eff38f9fc8a467b783809a0018 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Thu, 16 Oct 2014 14:26:57 +0200
Subject: [PATCH] backport 7518acb1379bec986f21ff3e059f4847aa60216b
---
.../disprover/core/internal/DisproverReasoner.java | 13 ++++++++++++-
1 file changed, 12 insertions(+), 1 deletion(-)
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 2f935d43..391b76d8 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
@@ -3,6 +3,9 @@ package de.prob.eventb.disprover.core.internal;
import java.util.*;
import org.eclipse.core.runtime.Status;
+import org.eclipse.jface.dialogs.MessageDialog;
+import org.eclipse.swt.widgets.Shell;
+import org.eclipse.ui.PlatformUI;
import org.eventb.core.*;
import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.*;
@@ -167,6 +170,15 @@ public class DisproverReasoner implements IReasoner {
System.out.println(sequent.toString()
+ ": Counter-Example for selected hypotheses found.");
+ Shell activeShell = PlatformUI.getWorkbench()
+ .getActiveWorkbenchWindow().getShell();
+ MessageDialog
+ .openWarning(
+ activeShell,
+ "Goal not provable",
+ "ProB found a Counter-Example for the selected Hypotheses, Goal not provable from selected Hypotheses but may be provable with all Hypotheses.\n"
+ + counterExample.toString());
+
return ProverFactory
.reasonerFailure(
this,
@@ -189,5 +201,4 @@ public class DisproverReasoner implements IReasoner {
public void serializeInput(final IReasonerInput input,
final IReasonerInputWriter writer) throws SerializeException {
}
-
}
--
GitLab