Init/endinit for constants?

[Mridu Nanda]

Is it possible to use init/endinit to initialize constants? When I try this in the GUI, I get asked for to provide a value of the constant before verifying the property..

Is there a way to easily incorporate this functionality in PRISM source code? I would really appreciate some help in pointing me to the correct location in the source code?

Thanks,

Mridu

[Dave Parker]

I'm not sure what you mean by this Mridu. Constants are values that are
fixed at the start of model checking and retain their value throughout.
You can use experiments to do model checking for a range of different
constant values. The init/endinit construct is used to specify a range
of different possible initial states within the same model.

If you explain in more detail what you are aiming to achieve, I can try
to advise you which is more appropriate.

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/c9bfc9f8-c192-4625-a634-8a73714920f9n%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/c9bfc9f8-c192-4625-a634-8a73714920f9n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Mridu Nanda]

Hi Prof. Parker,

Thanks for your response! Suppose I have some constant my_const. Then I want my_const to take different values depending on the initial state. So for example, if I am in initial state 1, then my_const should be 10, but if I am in initial state 2, my_const should be 12.

I know an alternate solution would be to declare my_const as a variable like so: 

my_const [10..12];

And then use the init/endinit construct to initialize the value per initial state.However, I would like to avoid allocating extra variables, especially since the value of my_const does not change for a given initial state.

Does this help clarify what I am trying to implement?
Thanks again for all your help!
Mridu

[Dave Parker]

Thanks for clarifying Mridu. I assume you want to use this constant in
commands (or reward structures) somehow? If so, this will not work, I'm
afraid. The models are Markov, meaning that the current state
(comprising the values of all the variables) should contain all
information needed to define what happens from that point onwards.

Effectively, you seem to want to "remember" which initial state you
started in. This would mean that different states would behave
differently depending on which initial state you started from, which
violates this assumption. So, if I understand correctly what you want,
you woudl indeed need to add my_const as an extra variable.

Best wishes,

Dave

> https://groups.google.com/d/msgid/prismmodelchecker/c9bfc9f8-c192-4625-a634-8a73714920f9n%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/c9bfc9f8-c192-4625-a634-8a73714920f9n%40googlegroups.com> <https://groups.google.com/d/msgid/prismmodelchecker/c9bfc9f8-c192-4625-a634-8a73714920f9n%40googlegroups.com?utm_medium=email&utm_source=footer <https://groups.google.com/d/msgid/prismmodelchecker/c9bfc9f8-c192-4625-a634-8a73714920f9n%40googlegroups.com?utm_medium=email&utm_source=footer>>.

>
> --
> 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/fa728daa-099d-4dea-98e8-4410637fb79an%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/fa728daa-099d-4dea-98e8-4410637fb79an%40googlegroups.com?utm_medium=email&utm_source=footer>.