Experiment SPRT not re-using previous simulation result

[Junho Kim]

Hi, I'm now doing an experiment about statistical model checking.

My question is that I want to do SMC using simulation.

My property is that checking the probability when some variable is greater than x value.

I want to do experiment when the probability is 

P>=prop [ F<10000 ("terminate"& utility>= x) ]

like this property .

I did this when prop is from 0.01 to 0.99, but the problem is that PRISM used the maximum number of samples that required to verifying the property.

But, I want to not re-use the previous simulation result.

How do I do experiment without re-using simulation result on SPRT?

CI asked me whether re-use or not, but SPRT does not.

[Dave Parker]

If you want PRISM to *not* use the same set of simulation paths for
different values of the prop constant, either:

1. Untick "Check properties simultaneously" in the "Simulator" tab of
the options dialog; or

2. Put the constant prop in the model rather than with the properties

I don't see why you would get different settings for CI vs SPRT though.

Best wishes,

Dave

On 09/09/2016 02:29, Junho Kim wrote:
> Hi, I'm now doing an experiment about statistical model checking.
>
> My question is that I want to do SMC using simulation.
>
> My property is that checking the probability when some variable is
> greater than x value.
> I want to do experiment when the probability is
>

> *P>=prop [ F<10000 ("terminate"& utility>= x) ]*

>
>
> like this property .
>
> I did this when prop is from 0.01 to 0.99, but the problem is that PRISM
> used the maximum number of samples that required to verifying the property.
> But, I want to not re-use the previous simulation result.
>

> How do I do experiment without re-using simulation result on *SPRT?*

> CI asked me whether re-use or not, but SPRT does not.
>

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To post to this group, send email to prismmod...@googlegroups.com
> <mailto:prismmod...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.