From 43a2184197aaf35297e00590ba7197a7a728b9cc Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Tue, 1 Oct 2019 12:33:35 +0200
Subject: [PATCH] fix showResult in AssertionDynCheckFinishedListener
---
.../src/de/prob/ui/assertion/AssertionCheckHandler.java | 2 +-
.../ui/assertion/AssertionDynCheckFinishedListener.java | 8 ++++----
.../de/prob/ui/assertion/AssertionDynCheckHandler.java | 3 +--
3 files changed, 6 insertions(+), 7 deletions(-)
diff --git a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckHandler.java b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckHandler.java
index 65b6f799..109774b1 100644
--- a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckHandler.java
+++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckHandler.java
@@ -28,7 +28,7 @@ public class AssertionCheckHandler extends AbstractHandler {
if (Animator.getAnimator().isMachineLoaded()) {
performAssertionCheck(shell);
} else {
- Logger.notifyUser("No ProB animation running. This is a bug. Please submit a report. Error in declaraion for class DeadlockCheckHandler");
+ Logger.notifyUser("No ProB animation running. This is a bug. Please submit a report. Error in declaraion for class AssertionCheckHandler");
}
return null;
}
diff --git a/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.java b/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.java
index 9796d1fe..074c5ae5 100644
--- a/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.java
+++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.java
@@ -9,8 +9,8 @@ import org.eclipse.swt.widgets.Shell;
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.ConstraintBasedDynamicAssertionCheckCommand;
+import de.prob.core.command.ConstraintBasedDynamicAssertionCheckCommand.ResultType;
import de.prob.core.command.ExecuteOperationCommand;
import de.prob.core.command.IComposableCommand;
import de.prob.core.domainobjects.Operation;
@@ -35,7 +35,7 @@ public class AssertionDynCheckFinishedListener extends ProBJobFinishedListener {
@Override
protected void showResult(final IComposableCommand cmd,
final Animator animator) {
- final ConstraintBasedAssertionCheckCommand command = (ConstraintBasedAssertionCheckCommand) cmd;
+ final ConstraintBasedDynamicAssertionCheckCommand command = (ConstraintBasedDynamicAssertionCheckCommand) cmd;
final ResultType result = command.getResult();
final int dialogType;
final String dialogTitle;
@@ -89,7 +89,7 @@ public class AssertionDynCheckFinishedListener extends ProBJobFinishedListener {
}
private void displayCounterExample(
- final ConstraintBasedAssertionCheckCommand command,
+ final ConstraintBasedDynamicAssertionCheckCommand command,
final Animator animator) {
final Operation operation = command.getCounterExampleOperation();
try {
diff --git a/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckHandler.java b/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckHandler.java
index 4ba3f822..57a08f3d 100644
--- a/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckHandler.java
+++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckHandler.java
@@ -13,7 +13,6 @@ import org.eclipse.ui.handlers.HandlerUtil;
import de.prob.core.Animator;
import de.prob.core.LanguageDependendAnimationPart;
import de.prob.core.ProBCommandJob;
-import de.prob.core.command.ConstraintBasedAssertionCheckCommand;
import de.prob.core.command.ConstraintBasedDynamicAssertionCheckCommand;
import de.prob.logging.Logger;
@@ -29,7 +28,7 @@ public class AssertionDynCheckHandler extends AbstractHandler {
if (Animator.getAnimator().isMachineLoaded()) {
performAssertionCheck(shell);
} else {
- Logger.notifyUser("No ProB animation running. This is a bug. Please submit a report. Error in declaraion for class DeadlockCheckHandler");
+ Logger.notifyUser("No ProB animation running. This is a bug. Please submit a report. Error in declaraion for class AssertionDynCheckHandler");
}
return null;
}
--
GitLab