Parametric model checking P< result

[Artur Rataj]

Hi, I have a small model

mdp

const double q;

module m

l : [0..1] init 0;

s0 : [0..1] init 0;

[] (s0=0) -> q:(s0'=1) + (1-q):(l'=l+1)&(s0'=1);

[] (s0=1) -> true;

endmodule

The command line is

prism -param q=0:1 m.nm -pctl "P<0.5[F l=1]"

I can not interpret the result:

Result: ([0.53125,1.0]): true ([0.0,0.5]): false

I would expect (0.5,1.0] true, [0.0,0.5] false

Could you please explain the result?

Best regards,

Artur

[Dave Parker]

Hi Artur,

PRISM answers these kinds of queries by partitioning the parameter space
into increasingly small hyper-rectangles. There will often be a part of
this space for which the result is still undecided at the end (in this
case 0.5<q<0.53125). You can increase the precision using the
-paramprecision switch. For example, using -paramprecision 1e-6 gives:

Result: ([0.5000009536743164,1.0]): true
([0.0,0.5]): false

See here for more info:

http://www.prismmodelchecker.org/manual/RunningPRISM/ParametricModelChecking

Best wishes,

Dave

> --
> 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.