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
