get assertion checking counter example transition from prolog and update animator

de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java

@@ -3,9 +3,10 @@
  */
 package de.prob.core.command;
 
+import de.prob.core.domainobjects.Operation;
 import de.prob.parser.ISimplifiedROMap;
 import de.prob.prolog.output.IPrologTermOutput;
-import de.prob.prolog.term.ListPrologTerm;
+import de.prob.prolog.term.CompoundPrologTerm;
 import de.prob.prolog.term.PrologTerm;
 
 /**
@@ -34,8 +35,12 @@ public class ConstraintBasedAssertionCheckCommand implements IComposableCommand
 		return result;
 	}
 
-	public ListPrologTerm getCounterExampleState() {
-		return counterExampleState;
+	public Operation getCounterExampleOperation() {
+		return counterExampleOperation;
+	}
+
+	public String getCounterExampleStateID() {
+		return counterExampleStateID;
 	}
 
 	@Override
@@ -55,9 +60,13 @@ public class ConstraintBasedAssertionCheckCommand implements IComposableCommand
 			result = ResultType.INTERRUPTED;
 		} else if (resultTerm.hasFunctor("no_counterexample_found", 0)) {
 			result = ResultType.NO_COUNTER_EXAMPLE;
-		} else if (resultTerm.hasFunctor("counterexample_found", 1)) {
-			counterExampleState = (ListPrologTerm) resultTerm.getArgument(1);
+		} else if (resultTerm.hasFunctor("counterexample_found", 2)) {
 			result = ResultType.COUNTER_EXAMPLE;
+			CompoundPrologTerm counterExampleTerm = (CompoundPrologTerm) resultTerm;
+			counterExampleOperation = Operation
+					.fromPrologTerm(counterExampleTerm.getArgument(1));
+			counterExampleStateID = counterExampleTerm.getArgument(2)
+					.toString();
 		} else
 			throw new CommandException(
 					"unexpected result from deadlock check: " + resultTerm);

de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java

@@ -11,9 +11,11 @@ import de.prob.core.Animator;
 import de.prob.core.ProBJobFinishedListener;
 import de.prob.core.command.ConstraintBasedAssertionCheckCommand;
 import de.prob.core.command.ConstraintBasedAssertionCheckCommand.ResultType;
+import de.prob.core.command.ExecuteOperationCommand;
 import de.prob.core.command.IComposableCommand;
+import de.prob.core.domainobjects.Operation;
+import de.prob.exceptions.ProBException;
 import de.prob.logging.Logger;
-import de.prob.prolog.term.ListPrologTerm;
 
 /**
  * This JobChangeAdapter presents the user the results of a deadlock freedom
@@ -84,13 +86,14 @@ public class AssertionCheckFinishedListener extends ProBJobFinishedListener {
 	private void displayCounterExample(
 			final ConstraintBasedAssertionCheckCommand command,
 			final Animator animator) {
-		final ListPrologTerm errorState = command.getCounterExampleState();
-		// try {
-		// animator.getHistory().reset();
-
-		// ExecuteOperationCommand.executeOperation(animator, operation);
-		// } catch (ProBException e) {
-		// e.notifyUserOnce();
-		// }
+		final Operation operation = command.getCounterExampleOperation();
+		try {
+			// we do not reset the history because we want to keep the root
+			// state, we just start a new path from root
+			animator.getHistory().gotoPos(0);
+			ExecuteOperationCommand.executeOperation(animator, operation);
+		} catch (ProBException e) {
+			e.notifyUserOnce();
+		}
 	}
 }