Hello all,

I think there are bugs in the methods to handle the reward-bounded until in the MRMC. The problem occurs with the latest version 1.5 as well as the version in the repository. As already pointed out by David Jansen in a comment in transient_ctmrm.c at lines 644 and 645, I think the rounding should be different. When changing these lines it seems to work. The problem also occurs in practise, for instance the results for time bounds 0.99 and 1.0 are completely different. The discretisation factor needs to be quite small to be accepted by MRMC, such that the model checking process takes a lot of time, but I think this is not a bug.

For the uniformisation method, I get completely useless results, although I set the parameter "w" to a rather small value.

The attachment contains the archive bugreport.zip to demonstrate this phenomenon. The model files are google_mrmc.tra, google_mrmc.lab, google_mrmc.rew and google_mrmc.lab. The file input_dis.inp demonstrates that the discretisation method is seemingly broken and input_uni.inp is for the uniformisation method.

I'm not sure who is currently responsible for this part of the MRMC. It would be nice if the problem could be handled in time. We are currently preparing a paper for MSCS and want to add some experimental results involving the reward-bounded until for a model similar to the one in the attachment.

Best regards, Moritz