Dear all,
I'm a newbie in model checking but for my PhD project a great option is model analysis. In project 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).
Do you have some experience with analysing such big models? Are there some restrictions by MRMC ?
Best Martin Groessl
----------------------------------------------------- Technical University of Kaiserslautern Department of ComputerScience
67653 Kaiserslautern,Germany Email: groessl@informatik.uni-kl.de