From: <wo...@in...> - 2008-07-14 12:21:16
|
It is finite state (or at least should be). There are just boolean and string variables (altogether about 1400). The integer variables are not implemented yet. Maybe it is really just too big. I'm wondering if a model checker like SPIN or NuSMV could handle the model. Thank you for your help so far! Best regards, Elisabeth > The model may simply be too big. > Is it finite state? ( am not asking about the number of states in the > UML statechart, but rather the states that are explored by JPF: Do you > have some variables that maybe are incremented in an infinite loop? > I hope this helps, > Corina > > wo...@in... wrote: >> Hello JPF-Team, >> >> the JPF Statechart Extension is working well with a small example, but >> with my huge statechart-model I'll get the message >> >> [SEVERE] JPF out of memory >> >> . How can I increase the max memory? Do you have other ideas, how it >> will >> work better? >> >> I tried the VM-command -Xmx512M and "+search.depth_limit=8" but, as a >> result, the same or less states were checked. The model is really huge >> with about 1000 states and 6000 transitions. >> >> Thank you very much in advance, >> >> Elisabeth >> >> >> ------------------------------------------------------------------------- >> Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW! >> Studies have shown that voting for your favorite open source project, >> along with a healthy diet, reduces your potential for chronic lameness >> and boredom. Vote Now at http://www.sourceforge.net/community/cca08 >> _______________________________________________ >> Javapathfinder-user mailing list >> Jav...@li... >> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user >> > > |