Change meaning of isLowerBound() in RelOp and fix calls to it accordingly (to address a problem caused elsewhere in prism-games).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8623 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/ProbModelChecker.java

@@ -479,7 +479,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			if (p < 0 || p > 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Compute probabilities
 		switch (modelType) {
@@ -546,7 +546,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			if (r < 0)
 				throw new PrismException("Invalid reward bound " + r + " in R[] formula");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Get reward info
 		if (modulesFile == null)

prism/src/param/ParamModelChecker.java

@@ -873,7 +873,7 @@ final public class ParamModelChecker extends PrismComponent
 			if (p.compareTo(0) == -1 || p.compareTo(1) == 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Compute probabilities
 		if (!expr.getExpression().isSimplePathFormula()) {
@@ -977,7 +977,7 @@ final public class ParamModelChecker extends PrismComponent
 			if (r.compareTo(0) == -1)
 				throw new PrismException("Invalid reward bound " + r + " in R[] formula");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Get reward info
 		if (modulesFile == null)
@@ -1130,7 +1130,7 @@ final public class ParamModelChecker extends PrismComponent
 			if (p.compareTo(0) == -1 || p.compareTo(1) == 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Compute probabilities
 		probs = checkProbSteadyState(model, expr.getExpression(), min, needStates);

prism/src/parser/ast/RelOp.java

@@ -31,14 +31,29 @@ public enum RelOp {
 	}
 
 	/**
-	 * Returns true if this corresponds to a lower bound (e.g. >, >=, min=).
+	 * Returns true if this corresponds to a lower bound (i.e. >, >=).
+	 * NB: "min=?" does not return true for this.
 	 */
 	public boolean isLowerBound()
 	{
 		switch (this) {
 		case GT:
 		case GEQ:
-		case MIN:
+			return true;
+		default:
+			return false;
+		}
+	}
+
+	/**
+	 * Returns true if this corresponds to an upper bound (i.e. <, <=).
+	 * NB: "max=?" does not return true for this.
+	 */
+	public boolean isUpperBound()
+	{
+		switch (this) {
+		case LT:
+		case LEQ:
 			return true;
 		default:
 			return false;
@@ -60,13 +75,38 @@ public enum RelOp {
 	}
 
 	/**
-	 * Returns true if this corresponds to an upper bound (e.g. <, <=, max=).
+	 * Returns true if this is numerical (e.g. min=?, max=?).
 	 */
-	public boolean isUpperBound()
+	public boolean isNumerical()
+	{
+		switch (this) {
+		case MIN:
+		case MAX:
+			return true;
+		default:
+			return false;
+		}
+	}
+
+	/**
+	 * Returns true if this corresponds to minimum (min=?).
+	 */
+	public boolean isMin()
+	{
+		switch (this) {
+		case MIN:
+			return true;
+		default:
+			return false;
+		}
+	}
+
+	/**
+	 * Returns true if this corresponds to maximum (max=?).
+	 */
+	public boolean isMax()
 	{
 		switch (this) {
-		case LT:
-		case LEQ:
 		case MAX:
 			return true;
 		default:

prism/src/prism/NondetModelChecker.java

@@ -170,7 +170,7 @@ public class NondetModelChecker extends NonProbModelChecker
 			if (p < 0 || p > 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Check for trivial (i.e. stupid) cases
 		if (pb != null) {
@@ -235,7 +235,7 @@ public class NondetModelChecker extends NonProbModelChecker
 			if (r < 0)
 				throw new PrismException("Invalid reward bound " + r + " in R operator");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// get reward info
 		if (model.getNumRewardStructs() == 0)

prism/src/pta/PTAModelChecker.java

@@ -190,10 +190,11 @@ public class PTAModelChecker extends PrismComponent
 		double prob;
 
 		// Check whether Pmin=? or Pmax=? (only two cases allowed)
-		if (expr.getProb() != null) {
+		RelOp relOp = expr.getRelOp();
+		if (!relOp.isNumerical()) {
 			throw new PrismException("PTA model checking currently only supports Pmin=? and Pmax=? properties (try the digital clocks engine instead)");
 		}
-		min = expr.getRelOp().isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Check this is a F path property (only case allowed at the moment)
 		if (!(expr.getExpression() instanceof ExpressionTemporal))