Hi all, I'm trying out MRMC and encountered a segfault on one of my first tries. I'm attaching the model so you can take a look. It is a smallish (~600 states) model, so I thought I would have no problems. By the way, what is the max state count MRMC can handle?
Some considerations I generated the model automatically, so I cannot give you many insights on what it does. It has CTMDPI format, but it really is not, as it has rate 1 on every transition (or else, it is a quite simple CTMDPI). The model loads with no problems One of the states (which is reachable via many other ones) is labeled "goal", when trying to verify the CSL formula P{<1}[tt U[0,10] goal] it segfaults
in fact, the upper time bound is inconsequential, I've tried setting to other values to no avail. I tried it first on an Ubuntu 9.04 64-bit machine with 2GB RAM. I thought it may have been a 64-bit issue, so I tried it too on a FreeBSD 6.4 32-bit 2GB machine but it failed too. Will try on a Mac later. I've compiled from source on both tries.
Am I doing something wrong here?
Thanks Esteban
PS on an unrelated note, what I really want to do is to do verification for MDPs. I saw MRMC does not provide MDP verification, and I thought it had steady-state CTMDPI verification, but it didn't. Can I get away with approximating via big timebounds on CTMDPIs or something like that?
Dear Esteban,
It seems to me no one is reacting on your e-mail. So I will, although I am not payed by RWTH or Twente any more. So I do it on my free will. Now, the CTMDPI part was implemented in Saarland. The persons you really would like to contact are either:
E. Moritz Hahn: emh@cs.uni-sb.de or Holger Hermanns: hermanns@cs.uni-saarland.de
The first one is the person who worked on the CTMDPI implementation, the second is the professor who guided the research of Moritz.
Best regards, Ivan.
On Fri, Jun 4, 2010 at 10:19 PM, Esteban Pavese epavese@dc.uba.ar wrote:
Hi all, I'm trying out MRMC and encountered a segfault on one of my first tries. I'm attaching the model so you can take a look. It is a smallish (~600 states) model, so I thought I would have no problems. By the way, what is the max state count MRMC can handle?
Some considerations I generated the model automatically, so I cannot give you many insights on what it does. It has CTMDPI format, but it really is not, as it has rate 1 on every transition (or else, it is a quite simple CTMDPI). The model loads with no problems One of the states (which is reachable via many other ones) is labeled "goal", when trying to verify the CSL formula P{<1}[tt U[0,10] goal] it segfaults
in fact, the upper time bound is inconsequential, I've tried setting to other values to no avail. I tried it first on an Ubuntu 9.04 64-bit machine with 2GB RAM. I thought it may have been a 64-bit issue, so I tried it too on a FreeBSD 6.4 32-bit 2GB machine but it failed too. Will try on a Mac later. I've compiled from source on both tries.
Am I doing something wrong here?
Thanks Esteban
PS on an unrelated note, what I really want to do is to do verification for MDPs. I saw MRMC does not provide MDP verification, and I thought it had steady-state CTMDPI verification, but it didn't. Can I get away with approximating via big timebounds on CTMDPIs or something like that?
MRMC-users mailing list MRMC-users@lists.rwth-aachen.de https://mailman.rwth-aachen.de/mailman/listinfo/mrmc-users
Dear all,
I already sent an answer to Esteban, but I forgot to also send it to the mailing list. You find it attached to this mail.
Best regards, Moritz
Am Montag, den 14.06.2010, 15:53 +0200 schrieb Ivan Zapreev:
Dear Esteban,
It seems to me no one is reacting on your e-mail. So I will, although I am not payed by RWTH or Twente any more. So I do it on my free will. Now, the CTMDPI part was implemented in Saarland. The persons you really would like to contact are either:
E. Moritz Hahn: emh@cs.uni-sb.de or Holger Hermanns: hermanns@cs.uni-saarland.de
The first one is the person who worked on the CTMDPI implementation, the second is the professor who guided the research of Moritz.
Best regards, Ivan.
On Fri, Jun 4, 2010 at 10:19 PM, Esteban Pavese epavese@dc.uba.ar wrote: Hi all, I'm trying out MRMC and encountered a segfault on one of my first tries. I'm attaching the model so you can take a look. It is a smallish (~600 states) model, so I thought I would have no problems. By the way, what is the max state count MRMC can handle?
Some considerations I generated the model automatically, so I cannot give you many insights on what it does. It has CTMDPI format, but it really is not, as it has rate 1 on every transition (or else, it is a quite simple CTMDPI). The model loads with no problems One of the states (which is reachable via many other ones) is labeled "goal", when trying to verify the CSL formula P{<1}[tt U[0,10] goal] it segfaults in fact, the upper time bound is inconsequential, I've tried setting to other values to no avail. I tried it first on an Ubuntu 9.04 64-bit machine with 2GB RAM. I thought it may have been a 64-bit issue, so I tried it too on a FreeBSD 6.4 32-bit 2GB machine but it failed too. Will try on a Mac later. I've compiled from source on both tries. Am I doing something wrong here? Thanks Esteban PS on an unrelated note, what I really want to do is to do verification for MDPs. I saw MRMC does not provide MDP verification, and I thought it had steady-state CTMDPI verification, but it didn't. Can I get away with approximating via big timebounds on CTMDPIs or something like that? _______________________________________________ MRMC-users mailing list MRMC-users@lists.rwth-aachen.de https://mailman.rwth-aachen.de/mailman/listinfo/mrmc-users-- Best regards,
Ivan
PS: Visit me at http://www.tainichok.ru/ _______________________________________________ MRMC-users mailing list MRMC-users@lists.rwth-aachen.de https://mailman.rwth-aachen.de/mailman/listinfo/mrmc-users
mrmc-users@lists.rwth-aachen.de
-
Ernst Moritz Hahn -
Esteban Pavese -
Ivan Zapreev