PRISM update doesn't do anything warning

[Robert Goldman]

In a PRISM dtmc, sometimes I want to have a command where with some probability, p, something happens, but with probability 1 - p nothing happens (i.e., the transition is a self-loop).

When I try to do this, either by making the update be "true" or making the update set a primed value to the same as its current value, PRISM gives me a warning that my update doesn't do anything.  Is there any way to tell PRISM "yes, I know -- that update is not meant to do anything"?

Looking at the source code in prism/src/symbolic/build/Modules2MTBDD.java it looks like the warning is unconditional. What if one was to treat an update of just `true` as distinct, and suppress the warning in that case?

[Dave Parker]

Hi Robert,

Updates that do not change the state (e.g. specified by "true") are
normal and should not trigger any warning, so there must be something
else going on. Feel free to send the model an I'll take a look.

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, visit https://groups.google.com/d/msgid/
> prismmodelchecker/2e21b757-96a8-47fd-
> aaab-07232bff08b4n%40googlegroups.com <https://groups.google.com/d/
> msgid/prismmodelchecker/2e21b757-96a8-47fd-
> aaab-07232bff08b4n%40googlegroups.com?utm_medium=email&utm_source=footer>.