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?
