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

ltlcross: Add a --seed option.

Browse source 
* src/bin/ltlcross.cc: Here.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2013-05-12 17:28:09 +02:00
parent 6b5b002ff9
commit 9e589422d1
2 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -30,6 +30,9 @@ New in spot 1.1a (not yet released):
the automaton. scc_filter_state() should be used when the automaton. scc_filter_state() should be used when
post-processing TGBAs that actually represent BAs. post-processing TGBAs that actually represent BAs.
- ltlcross has a new option --seed, that makes it possible to
change the seed used by the random graph generator.
* Bug fixes: * Bug fixes:
- genltl --gh-r generated the wrong formulas due to a typo. - genltl --gh-r generated the wrong formulas due to a typo.

10
src/bin/ltlcross.cc
View file

@ -54,6 +54,7 @@
#include "tgbaalgos/isdet.hh" #include "tgbaalgos/isdet.hh"
#include "misc/escape.hh" #include "misc/escape.hh"
#include "misc/hash.hh" #include "misc/hash.hh"
#include "misc/random.hh"
// Disable handling of timeout on systems that miss kill() or alarm(). // Disable handling of timeout on systems that miss kill() or alarm().
// For instance MinGW. // For instance MinGW.
@ -82,6 +83,7 @@ Exit status:\n\
#define OPT_DUPS 5 #define OPT_DUPS 5
#define OPT_NOCHECKS 6 #define OPT_NOCHECKS 6
#define OPT_STOP_ERR 7 #define OPT_STOP_ERR 7
#define OPT_SEED 8
static const argp_option options[] = static const argp_option options[] =
{ {
@ -122,6 +124,8 @@ static const argp_option options[] =
{ "density", OPT_DENSITY, "FLOAT", 0, { "density", OPT_DENSITY, "FLOAT", 0,
"probability, between 0.0 and 1.0, to add a transition between " "probability, between 0.0 and 1.0, to add a transition between "
"two states (0.1 by default)", 0 }, "two states (0.1 by default)", 0 },
{ "seed", OPT_SEED, "INT", 0,
"seed for the random number generator (0 by default)", 0 },
/**************************************************/ /**************************************************/
{ 0, 0, 0, 0, "Statistics output:", 6 }, { 0, 0, 0, 0, "Statistics output:", 6 },
{ "json", OPT_JSON, "FILENAME", OPTION_ARG_OPTIONAL, { "json", OPT_JSON, "FILENAME", OPTION_ARG_OPTIONAL,
@ -149,6 +153,7 @@ bool want_stats = false;
bool allow_dups = false; bool allow_dups = false;
bool no_checks = false; bool no_checks = false;
bool stop_on_error = false; bool stop_on_error = false;
int seed = 0;
std::vector<char*> translators; std::vector<char*> translators;
bool global_error_flag = false; bool global_error_flag = false;
@ -319,6 +324,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_NOCHECKS: case OPT_NOCHECKS:
no_checks = true; no_checks = true;
break; break;
case OPT_SEED:
seed = to_pos_int(arg);
break;
case OPT_STATES: case OPT_STATES:
states = to_pos_int(arg); states = to_pos_int(arg);
break; break;
@ -959,6 +967,7 @@ namespace
// build products with a random state-space. // build products with a random state-space.
spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f); spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f);
spot::srand(seed);
spot::tgba* statespace = spot::random_graph(states, density, ap, &dict); spot::tgba* statespace = spot::random_graph(states, density, ap, &dict);
delete ap; delete ap;
@ -1034,6 +1043,7 @@ namespace
delete pos[n]; delete pos[n];
} }
delete statespace; delete statespace;
++seed;
std::cerr << std::endl; std::cerr << std::endl;
// Shall we stop processing formulas now? // Shall we stop processing formulas now?