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

randomgraph: Use tgba_digraph.

Browse source 
* src/graph/graph.hh (new_states): Call reserve().
* src/tgbaalgos/randomgraph.cc: Use tgba_digraph
instead of tgba_string_explicit.
This commit is contained in:
Alexandre Duret-Lutz 2014-06-26 23:13:19 +02:00
parent 4170080c35
commit c93b41a2c7
2 changed files with 26 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/graph/graph.hh
View file

@ -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>(args)...);
return s;

66
src/tgbaalgos/randomgraph.cc
View file

@ -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 <http://www.gnu.org/licenses/>.
#include "randomgraph.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgba/tgbagraph.hh"
#include "misc/random.hh"
#include "ltlast/atomic_prop.hh"
#include <sstream>
@ -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<bdd>& 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<state_explicit_string*> states(n);
// Indirect access to state[] to help random selection of successors.
std::vector<int> state_randomizer(n);
for (auto i: *ap)
props[pi++] = dict->register_proposition(i, res);
std::list<bdd> 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<bdd>::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<unsigned> 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());