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(a)informatik.uni-kl.de
