diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index ede5acaf..af527b32 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -1037,6 +1037,11 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkRewardReach(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { + // No time bounds allowed + if (expr.hasBounds()) { + throw new PrismNotSupportedException("R operator cannot contain a bounded F operator: " + expr); + } + // Model check the operand for all states BitSet target = checkExpression(model, expr.getOperand2(), null).getBitSet(); diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index cb770909..a0568947 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -725,10 +725,8 @@ public abstract class Expression extends ASTElement { public void visitPre(ExpressionTemporal e) throws PrismLangException { - if (e.getLowerBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - if (e.getUpperBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); + if (e.hasBounds()) + throw new PrismLangException(""); } }); } catch (PrismLangException e) { diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index e3704be7..b3a22764 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1202,6 +1202,11 @@ public class NondetModelChecker extends NonProbModelChecker JDDNode b; StateValues rewards = null; + // No time bounds allowed + if (expr.hasBounds()) { + throw new PrismNotSupportedException("R operator cannot contain a bounded F operator: " + expr); + } + // model check operand first b = checkExpressionDD(expr.getOperand2()); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index cd1519e2..f2e98250 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -876,6 +876,11 @@ public class ProbModelChecker extends NonProbModelChecker JDDNode b; StateValues rewards = null; + // No time bounds allowed + if (expr.hasBounds()) { + throw new PrismNotSupportedException("R operator cannot contain a bounded F operator: " + expr); + } + // model check operand first b = checkExpressionDD(expr.getOperand2());