Dear Ignacio, I am forwarding your email to the MRMC users mailing list. The MRMC server is maintained by people in the group of Joost-Pieter Katoen, RWTH Aachen. I have just tried to download the source version myself; I can see that the email format is broken, but I have no access to the server and do not know how to repair it. The problem is that there are some lines with two line breaks instead of one. The relevant RFCs (822, ..., 5322) all prescribe that lines in emails are separated by CR LF; it may be that the current mailserver actually changes CR LF to two line breaks. The PHP mail() documentation <http://php.net/manual/en/function.mail.php> mentions that the qmail server software does so. Regarding your second question on discrete-time MDPs: No, I do not know of a mode to support discrete-time MDPs. The support for continuous-time MDPs was added to MRMC later, as a result of the research of Moritz Hahn. Kind regards, David N. Jansen. Op 17 mei 2014, om 23:03 heeft Ignacio Fernandez De La Puente <puente@in.tum.de> het volgende geschreven:

Dear David,

I found out today about your Markov Reward Model Checker (MRMC) and I must say that I am very interested. I am working with Prof. Broy at the TUM and I would like to apply it to a reward model for generating test cases for feature interaction in software production lines.

The thing is that I have been trying to download the source code and unfortunately I must say that your php server is not working properly because I did not receive the attachment with the source code. Instead, I received an email without attachment and with a binary as text. As I matter of fact I tried again with the windows file and occurred the same.

Could you please send me the version 5 of MRMC Tool (source code, windows version and linux-32 version). That would be fantastic!!=)

The last question is concerning the documentation. Unfortunately I am not familiar with continous time MDPs and I could not find if a continous MDP can be transformed into a discrete MDP. This is why I would like to ask you if your tool MRMC also support discrete time MDP's?

Thank you very much! =)

Best Regards from Munich! Ignacio FP