Re: [Javapathfinder-user] JPF - increase memory? (statechart extension)

[Peter C. M. <Pet...@na...>]

Elisabeth,

the default from the bin/jpf script is -Xmx1024m, which might explain  
why there were less states (apart from a rather small search depth  
limit of 8). Remove the search depth limit, increase the heap, but  
first make sure that JPF instruction logging is turned off (use  
"+jpf.report.console.property_violation=error:snapshot", i.e. no  
'trace' topic). If you ever get to traces, you probably are more  
interested in UML events than Java instructions, i.e. use the  
ChoiceTracker listener to create event traces.

6000 transitions should not impose problems, unless your transitions  
contain lots of changes in large arrays and lots of instructions. You  
have to distinguish between UML states and program states, and the  
first step is to find out of they correspond. Are there any threads  
used in our model? Are there random variables? Do you use  
Verify.getInt()/Boolean() etc.? If so, you will have (potentially a  
lot) more program states than UML states.

How does JPF react to the out-of-memory - does it just die, or does it  
report hitting a search constraint? What if you increase the  
+search.min_free property? You can also run with  
+jpf.listener=.tools.SearchMonitor to see how many program states /  
instructions you get executed

-- Peter


On Jul 11, 2008, at 8:19 AM, 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