From 6bb071105c9117f018c9f212d2d76378853af5a8 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Tue, 3 Jun 2014 14:57:40 +0200
Subject: [PATCH] add missing case (PROBPLUGIN-103)
---
.../core/command/ConstraintBasedAssertionCheckCommand.java | 6 ++++--
.../prob/ui/assertion/AssertionCheckFinishedListener.java | 7 ++++++-
2 files changed, 10 insertions(+), 3 deletions(-)
diff --git a/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java b/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java
index 5b17b630..31439404 100644
--- a/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java
+++ b/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java
@@ -18,7 +18,7 @@ import de.prob.prolog.term.PrologTerm;
public class ConstraintBasedAssertionCheckCommand implements IComposableCommand {
public static enum ResultType {
- INTERRUPTED, COUNTER_EXAMPLE, NO_COUNTER_EXAMPLE
+ INTERRUPTED, COUNTER_EXAMPLE, NO_COUNTER_EXAMPLE_FOUND, NO_COUNTER_EXAMPLE_EXISTS
};
private static final String COMMAND_NAME = "cbc_static_assertion_violation_checking";
@@ -59,7 +59,9 @@ public class ConstraintBasedAssertionCheckCommand implements IComposableCommand
if (resultTerm.hasFunctor("interrupted", 0)) {
result = ResultType.INTERRUPTED;
} else if (resultTerm.hasFunctor("no_counterexample_found", 0)) {
- result = ResultType.NO_COUNTER_EXAMPLE;
+ result = ResultType.NO_COUNTER_EXAMPLE_FOUND;
+ } else if (resultTerm.hasFunctor("no_counterexample_exists", 0)) {
+ result = ResultType.NO_COUNTER_EXAMPLE_EXISTS;
} else if (resultTerm.hasFunctor("counterexample_found", 2)) {
result = ResultType.COUNTER_EXAMPLE;
CompoundPrologTerm counterExampleTerm = (CompoundPrologTerm) resultTerm;
diff --git a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java
index 876a6b17..4f8826d8 100644
--- a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java
+++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java
@@ -47,7 +47,12 @@ public class AssertionCheckFinishedListener extends ProBJobFinishedListener {
message = "ProB did not return a result";
} else {
switch (result) {
- case NO_COUNTER_EXAMPLE:
+ case NO_COUNTER_EXAMPLE_EXISTS:
+ dialogType = MessageDialog.INFORMATION;
+ dialogTitle = "No Counter-Example Exists";
+ message = "No Counter-Example to the Context Theorems exists.";
+ break;
+ case NO_COUNTER_EXAMPLE_FOUND:
dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Counter-Example Found";
message = "No Counter-Example to the Context Theorems was found.";
--
GitLab