From ee86fbc84cb0496702b14645d8a4e61c3708533c Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Mon, 13 Oct 2014 11:30:03 +0200
Subject: [PATCH] rise error message regarding valid constants and properties
even if there is no operation available
---
.../prob/core/command/ExploreStateCommand.java | 16 ++++++++++------
1 file changed, 10 insertions(+), 6 deletions(-)
diff --git a/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java b/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java
index 30af5f46..98f0b1e5 100644
--- a/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java
+++ b/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java
@@ -6,10 +6,16 @@
package de.prob.core.command;
-import java.util.*;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
import de.prob.core.Animator;
-import de.prob.core.domainobjects.*;
+import de.prob.core.domainobjects.Operation;
+import de.prob.core.domainobjects.State;
+import de.prob.core.domainobjects.StateError;
+import de.prob.core.domainobjects.Variable;
import de.prob.core.internal.Activator;
import de.prob.exceptions.ProBException;
import de.prob.logging.Logger;
@@ -80,10 +86,8 @@ public final class ExploreStateCommand implements IComposableCommand {
// only show error message on SETUP_CONSTANTS and
// PARTIALLY_SETUP_CONSTANTS
- if (enabledOperations.size() == 1
- && enabledOperations.get(0).getName().toLowerCase()
- .contains("constants") && unsatPropertiesExist) {
- Logger.notifyUserWithoutBugreport("ProB could not find valid constants wich satisfy the properties:\n\n"
+ if (unsatPropertiesExist) {
+ Logger.notifyUserWithoutBugreport("ProB could not find valid constants wich satisfy the properties.\n"
+ unsatPropsCommand.getUnsatPropertiesDescription());
} else if (!initialised && enabledOperations.isEmpty()
--
GitLab