From c93b41a2c725752c91b93a64a5082d53418293e8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Jun 2014 23:13:19 +0200 Subject: [PATCH] randomgraph: Use tgba_digraph. * src/graph/graph.hh (new_states): Call reserve(). * src/tgbaalgos/randomgraph.cc: Use tgba_digraph instead of tgba_string_explicit. --- src/graph/graph.hh | 1 + src/tgbaalgos/randomgraph.cc | 66 ++++++++++++++---------------------- 2 files changed, 26 insertions(+), 41 deletions(-) diff --git a/src/graph/graph.hh b/src/graph/graph.hh index c9376f600..9182c4ee1 100644 --- a/src/graph/graph.hh +++ b/src/graph/graph.hh @@ -446,6 +446,7 @@ namespace spot state new_states(unsigned n, Args&&... args) { state s = states_.size(); + states_.reserve(s + n); while (n--) states_.emplace_back(std::forward(args)...); return s; diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index 220321ec2..800a5d9cb 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2012, 2013, 2014 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -21,7 +21,7 @@ // along with this program. If not, see . #include "randomgraph.hh" -#include "tgba/tgbaexplicit.hh" +#include "tgba/tgbagraph.hh" #include "misc/random.hh" #include "ltlast/atomic_prop.hh" #include @@ -35,14 +35,6 @@ namespace spot namespace { - std::string - st(int n) - { - std::stringstream s; - s << n; - return "S" + s.str(); - } - std::string acc(int n) { @@ -52,9 +44,9 @@ namespace spot } void - random_labels(tgba_explicit_string* aut, - state_explicit_string* src, - const state_explicit_string* dest, + random_labels(tgba_digraph* aut, + unsigned src, + unsigned dest, int* props, int props_n, float t, const std::list& accs, float a) { @@ -84,9 +76,7 @@ namespace spot if (drand() < a) ac |= *i; - state_explicit_string::transition* u = aut->create_transition(src, dest); - aut->add_conditions(u, p); - aut->add_acceptance_conditions(u, ac); + aut->get_graph().new_transition(src, dest, p, ac); } } @@ -97,19 +87,14 @@ namespace spot ltl::environment* env) { assert(n > 0); - tgba_explicit_string* res = new tgba_explicit_string(dict); + auto res = new tgba_digraph(dict); 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[pi++] = dict->register_proposition(*i, res); - - std::vector states(n); - // Indirect access to state[] to help random selection of successors. - std::vector state_randomizer(n); + for (auto i: *ap) + props[pi++] = dict->register_proposition(i, res); std::list accs; bdd allneg = bddtrue; @@ -117,14 +102,14 @@ namespace spot { const ltl::formula* f = env->require(acc(i)); int v = dict->register_acceptance_variable(f, res); - res->declare_acceptance_condition(f); - allneg &= bdd_nithvar(v); - bdd b = bdd_ithvar(v); + f->destroy(); + bdd b = bdd_nithvar(v); + allneg &= b; accs.push_back(b); } - for (std::list::iterator i = accs.begin(); i != accs.end(); ++i) - *i &= bdd_exist(allneg, *i); - + res->set_acceptance_conditions(allneg); + for (auto& i: accs) + i = bdd_compose(allneg, i, bdd_var(i)); // Using std::unordered_set instead of std::set for these sets is 3 // times slower (tested on a 50000 nodes example). Use an int @@ -135,13 +120,14 @@ namespace spot node_set nodes_to_process; node_set unreachable_nodes; - states[0] = res->add_state(st(0)); + res->get_graph().new_states(n); + + std::vector state_randomizer(n); state_randomizer[0] = 0; nodes_to_process.insert(0); for (int i = 1; i < n; ++i) { - states[i] = res->add_state(st(i)); state_randomizer[i] = i; unreachable_nodes.insert(i); } @@ -153,7 +139,7 @@ namespace spot while (!nodes_to_process.empty()) { - state_explicit_string* src = states[*nodes_to_process.begin()]; + auto src = *nodes_to_process.begin(); nodes_to_process.erase(nodes_to_process.begin()); // Choose a random number of successors (at least one), using @@ -179,7 +165,7 @@ namespace spot std::advance(i, index); // Link it from src. - random_labels(res, src, states[*i], props, props_n, t, accs, a); + random_labels(res, src, *i, props, props_n, t, accs, a); nodes_to_process.insert(*i); unreachable_nodes.erase(i); break; @@ -191,15 +177,13 @@ namespace spot // Permute it with state_randomizer[possibilities], so // we cannot pick it again. - int x = state_randomizer[index]; + auto x = state_randomizer[index]; state_randomizer[index] = state_randomizer[possibilities]; state_randomizer[possibilities] = x; - state_explicit_string* dest = states[x]; + random_labels(res, src, x, props, props_n, t, accs, a); - random_labels(res, src, dest, props, props_n, t, accs, a); - - node_set::iterator j = unreachable_nodes.find(x); + auto j = unreachable_nodes.find(x); if (j != unreachable_nodes.end()) { nodes_to_process.insert(x); @@ -210,7 +194,7 @@ namespace spot } // The node must have at least one successor. - assert(!src->empty()); + assert(res->get_graph().state_storage(src).succ); } // All nodes must be reachable. assert(unreachable_nodes.empty());