Re: [Javapathfinder-user] about ChoiceGenerator

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

either from the command line (like "+velocity.class=..."), or from  
any of the JPF property files (preferably mode property file, as you  
should try to avoid changing default.properties). Please see the  
"Configuring JPF Runtime Options" page on the website docu.

- Peter


On Dec 13, 2007, at 1:39 PM, H CC wrote:

> Hello, from  http://javapathfinder.sourceforge.net/doc/ 
> ChoiceGenerators.html (ChoiceGenerator),
> we can see an example:
>
> double v = Verify.getDouble("velocity");
>
> and "velocity" can be configured by:
>
> velocity.class = gov.nasa.jpf.jvm.choice.DoubleThreholdGenerator
> velocity.threhold = 13250
> velocity.delta = 500
>
> but can anyone tell me where we can do the configuration, and show  
> me a simple example.
>
> Thank you.
>
> Harold
>
> Express yourself instantly with MSN Messenger! MSN Messenger
> ---------------------------------------------------------------------- 
> ---
> SF.Net email is sponsored by:
> Check out the new SourceForge.net Marketplace.
> It's the best place to buy or sell services
> for just about anything Open Source.
> http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/ 
> marketplace_______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user