Dear Martin,
... a huge CTMC model (.tra) with 797382144 STATES and 64470375837 TRANSITIONS is generated. First I noticed that MRMC "only" requests 3GB RAM which seems to be filled. In that process a core dump is generated. I noticed that MRMC seems not to load all transitions or eventually represents the transition count in a wrong way (may be a variable overflow).
I think that is it: The number of transitions is almost 2^36, but is stored by MRMC in an integer variable. Most C compilers assign 32 bits for this type. MRMC unfortunately does not check in the first two lines whether the number of states or the number of transitions exceed the bounds; the lines that contain the transitions themselves are checked a bit more thoroughly.
Before requesting space for all the transitions, MRMC makes a first pass through the file to find the out-degree of each state. These out-degrees are stored in an array of integers; in your case, that array would be 797382144 * 4 B = 2,97 GB large. After the first pass through the file, MRMC allocates space for the actual transitions: initially 12 B per transition, which will later be extended by another 4 B for the so-called backsets. However, it only allocates space for 45866397 transitions (= 64470375837 modulo 2^32), i. e. 525 KB. When this space is full, MRMC will (without checking further) store remaining transitions outside its assigned memory, which then leads to the core dump. I think this is why MRMC uses (a bit more than) 3 GB before crashing.
Kind regards, David N. Jansen.