From 47d5e573d66d4d9772334a4beaead044e26809a0 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:24:57 +0200 Subject: [PATCH] Use reachability reward computation for complex state formulas E.g., R=?[ F (a & A[F b])] was previously handled via co-safety, as the operand of the F operator is not a proposition. --- prism/src/explicit/ProbModelChecker.java | 2 +- prism/src/param/ParamModelChecker.java | 2 +- prism/src/prism/NondetModelChecker.java | 2 +- prism/src/prism/ProbModelChecker.java | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 09215b8a..19d9dd70 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -1117,7 +1117,7 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkRewardPathFormula(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { - if (Expression.isReach(expr)) { + if (Expression.isReachWithStateFormula(expr)) { return checkRewardReach(model, modelRewards, (ExpressionTemporal) expr, minMax, statesOfInterest); } else if (Expression.isCoSafeLTLSyntactic(expr, true)) { diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index fda74d59..16da189b 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -1082,7 +1082,7 @@ final public class ParamModelChecker extends PrismComponent */ private RegionValues checkRewardPathFormula(ParamModel model, ParamRewardStruct rew, Expression expr, boolean min, BitSet needStates) throws PrismException { - if (Expression.isReach(expr)) { + if (Expression.isReachWithStateFormula(expr)) { return checkRewardReach(model, rew, (ExpressionTemporal) expr, min, needStates); } else if (Expression.isCoSafeLTLSyntactic(expr, true)) { throw new PrismNotSupportedException(mode.Engine() + " does not yet support co-safe reward computation"); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index a5e14463..382128d9 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1414,7 +1414,7 @@ public class NondetModelChecker extends NonProbModelChecker */ protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException { - if (Expression.isReach(expr)) { + if (Expression.isReachWithStateFormula(expr)) { return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, min, statesOfInterest); } else if (Expression.isCoSafeLTLSyntactic(expr, true)) { diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 0acbc159..3622c015 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -906,7 +906,7 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException { - if (Expression.isReach(expr)) { + if (Expression.isReachWithStateFormula(expr)) { return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, statesOfInterest); } else if (Expression.isCoSafeLTLSyntactic(expr, true)) {