diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index ca7b6b59..51553779 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -55,6 +55,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"); } @@ -77,6 +80,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"); } @@ -105,6 +111,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"); }