Hi all,<br>I&#39;m trying out MRMC and encountered a segfault on one of my first tries. I&#39;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?<br>

<br>Some considerations<br>I generated the model automatically, so I cannot give you many insights on what it does.<br>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<br>

One of the states (which is reachable via many other ones) is labeled &quot;goal&quot;, when trying to verify the CSL formula<br>P{&lt;1}[tt U[0,10] goal]<br>it segfaults<br><br>in fact, the upper time bound is inconsequential, I&#39;ve tried setting to other values to no avail.<br>

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&#39;ve compiled from source on both tries.<br>

<br>Am I doing something wrong here?<br><br>Thanks<br>Esteban<br><br>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&#39;t. Can I get away with approximating via big timebounds on CTMDPIs or something like that?<br>