From 7518acb1379bec986f21ff3e059f4847aa60216b Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Mon, 13 Oct 2014 11:24:32 +0200
Subject: [PATCH] show counterexample found on selected hypotheses
---
.../eventb/disprover/core/DisproverReasoner.java | 12 ++++++++++++
1 file changed, 12 insertions(+)
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 08d81201..5e834b9c 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
@@ -4,6 +4,9 @@ import java.util.HashSet;
import java.util.Set;
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.IEventBProject;
import org.eventb.core.IPOSequent;
import org.eventb.core.ast.Predicate;
@@ -183,6 +186,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,
--
GitLab