Error "command sum to zero" with not activated transition

[koelblfro...@gmail.com]

Hi,

with the example code below Prism 4.4 throws an error message:
"Error: Rates in command 1 of module "FASIC" sum to zero for some states. Perhaps some of the updates give out-of-range values. One possible solution is to strengthen the guard (line 7, column 9)."

But of course the transition is never activated and as such there can be no error. The problem appeared in a more complex model, but the example is a minimal example of the problem.

Is this a bug or normal?

Bye

Example code:
ctmc

module FASIC   
    tmp:  [0..3] init 0;
    tmp2: bool init false;
    [](tmp2=true)->(tmp'=tmp+1);
endmodule

[Gethin Norman]

This is normal behaviour - the checks are performed before the reachable states are computed so it considers all possible states of the model, i.e. all possible values for the variables.

thanks

Gethin

> --
> 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.
> To post to this group, send email to prismmod...@googlegroups.com.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.