Skip to content
Snippets Groups Projects
Commit 7518acb1 authored by Sebastian Krings's avatar Sebastian Krings
Browse files

show counterexample found on selected hypotheses

parent 32161a10
No related branches found
No related tags found
No related merge requests found
...@@ -4,6 +4,9 @@ import java.util.HashSet; ...@@ -4,6 +4,9 @@ import java.util.HashSet;
import java.util.Set; import java.util.Set;
import org.eclipse.core.runtime.Status; 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.IEventBProject;
import org.eventb.core.IPOSequent; import org.eventb.core.IPOSequent;
import org.eventb.core.ast.Predicate; import org.eventb.core.ast.Predicate;
...@@ -183,6 +186,15 @@ public class DisproverReasoner implements IReasoner { ...@@ -183,6 +186,15 @@ public class DisproverReasoner implements IReasoner {
System.out.println(sequent.toString() System.out.println(sequent.toString()
+ ": Counter-Example for selected hypotheses found."); + ": 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 return ProverFactory
.reasonerFailure( .reasonerFailure(
this, this,
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment