From 367a2bd71719e8c60bc0fa7b3752d79cd4b0e92a Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 11 Jul 2018 14:18:39 +0200 Subject: [PATCH] Statistical MC: Check bounds for CTMC bounded until Throw an error if the bounds are negative or upper bound smaller than lower bound (similar to the checks in the other engines / samplers). --- .../sampler/SamplerBoundedUntilCont.java | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java index 718840b8..ae97665d 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java @@ -55,8 +55,25 @@ public class SamplerBoundedUntilCont extends SamplerBoolean throw new PrismException("Error creating Sampler"); left = expr.getOperand1(); right = expr.getOperand2(); + lb = expr.getLowerBound() == null ? 0.0 : expr.getLowerBound().evaluateDouble(); - ub = expr.getUpperBound() == null ? Double.POSITIVE_INFINITY : expr.getUpperBound().evaluateDouble(); + if (lb < 0) { + throw new PrismException("Invalid lower bound " + lb + " in time-bounded until formula"); + } + + if (expr.getUpperBound() == null) { + ub = Double.POSITIVE_INFINITY; + } else { + ub = expr.getUpperBound().evaluateDouble(); + if (ub < 0 || (ub == 0 && expr.upperBoundIsStrict())) { + String bound = (expr.upperBoundIsStrict() ? "<" : "<=") + ub; + throw new PrismException("Invalid upper bound " + bound + " in time-bounded until formula"); + } + if (ub < lb) { + throw new PrismException("Upper bound must exceed lower bound in time-bounded until formula"); + } + } + // Initialise sampler info reset(); resetStats();