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