Auto-switch to explicit engine for interval interation on Rmin.

prism/src/parser/ast/Expression.java

@@ -845,6 +845,31 @@ public abstract class Expression extends ASTElement
 		return false;
 	}
 	
+	/**
+	 * Test if an expression contains a minimum expected reward operator. 
+	 * Actually, this returns true if there is an R operator with "min=?" or a lower bound attached to it,
+	 * so this is just an approximation. (For example, an R operator might be embedded within
+	 * an "exists" strategy operator)
+	 */
+	public static boolean containsMinReward(Expression expr)
+	{
+		try {
+			ASTTraverse astt = new ASTTraverse()
+			{
+				public void visitPost(ExpressionReward e) throws PrismLangException
+				{
+					if (e.isMin()) {
+						throw new PrismLangException("Found one", e);
+					}
+				}
+			};
+			expr.accept(astt);
+		} catch (PrismLangException e) {
+			return true;
+		}
+		return false;
+	}
+	
 	/**
 	 * Test if an expression contains a non-probabilistic LTL formula (i.e., a non-simple path formula). 
 	 */

prism/src/parser/ast/ExpressionReward.java

@@ -203,6 +203,17 @@ public class ExpressionReward extends ExpressionQuant
 		}
 	}
 	
+	/**
+	 * Returns true is this is a minimum rewards operator.
+	 * Actually, this returns true if the operator has "min=?" or a lower bound attached to it,
+	 * so this is just an approximation. (For example, this R operator might be embedded within
+	 * an "exists" strategy operator)
+	 */
+	public boolean isMin()
+	{
+		return getRelOp().isMin() || getRelOp().isLowerBound();
+	}
+	
 	// Methods required for Expression:
 	
 	@Override

prism/src/prism/Prism.java

@@ -3024,6 +3024,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 			lastEngine = getEngine();
 			setEngine(Prism.EXPLICIT);
 		}
+		if (settings.getBoolean(PrismSettings.PRISM_INTERVAL_ITER)) {
+			if (currentModelType == ModelType.MDP && Expression.containsMinReward(prop.getExpression())) {
+				mainLog.printWarning("Switching to explicit engine to allow interval iteration on Rmin operator.");
+				engineSwitch = true;
+				lastEngine = getEngine();
+				setEngine(Prism.EXPLICIT);
+			}
+		}
 		try {
 			// Build model, if necessary
 			buildModelIfRequired();