Multiple Initial states

[Mridu Nanda]

Hi,

I was trying to post a follow up question to this thread (https://groups.google.com/g/prismmodelchecker/c/PtufJCS3hZQ), but I don't think my message was posting. I have pasted my question below:

Is there a way to fully specify multiple initial states. For example, if I have three variables, a, b, and c, I want the initial states where a=0,b=0,c=0, and a=1,b=0,c=0. I can't specify this with the notation a+b+c=1, since that would explore more initial states than I am interested in..

Thanks,

Mridu

[Dave Parker]

Hi Mridu,

To specify multiple initial states, you need to provide a single
predicate (inside init...endinit) which is true precisely when the state
is an initial one. Can you use a>=0 & a<=1 & b=0 & c=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/0dfdcf55-a0f8-484e-86a7-5e47df424e8an%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/0dfdcf55-a0f8-484e-86a7-5e47df424e8an%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Mridu Nanda]

Hi Dave,

Thanks for your reply! Your response makes sense for the small example I gave. However, consider if I want the following initial states: a=0,b=0,c=1, a=1,b=0,c=0. Modding your previous response, I would be checking two additional states (a=0,b=0,c=0, and a=1,b=0,c=1). If the number of variables increase, then I would be checking many more initial states than necessary.

Is there a way to avoid this overhead?

Thanks,
Mridu

> On Jun 6, 2023, at 3:41 PM, Dave Parker <david....@cs.ox.ac.uk> wrote:
>
> Hi Mridu,

[Dave Parker]

It depends what you want your initial states to be as the number of
variables increases. If you can give us a precise definition, we can see
if that can be encoded conveniently as a PRISM expression.

Best wishes,

Dave