From 57b68f6f9d111b9680800d547f2b44ebb14730fc Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 11 Jul 2018 14:36:19 +0200 Subject: [PATCH] Statistical MC: Fix infinite sampling for lower bounded P[F]/P[U] Only F/U operators with upper bound have a bounded path length and can thus skip the maximal path length checks. Test cases (will continue sampling beyond the default max path length, appearing to hang): prism prism-examples/dice/dice.pm -pf 'P=?[ F>2 s=0 ]' -sim prism prism-examples/dice/dice.pm -pf 'P=?[ F>2 s=0 ]' -sim -ctmc After this fix, the usual error message for unbounded operators is generated. --- prism/src/simulator/sampler/SamplerBoundedUntilCont.java | 4 ++-- prism/src/simulator/sampler/SamplerBoundedUntilDisc.java | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java index ae97665d..0cd41b07 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java @@ -167,7 +167,7 @@ public class SamplerBoundedUntilCont extends SamplerBoolean @Override public boolean needsBoundedNumSteps() { - // Always bounded (although we don't know the exact num steps, just the time bound) - return true; + // Bounded if there is a non-finite upper-bound (although we don't know the exact num steps, just the time bound) + return ub < Double.POSITIVE_INFINITY; } } diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java index ff922410..b6f421ef 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java @@ -137,7 +137,7 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean @Override public boolean needsBoundedNumSteps() { - // Always bounded - return true; + // Bounded if there is an upper bound + return haveUpperBound; } }