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