the problem is that JPF runs should be reproducible (on different
machines/OSes/times). If you use a random seed, they wouldn't, so this
shouldn't be the default. But I agree that we should have an option
for random seeds.
-- Peter
On Oct 10, 2008, at 8:03 AM, Marco Ferreira wrote:
> Currently, in ChoiceGenerator.java, the random generator is
> initialized with a seed of 42 except if cg.seed is specified. This
> means that the choice generator is not "as random" as it could be.
> Wouldn't it be a better idea to initialize it with "new Random()"
> (using the system time as seed) except if cg.seed is specified (using
> the specified value instead in that case)?
>
> I've attached a .patch file with the required changes to
> ChoiceGenerator.java in case you agree with me...
>
> Best regards,
> Marco
> <
> ChoiceGeneratorNoDefaultSeed
> .patch
> >
> -------------------------------------------------------------------------
> This SF.Net email is sponsored by the Moblin Your Move Developer's
> challenge
> Build the coolest Linux based applications with Moblin SDK & win
> great prizes
> Grand prize is a trip for two to an Open Source event anywhere in
> the world
> http://moblin-contest.org/redirect.php?banner_id=100&url=/_______________________________________________
> Javapathfinder-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel
|
