From 17a946783d94ee48189a5a7a4eec7dd470c039aa Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 16 Jul 2015 23:13:58 +0000 Subject: [PATCH] Disallow properties of the form R[F<=k]. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10343 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ProbModelChecker.java | 5 +++++ prism/src/parser/ast/Expression.java | 6 ++---- prism/src/prism/NondetModelChecker.java | 5 +++++ prism/src/prism/ProbModelChecker.java | 5 +++++ 4 files changed, 17 insertions(+), 4 deletions(-) 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());