diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 18e1f69b..4304b61e 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -788,9 +788,9 @@ public class ProbModelChecker extends NonProbModelChecker int time; // time StateValues rewards = null; - //check that there is an upper time bound + // check that there is an upper time bound if (expr.getUpperBound() == null) { - throw new PrismException("Cumulative reward without any time bound is only allowed for multi-objective queries."); + throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries"); } // get info from inst reward diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 1a86964b..297fee8d 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -1306,6 +1306,17 @@ public class SimulatorEngine } catch (PrismException e) { return "Simulator cannot handle this property: " + e.getMessage(); } + // Simulator cannot handle cumulative reward properties without a time bound + if (expr instanceof ExpressionReward) { + Expression exprTemp = ((ExpressionReward) expr).getExpression(); + if (exprTemp instanceof ExpressionTemporal) { + if (((ExpressionTemporal) exprTemp).getOperator() == ExpressionTemporal.R_C) { + if (((ExpressionTemporal) exprTemp).getUpperBound() == null) { + return "Simulator cannot handle cumulative reward properties without time bounds"; + } + } + } + } // No errors return null; } diff --git a/prism/src/simulator/sampler/Sampler.java b/prism/src/simulator/sampler/Sampler.java index 0f1aed7d..e10212f0 100644 --- a/prism/src/simulator/sampler/Sampler.java +++ b/prism/src/simulator/sampler/Sampler.java @@ -238,11 +238,6 @@ public abstract class Sampler ExpressionTemporal exprTemp = (ExpressionTemporal) expr.getExpression(); switch (exprTemp.getOperator()) { case ExpressionTemporal.R_C: - //first check that there is an upper time bound - if (exprTemp.getUpperBound() == null) { - throw new PrismException("Cumulative reward without any time bound is only allowed for multi-objective queries."); - } - if (mf.getModelType().continuousTime()) { // Continuous-time cumulative reward return new SamplerRewardCumulCont(exprTemp, rsi); diff --git a/prism/src/simulator/sampler/SamplerRewardCumulCont.java b/prism/src/simulator/sampler/SamplerRewardCumulCont.java index 13c0f2c4..d2508ca4 100644 --- a/prism/src/simulator/sampler/SamplerRewardCumulCont.java +++ b/prism/src/simulator/sampler/SamplerRewardCumulCont.java @@ -48,11 +48,6 @@ public class SamplerRewardCumulCont extends SamplerDouble if (expr.getOperator() != ExpressionTemporal.R_C) throw new PrismException("Error creating Sampler"); - //check that there is an upper time bound - if (expr.getUpperBound() == null) { - throw new PrismException("Cumulative reward without any time bound is only allowed for multi-objective queries."); - } - timeBound = expr.getUpperBound().evaluateDouble(); this.rewardStructIndex = rewardStructIndex; // Initialise sampler info diff --git a/prism/src/simulator/sampler/SamplerRewardCumulDisc.java b/prism/src/simulator/sampler/SamplerRewardCumulDisc.java index 7815c359..6bdecd90 100644 --- a/prism/src/simulator/sampler/SamplerRewardCumulDisc.java +++ b/prism/src/simulator/sampler/SamplerRewardCumulDisc.java @@ -48,11 +48,6 @@ public class SamplerRewardCumulDisc extends SamplerDouble if (expr.getOperator() != ExpressionTemporal.R_C) throw new PrismException("Error creating Sampler"); - //Check that there is an upper time bound - if (expr.getUpperBound() == null) { - throw new PrismException("Cumulative reward without any time bound is only allowed for multi-objective queries."); - } - timeBound = expr.getUpperBound().evaluateInt(); this.rewardStructIndex = rewardStructIndex; // Initialise sampler info