alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

randltl: do not reset the seed between formulas

Browse source 
Reported by Joachim Klein.

* src/bin/randltl.cc: Here.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2014-08-21 13:23:36 +02:00
parent 44fc323e7b
commit 2227ad60cf
2 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -35,6 +35,10 @@ New in spot 1.2.4a (not yet released)
this was actually hiding the formulas for people using a this was actually hiding the formulas for people using a
terminal with white background... This version displays formula terminal with white background... This version displays formula
in bright blue instead. in bright blue instead.
- 'randltl -n -1 --seed 0' and 'randltl -n -1 --seed 1' used to
generate nearly the same list of formulas, shifted by one,
because the PRNG write reset with an incremented seed between
each output formula. The PRNG is now reset only once.
New in spot 1.2.4 (2014-05-15) New in spot 1.2.4 (2014-05-15)

4
src/bin/randltl.cc
View file

@ -379,9 +379,10 @@ main(int argc, char** argv)
error(2, 0, "No atomic proposition supplied? Run '%s --help' for usage.", error(2, 0, "No atomic proposition supplied? Run '%s --help' for usage.",
program_name); program_name);
spot::srand(opt_seed);
typedef Sgi::hash_set<const spot::ltl::formula*, typedef Sgi::hash_set<const spot::ltl::formula*,
const spot::ptr_hash<const spot::ltl::formula> > fset_t; const spot::ptr_hash<const spot::ltl::formula> > fset_t;
fset_t unique_set; fset_t unique_set;
spot::ltl::ltl_simplifier simpl(simplifier_options()); spot::ltl::ltl_simplifier simpl(simplifier_options());
@ -392,7 +393,6 @@ main(int argc, char** argv)
unsigned trials = MAX_TRIALS; unsigned trials = MAX_TRIALS;
bool ignore; bool ignore;
const spot::ltl::formula* f = 0; const spot::ltl::formula* f = 0;
spot::srand(opt_seed++);
do do
{ {
ignore = false; ignore = false;