Issue while using multi(Prop1,Prop2) property for my model

[Shahid Ali Khan]

Hi,

I am using multi property in my mdp typed model, my model contains multiple modules, and the number of states and transitions are quite high. I want to calculate minimum probabilities (Pmin=?), but the issue is it always give me 0. Here, I used two Pmin in multi e.g multi(Pmin=? [ F s1=13 ], Pmin=? [ F s1=20 ]) result: [(2.220446049250313E-16, 2.220446049250313E-16)], now it is giving some probability other than 0 but it is same. 

Can anyone please help me in understanding this behavior?

Regards, 

Shahid Ali

[Dave Parker]

Hi Shahid,

I guess that the probability _is_ 0, but there is some round-off error
when the computation is done via the multi-objective method.

If you can share the model, we can perhaps help you identify why the min
probability is 0.

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 view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/bfad25cc-f624-41a4-bb81-27d5da1ff98dn%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/bfad25cc-f624-41a4-bb81-27d5da1ff98dn%40googlegroups.com?utm_medium=email&utm_source=footer>.