From 688587d700c0ac88def0cd6e0ae67c08246e89cc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 8 Dec 2004 15:39:15 +0000 Subject: [PATCH] * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh (tgba_explicit::create_transition(state*, const state*)): New function. * src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: (random_graph): Revamp the algorithm to call rand() less often. * src/tgbatest/randtgba.cc: Add option -0 to easy profiling. --- ChangeLog | 6 ++ src/tgba/tgbaexplicit.cc | 21 +++--- src/tgba/tgbaexplicit.hh | 4 +- src/tgbaalgos/randomgraph.cc | 132 ++++++++++++++++++++++++----------- src/tgbaalgos/randomgraph.hh | 11 ++- src/tgbatest/randtgba.cc | 11 ++- 6 files changed, 129 insertions(+), 56 deletions(-) diff --git a/ChangeLog b/ChangeLog index 67939d829..483ed59a7 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,11 @@ 2004-12-08 Alexandre Duret-Lutz + * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh + (tgba_explicit::create_transition(state*, const state*)): New function. + * src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: + (random_graph): Revamp the algorithm to call rand() less often. + * src/tgbatest/randtgba.cc: Add option -0 to easy profiling. + * src/misc/random.hh: Add include guard. 2004-12-07 Alexandre Duret-Lutz diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 5fe0b5f93..d75ca9750 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -159,19 +159,22 @@ namespace spot init_ = s; } + tgba_explicit::transition* + tgba_explicit::create_transition(state* source, const state* dest) + { + transition* t = new transition; + t->dest = dest; + t->condition = bddtrue; + t->acceptance_conditions = bddfalse; + source->push_back(t); + return t; + } tgba_explicit::transition* tgba_explicit::create_transition(const std::string& source, const std::string& dest) { - tgba_explicit::state* s = add_state(source); - tgba_explicit::state* d = add_state(dest); - transition* t = new transition; - t->dest = d; - t->condition = bddtrue; - t->acceptance_conditions = bddfalse; - s->push_back(t); - return t; + return create_transition(add_state(source), add_state(dest)); } void @@ -243,7 +246,7 @@ namespace spot for (t1 = i->second->begin(); t1 != i->second->end(); ++t1) { bdd acc = (*t1)->acceptance_conditions; - state* dest = (*t1)->dest; + const state* dest = (*t1)->dest; // Find another transition with the same destination and // acceptance conditions. diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index ed55d141a..08492b99d 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -48,13 +48,15 @@ namespace spot { bdd condition; bdd acceptance_conditions; - state* dest; + const state* dest; }; void set_init_state(const std::string& state); transition* create_transition(const std::string& source, const std::string& dest); + transition* + create_transition(state* source, const state* dest); void add_condition(transition* t, const ltl::formula* f); /// This assumes that all variables in \a f are known from dict. diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index 79c646293..e60583211 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -27,6 +27,8 @@ #include #include #include +#include +#include "misc/hash.hh" namespace spot { @@ -51,14 +53,29 @@ namespace spot void random_labels(tgba_explicit* aut, - const std::string& src, const std::string& dest, - const std::list& props, float t, + tgba_explicit::state* src, const tgba_explicit::state* dest, + int* props, int props_n, float t, const std::list& accs, float a) { + int val = 0; + int size = 0; bdd p = bddtrue; - for (std::list::const_iterator i = props.begin(); - i != props.end(); ++i) - p &= (drand() < t ? bdd_ithvar : bdd_nithvar)(*i); + while (props_n) + { + if (size == 8 * sizeof(int)) + { + p &= bdd_ibuildcube(val, size, props); + props += size; + val = 0; + size = 0; + } + val <<= 1; + val |= (drand() < t); + ++size; + --props_n; + } + if (size > 0) + p &= bdd_ibuildcube(val, size, props); bdd ac = bddfalse; for (std::list::const_iterator i = accs.begin(); @@ -80,10 +97,15 @@ namespace spot { tgba_explicit* res = new tgba_explicit(dict); - std::list props; + int props_n = ap->size(); + int* props = new int[props_n]; + + int pi = 0; for (ltl::atomic_prop_set::const_iterator i = ap->begin(); i != ap->end(); ++i) - props.push_back(dict->register_proposition(*i, res)); + props[pi++] = dict->register_proposition(*i, res); + + std::vector states(n); std::list accs; bdd allneg = bddtrue; @@ -99,56 +121,82 @@ namespace spot for (std::list::iterator i = accs.begin(); i != accs.end(); ++i) *i &= bdd_exist(allneg, *i); - typedef std::set node_set; + + // Using Sgi::hash_set instead of std::set for these sets is 3 + // times slower (tested on a 50000 nodes example). + typedef std::set node_set; node_set nodes_to_process; node_set unreachable_nodes; - nodes_to_process.insert(st(0)); + nodes_to_process.insert(states[0] = res->add_state(st(0))); for (int i = 1; i < n; ++i) - unreachable_nodes.insert(st(i)); + unreachable_nodes.insert(states[i] = res->add_state(st(i))); + + // We want to connect each node to a number of successors between + // 1 and n (with probability d). This follow + barand bin(n - 1, d); while (!nodes_to_process.empty()) { - std::string src = *nodes_to_process.begin(); + tgba_explicit::state* src = *nodes_to_process.begin(); nodes_to_process.erase(nodes_to_process.begin()); - if (!unreachable_nodes.empty()) + // Choose a random number of successors (at least one), using + // a binomial distribution. + int nsucc = 1 + bin.rand(); + + // Connect to NSUCC randomly chosen successors. We want at + // least one unreachable successors among these if there are + // some. + bool saw_unreachable = false; + int possibilities = n; + while (nsucc--) { - // Pick a random unreachable node. - int index = mrand(unreachable_nodes.size()); - node_set::const_iterator i; - for (i = unreachable_nodes.begin(); index; ++i, --index) - assert(i != unreachable_nodes.end()); - - // Link it from src. - random_labels(res, src, *i, props, t, accs, a); - - nodes_to_process.insert(*i); - unreachable_nodes.erase(i); - } - // Randomly link node to another node (including itself). - for (int i = 0; i < n; ++i) - { - if (drand() >= d) - continue; - - std::string dest = st(i); - - random_labels(res, src, dest, props, t, accs, a); - - node_set::iterator j = unreachable_nodes.find(dest); - if (j != unreachable_nodes.end()) + if (nsucc == 0 + && !saw_unreachable + && !unreachable_nodes.empty()) { - nodes_to_process.insert(dest); - unreachable_nodes.erase(j); + // Pick a random unreachable node. + int index = mrand(unreachable_nodes.size()); + node_set::const_iterator i = unreachable_nodes.begin(); + std::advance(i, index); + + // Link it from src. + random_labels(res, src, *i, props, props_n, t, accs, a); + + nodes_to_process.insert(*i); + unreachable_nodes.erase(i); + break; + } + else + { + // Pick a random node. + int index = mrand(possibilities--); + tgba_explicit::state* dest = states[index]; + + // Permute the state with states[possibilities], so we + // cannot pick it again. + states[index] = states[possibilities]; + states[possibilities] = dest; + + random_labels(res, src, dest, props, props_n, t, accs, a); + + node_set::iterator j = unreachable_nodes.find(dest); + if (j != unreachable_nodes.end()) + { + nodes_to_process.insert(dest); + unreachable_nodes.erase(j); + saw_unreachable = true; + } } } - - // Avoid dead ends. - if (res->add_state(src)->empty()) - random_labels(res, src, src, props, t, accs, a); + // The node must have at least one successor. + assert(!src->empty()); } + // All nodes must be reachable. + assert(unreachable_nodes.empty()); + delete[] props; return res; } diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index e4afe40dd..fec64cb3f 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -65,8 +65,15 @@ namespace spot /// note = {Reprint of Master's thesis} /// } /// \endverbatim - /// The only difference is that labels are on transitions, and that - /// acceptance conditions are handled. Otherwise the logic is the same. + /// + /// Although the intent is similar, there are some differences with + /// between the above published algorithm and this implementation . + /// First labels are on transitions, and acceptance conditions are + /// generated too. Second, the number of successors of a node is + /// chosen in \f$[1,n]\f$ following a normal distribution with mean + /// \f$1+(n-1)d\f$ and variance \f$(n-1)d(1-d)\f$. (This is less + /// accurate, but faster than considering all possible \a n + /// successors one by one.) tgba* random_graph(int n, float d, const ltl::atomic_prop_set* ap, bdd_dict* dict, diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 20eb69398..37fab16c5 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -111,6 +111,8 @@ syntax(char* prog) std::cerr << "Usage: "<< prog << " [OPTIONS...] PROPS..." << std::endl << std::endl << "Options:" << std::endl + << " -0 suppress default output, just generate the graph" + << " in memory" << std::endl << " -a N F number of acceptance conditions and probability that" << " one is true" << std::endl << " [0 0.0]" << std::endl @@ -334,6 +336,7 @@ main(int argc, char** argv) int opt_n = 20; float opt_t = 0.5; + bool opt_0 = false; bool opt_z = false; bool opt_Z = false; @@ -357,7 +360,11 @@ main(int argc, char** argv) while (++argn < argc) { - if (!strcmp(argv[argn], "-a")) + if (!strcmp(argv[argn], "-0")) + { + opt_0 = true; + } + else if (!strcmp(argv[argn], "-a")) { if (argc < argn + 3) syntax(argv[0]); @@ -459,7 +466,7 @@ main(int argc, char** argv) { if (opt_dot) dotty_reachable(std::cout, a); - else + else if (!opt_0) tgba_save_reachable(std::cout, a); } else