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

[<wo...@in...>]

Hello Peter,

I tried all your suggestions.
My commands were most of the time:
+log.info=gov.nasa.jpf.sc  gov.nasa.jpf.sc.StateMachine Statechart
+jpf.report.console.property_violation=error:snapshot
+jpf.listener=.tools.ChoiceTracker
+choice.class=.jvm.choice.sc.SCEventGenerator

and sometimes:
+search.depth_limit=8 (to find a trace with 7 steps)

I have boolean and string variables which are checked (in guards) or set
(in actions). In my small example it worked fine with ChoiceTracker and I
found a trace to tripmode:
the variable was false at the beginning: boolean tripmodeactive = false
an action to set tripmode:
void setTripmode(){tripmodeactive = true;}
I have a guard with tripmode-check (and the constraint to check):
assert !tripmodeactive : "Tripmode = true";
if (tripmodeactive) {
  setNextState(stateC507_10235);
} else {
  setNextState(stateC507_179);
}

The following trace was shown:
====================================================== choice trace #1
INPUT_RIGHTtoC179()
INPUT_PRESStoC180()
INPUT_NAVItoC181()
INPUT_WESTtoC182()
INPUT_OPTIONStoC183()
INPUT_PRESStoC184()
INPUT_RIGHTtoC185()

This is what I was looking for. So I started to test the huge model, but
here it always stops like that:

[SEVERE] JPF out of memory

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       0:01:00
states:             new=77, visited=78, backtracked=78, end=0
search:             maxDepth=76, constraints=0
choice generators:  thread=1, data=77
heap:               gc=230, new=16279, free=175
instructions:       4110692
max memory:         63MB
loaded code:        classes=1735, methods=20281

====================================================== search finished:
14.07.08 14:43

The search states didn't change, when I added the vm-command -xmx512m.
When I start JPF in Eclipse without this command, it takes about 1 or 2
minutes - with the command it takes about 20 minutes. The visited states
etc. are the same. When I added the search-limit with 8, less states were
searched.

I have no large arrays or many instructions, it's just a simple
if-construct for a guard and in an action I assign a new value to a
variable. I have no random variables or threads. I don't use the
Verify.getInt()-commands.
When I changed the +search.min_free property to a higher value, less
states were explored.

I couldn't see the search monitor with the big model, with the small
example it worked.

Thank you very much for your fast replies and support!

Best regards, Elisabeth

> 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
>