From 5f62d80cc2ec88b837e1ded2fd49981e7b799037 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Tue, 23 Apr 2013 18:16:39 +0200
Subject: [PATCH] get assertion checking counter example transition from prolog
and update animator
---
.../ConstraintBasedAssertionCheckCommand.java | 19 ++++++++++++-----
.../AssertionCheckFinishedListener.java | 21 +++++++++++--------
2 files changed, 26 insertions(+), 14 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 88edcfaf..5b17b630 100644
--- a/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java
+++ b/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);
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 68c45628..876a6b17 100644
--- a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java
+++ b/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();
+ }
}
}
--
GitLab