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

add missing case (PROBPLUGIN-103)

parent b254dc6d
Branches
No related tags found
No related merge requests found
...@@ -18,7 +18,7 @@ import de.prob.prolog.term.PrologTerm; ...@@ -18,7 +18,7 @@ import de.prob.prolog.term.PrologTerm;
public class ConstraintBasedAssertionCheckCommand implements IComposableCommand { public class ConstraintBasedAssertionCheckCommand implements IComposableCommand {
public static enum ResultType { 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"; private static final String COMMAND_NAME = "cbc_static_assertion_violation_checking";
...@@ -59,7 +59,9 @@ public class ConstraintBasedAssertionCheckCommand implements IComposableCommand ...@@ -59,7 +59,9 @@ public class ConstraintBasedAssertionCheckCommand implements IComposableCommand
if (resultTerm.hasFunctor("interrupted", 0)) { if (resultTerm.hasFunctor("interrupted", 0)) {
result = ResultType.INTERRUPTED; result = ResultType.INTERRUPTED;
} else if (resultTerm.hasFunctor("no_counterexample_found", 0)) { } 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)) { } else if (resultTerm.hasFunctor("counterexample_found", 2)) {
result = ResultType.COUNTER_EXAMPLE; result = ResultType.COUNTER_EXAMPLE;
CompoundPrologTerm counterExampleTerm = (CompoundPrologTerm) resultTerm; CompoundPrologTerm counterExampleTerm = (CompoundPrologTerm) resultTerm;
......
...@@ -47,7 +47,12 @@ public class AssertionCheckFinishedListener extends ProBJobFinishedListener { ...@@ -47,7 +47,12 @@ public class AssertionCheckFinishedListener extends ProBJobFinishedListener {
message = "ProB did not return a result"; message = "ProB did not return a result";
} else { } else {
switch (result) { 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; dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Counter-Example Found"; dialogTitle = "No Counter-Example Found";
message = "No Counter-Example to the Context Theorems was found."; message = "No Counter-Example to the Context Theorems was found.";
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment