From 37fad8894e0036db97c952f0a8f5798c52f82431 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 11 Jul 2018 14:32:50 +0200 Subject: [PATCH] SamplerBoundedUntilDisc: tweak handling of absent upper bound We now explicitly remember if there was an upper bound instead of relying on an upper bound of Integer.MAX_VALUE in the case of an absent bound. Statistical MC, P[F]/P[U] in discrete time setting with time bounds. --- .../simulator/sampler/SamplerBoundedUntilDisc.java | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java index c58b8368..ff922410 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java @@ -38,6 +38,7 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean private Expression right; private int lb; private int ub; + private boolean haveUpperBound; /** * Construct a sampler for a (discrete-time) bounded until property. @@ -68,17 +69,19 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean } // Upper bound if (expr.getUpperBound() != null) { + haveUpperBound = true; ub = expr.getUpperBound().evaluateInt(); if (expr.upperBoundIsStrict()) { // Convert to non-strict bound: <=ub-1 ub = ub - 1; } + + if (ub < 0) { + throw new PrismException("Invalid upper bound in "+expr); + } } else { // No upper bound - ub = Integer.MAX_VALUE; - } - if (ub < 0) { - throw new PrismException("Invalid upper bound in "+expr); + haveUpperBound = false; } // Initialise sampler info @@ -95,7 +98,7 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean long pathSize = path.size(); // Upper bound exceeded - if (pathSize > ub) { + if (haveUpperBound && pathSize > ub) { valueKnown = true; value = false; }