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 802e83ad1674560e06e6b82aedde25fb6edaa2e4..88edcfafa062aab49fa4f4397221c2afa29f00e0 100644 --- a/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java +++ b/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java @@ -17,14 +17,15 @@ import de.prob.prolog.term.PrologTerm; public class ConstraintBasedAssertionCheckCommand implements IComposableCommand { public static enum ResultType { - TIMEOUT, COUNTER_EXAMPLE, NO_COUNTER_EXAMPLE + INTERRUPTED, COUNTER_EXAMPLE, NO_COUNTER_EXAMPLE }; private static final String COMMAND_NAME = "cbc_static_assertion_violation_checking"; private static final String RESULT_VARIABLE = "R"; private ResultType result; - private ListPrologTerm counterExampleState; + private Operation counterExampleOperation; + private String counterExampleStateID; public ConstraintBasedAssertionCheckCommand() { } @@ -50,8 +51,8 @@ public class ConstraintBasedAssertionCheckCommand implements IComposableCommand throws CommandException { final PrologTerm resultTerm = bindings.get(RESULT_VARIABLE); final ResultType result; - if (resultTerm.hasFunctor("time_out", 0)) { - result = ResultType.TIMEOUT; + if (resultTerm.hasFunctor("interrupted", 0)) { + result = ResultType.INTERRUPTED; } else if (resultTerm.hasFunctor("no_counterexample_found", 0)) { result = ResultType.NO_COUNTER_EXAMPLE; } else if (resultTerm.hasFunctor("counterexample_found", 1)) { 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 03ae30457c6a0b2e6f38b2cfeaa8acd04e95f6fe..68c45628f2264dfb30ae8cba6593826b1e05a070 100644 --- a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java +++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java @@ -56,7 +56,7 @@ public class AssertionCheckFinishedListener extends ProBJobFinishedListener { message = "The model contains a Counter-Example state, it will be shown in the state view."; displayCounterExample(command, animator); break; - case TIMEOUT: + case INTERRUPTED: dialogType = MessageDialog.WARNING; dialogTitle = " Interrupt"; message = "The deadlock check has been interrupted by the user or a time-out.";