diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index f052dd94c..1e4197244 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -23,6 +23,7 @@ #include "randomgraph.hh" #include "tgba/tgbagraph.hh" #include "misc/random.hh" +#include "misc/bddlt.hh" #include "ltlast/atomic_prop.hh" #include #include @@ -35,12 +36,59 @@ namespace spot namespace { - void - random_labels(tgba_digraph_ptr aut, - unsigned src, - unsigned dest, - int* props, int props_n, float t, - unsigned n_accs, float a) + unsigned + random_deterministic_labels_rec(std::vector& labels, int *props, + int props_n, bdd current, unsigned n) + { + if (n > 1 && props_n >= 1) + { + bdd ap = bdd_ithvar(*props); + ++props; + --props_n; + + // There are m labels generated from "current & ap" + // and n - m labels generated from "current & !ap" + unsigned m = rrand(1, n - 1); + if (2 * m < n) + { + m = n - m; + ap = !ap; + } + + unsigned res = random_deterministic_labels_rec(labels, props, + props_n, + current & ap, m); + res += random_deterministic_labels_rec(labels, props, props_n, + current & !ap, n - res); + return res; + } + else + { + labels.push_back(current); + return 1; + } + } + + std::vector + random_deterministic_labels(int *props, int props_n, unsigned n) + { + std::vector bddvec; + random_deterministic_labels_rec(bddvec, props, props_n, bddtrue, n); + return bddvec; + } + + acc_cond::mark_t + random_acc_cond(tgba_digraph_ptr aut, unsigned n_accs, float a) + { + acc_cond::mark_t m = 0U; + for (unsigned i = 0U; i < n_accs; ++i) + if (drand() < a) + m |= aut->acc().mark(i); + return m; + } + + bdd + random_labels(int* props, int props_n, float t) { int val = 0; int size = 0; @@ -62,18 +110,14 @@ namespace spot if (size > 0) p &= bdd_ibuildcube(val, size, props); - acc_cond::mark_t m = 0U; - for (unsigned i = 0U; i < n_accs; ++i) - if (drand() < a) - m |= aut->acc().mark(i); - aut->new_transition(src, dest, p, m); + return p; } } tgba_digraph_ptr random_graph(int n, float d, const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, - unsigned n_accs, float a, float t) + unsigned n_accs, float a, float t, bool deterministic) { assert(n > 0); auto res = make_tgba_digraph(dict); @@ -117,20 +161,35 @@ namespace spot // Choose a random number of successors (at least one), using // a binomial distribution. - int nsucc = 1 + bin.rand(); + unsigned 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--) + + // Create NSUCC random labels. + std::vector labels; + if (deterministic) { + labels = random_deterministic_labels(props, props_n, nsucc); + + // if nsucc > 2^props_n, we cannot produce nsucc deterministic + // transitions so we set it to labels.size() + nsucc = labels.size(); + } + else + for (unsigned i = 0; i < nsucc; ++i) + labels.push_back(random_labels(props, props_n, t)); + + int possibilities = n; + unsigned dst; + for (auto& l: labels) + { + acc_cond::mark_t m = random_acc_cond(res, n_accs, a); + // No connection to unreachable successors so far. This // is our last chance, so force it now. - if (nsucc == 0 - && !saw_unreachable - && !unreachable_nodes.empty()) + if (--nsucc == 0 + && !unreachable_nodes.empty() + && !saw_unreachable) { // Pick a random unreachable node. int index = mrand(unreachable_nodes.size()); @@ -138,32 +197,29 @@ namespace spot std::advance(i, index); // Link it from src. - random_labels(res, src, *i, props, props_n, t, n_accs, a); + res->new_transition(src, *i, l, m); nodes_to_process.insert(*i); - unreachable_nodes.erase(i); + unreachable_nodes.erase(*i); break; } - else - { - // Pick the index of a random node. - int index = mrand(possibilities--); - // Permute it with state_randomizer[possibilities], so - // we cannot pick it again. - auto x = state_randomizer[index]; - state_randomizer[index] = state_randomizer[possibilities]; - state_randomizer[possibilities] = x; + // Pick the index of a random node. + int index = mrand(possibilities--); - random_labels(res, src, x, props, props_n, t, n_accs, a); + // Permute it with state_randomizer[possibilities], so + // we cannot pick it again. + dst = state_randomizer[index]; + state_randomizer[index] = state_randomizer[possibilities]; + state_randomizer[possibilities] = dst; - auto j = unreachable_nodes.find(x); - if (j != unreachable_nodes.end()) - { - nodes_to_process.insert(x); - unreachable_nodes.erase(j); - saw_unreachable = true; - } - } + res->new_transition(src, dst, l, m); + auto j = unreachable_nodes.find(dst); + if (j != unreachable_nodes.end()) + { + nodes_to_process.insert(dst); + unreachable_nodes.erase(j); + saw_unreachable = true; + } } // The node must have at least one successor. diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index aa6877449..bbcfaf7d5 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -78,7 +78,8 @@ namespace spot SPOT_API tgba_digraph_ptr random_graph(int n, float d, const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, - unsigned n_accs = 0, float a = 0.1, float t = 0.5); + unsigned n_accs = 0, float a = 0.1, float t = 0.5, + bool deterministic = false); } #endif // SPOT_TGBAALGOS_RANDOMGRAPH_HH diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 5e05c945c..38658e8b5 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -122,6 +122,7 @@ syntax(char* prog) << " -n N number of nodes of the graph [20]" << std::endl << " -t F probability of the atomic propositions to be true" << " [0.5]" << std::endl + << " -det generate a deterministic and complete graph [false]" << std::endl << "LTL Formula Generation Options:" << std::endl << " -dp dump priorities, do not generate any formula" @@ -560,6 +561,7 @@ main(int argc, char** argv) float opt_d = 0.2; int opt_n = 20; float opt_t = 0.5; + bool opt_det = false; bool opt_0 = false; bool opt_z = false; @@ -668,6 +670,10 @@ main(int argc, char** argv) if (!opt_ec) opt_ec = 1; } + else if (!strcmp(argv[argn], "-det")) + { + opt_det = true; + } else if (!strcmp(argv[argn], "-e")) { if (argc < argn + 2) @@ -908,7 +914,7 @@ main(int argc, char** argv) spot::tgba_digraph_ptr a = spot::random_graph(opt_n, opt_d, apf, dict, - opt_n_acc, opt_a, opt_t); + opt_n_acc, opt_a, opt_t, opt_det); if (formula) a = spot::product(formula, a);