Browse Source

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.
master
Joachim Klein 8 years ago
parent
commit
57b68f6f9d
  1. 4
      prism/src/simulator/sampler/SamplerBoundedUntilCont.java
  2. 4
      prism/src/simulator/sampler/SamplerBoundedUntilDisc.java

4
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;
}
}

4
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;
}
}
Loading…
Cancel
Save