From 69c8b2ce1ff48685dc7b8f8196fb9ed4d676022c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 16 Jul 2015 22:06:09 +0000 Subject: [PATCH] Bug fix: better detection of R[F] when seeing if it is cosafe. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10338 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ProbModelChecker.java | 2 +- prism/src/parser/ast/Expression.java | 13 +++++++++++++ prism/src/prism/NondetModelChecker.java | 2 +- 3 files changed, 15 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 02e7d3f6..b7139e88 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -1054,7 +1054,7 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkRewardPathFormula(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { - if (expr instanceof ExpressionTemporal && ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F){ + if (Expression.isReach(expr)) { return checkRewardReach(model, modelRewards, (ExpressionTemporal) expr, minMax, statesOfInterest); } else if (Expression.isCoSafeLTLSyntactic(expr)) { diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 4366f233..cb770909 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -702,6 +702,19 @@ public abstract class Expression extends ASTElement return false; } + /** + * Test if an expression is a reachability path formula (F phi) + */ + public static boolean isReach(Expression expr) + { + if (expr instanceof ExpressionTemporal) { + if (((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F) { + return ((ExpressionTemporal) expr).getOperand2().isProposition(); + } + } + return false; + } + /** * Test if an expression contains time bounds on temporal operators */ diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 1db0630f..e3704be7 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1186,7 +1186,7 @@ public class NondetModelChecker extends NonProbModelChecker */ protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException { - if (expr instanceof ExpressionTemporal && ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F){ + if (Expression.isReach(expr)) { return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, min); } else if (Expression.isCoSafeLTLSyntactic(expr)) {