diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 22e4010b..af13b03c 100644 --- a/prism/src/parser/ast/Expression.java +++ b/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). */ diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java index dc6c647f..9a5b8251 100644 --- a/prism/src/parser/ast/ExpressionReward.java +++ b/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 diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index b4b7793d..841fbc82 100644 --- a/prism/src/prism/Prism.java +++ b/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();