From a911a2eb8867c4b5c74eec07d33cbde9db15ddb6 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:26:06 +0200 Subject: [PATCH] imported patch rewardcounter-CTMC-extra-check-TODO.patch --- prism/src/explicit/CTMCModelChecker.java | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 60387270..1b05cd2e 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -53,6 +53,9 @@ public class CTMCModelChecker extends ProbModelChecker @Override protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException { + if (Expression.containsTemporalRewardBounds(expr)) { + throw new PrismNotSupportedException("LTL formulas with reward bounds not supported for CTMCs"); + } if (Expression.containsTemporalTimeBounds(expr)) { throw new PrismNotSupportedException("LTL formulas with time bounds not supported for CTMCs"); } @@ -75,6 +78,9 @@ public class CTMCModelChecker extends ProbModelChecker @Override protected StateValues checkRewardCoSafeLTL(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { + if (Expression.containsTemporalRewardBounds(expr)) { + throw new PrismNotSupportedException("LTL formulas with reward bounds not supported for CTMCs"); + } if (Expression.containsTemporalTimeBounds(expr)) { throw new PrismNotSupportedException("LTL formulas with time bounds not supported for CTMCs"); } @@ -103,6 +109,9 @@ public class CTMCModelChecker extends ProbModelChecker @Override protected StateValues checkExistsLTL(Model model, Expression expr, BitSet statesOfInterest) throws PrismException { + if (Expression.containsTemporalRewardBounds(expr)) { + throw new PrismNotSupportedException("LTL formulas with reward bounds not supported for CTMCs"); + } if (Expression.containsTemporalTimeBounds(expr)) { throw new PrismNotSupportedException("LTL formulas with time bounds not supported for CTMCs"); }