From db928a3402f1848173b035f9de7a0d2297d807ce Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 17 Dec 2012 15:46:01 +0000 Subject: [PATCH] Tweak/move error messages for non-supported R[C] operator. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6222 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ProbModelChecker.java | 4 ++-- prism/src/simulator/SimulatorEngine.java | 11 +++++++++++ prism/src/simulator/sampler/Sampler.java | 5 ----- .../src/simulator/sampler/SamplerRewardCumulCont.java | 5 ----- .../src/simulator/sampler/SamplerRewardCumulDisc.java | 5 ----- 5 files changed, 13 insertions(+), 17 deletions(-) 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