sjunges
commented
4 years ago This occurs with sparse model building. I propose that at leat with the option -ec this needs to be checked, and possibly in debug mode before model checking.
As the issue has been around for ages and this is the only report about this problem, I do not think it is urgent. I therefore label it as a good first issue and defer solving it to someone working on the model builder.
For the symbolic model building, there is a warning. We might want to make this an error.
When specifying negative rewards in a PRISM model, there is no error message but weird values are computed. According to Christian Hensel, negative rewards shall never be specified.