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?