Dear David, many thanks for you reply.
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.
I noticed that and adapted the variable types from int to long.
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.
That size (2,97 GB) corresponds to what htop shows.
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.
Do you think allocating more space is feasible in (case it's physical available).
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.
I'll try to find a work around for that. Best regards Martin Am Mi 19.11.2014 10:07 schrieb David N. Jansen <dnjansen@cs.ru.nl>:
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.