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

* src/tgbaalgos/randomgraph.cc (random_graph): Do not use the

Browse source 
pointer of the state created as keys in sets; otherwise the graph
created depends on the memory layout.
This commit is contained in:
Alexandre Duret-Lutz 2004-12-10 15:10:19 +00:00
parent d4b9ebaaff
commit 8b8257b157
2 changed files with 21 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,3 +1,9 @@
2004-12-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/randomgraph.cc (random_graph): Do not use the
pointer of the state created as keys in sets; otherwise the graph
created depends on the memory layout.
2004-12-09 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-12-09 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgba/tgbaexplicit.cc (tgba_explicit::create_transition): * src/tgba/tgbaexplicit.cc (tgba_explicit::create_transition):

24
src/tgbaalgos/randomgraph.cc
View file

@ -28,7 +28,6 @@
#include <list> #include <list>
#include <set> #include <set>
#include <iterator> #include <iterator>
#include "misc/hash.hh"
namespace spot namespace spot
{ {
@ -123,15 +122,22 @@ namespace spot
// Using Sgi::hash_set instead of std::set for these sets is 3 // Using Sgi::hash_set instead of std::set for these sets is 3
// times slower (tested on a 50000 nodes example). // times slower (tested on a 50000 nodes example). Use an int
typedef std::set<tgba_explicit::state*> node_set; // (the index into states[]), not the tgba_explicit::state*
// directly, because the later would yield different graph
// depending on the memory layout.
typedef std::set<int> node_set;
node_set nodes_to_process; node_set nodes_to_process;
node_set unreachable_nodes; node_set unreachable_nodes;
nodes_to_process.insert(states[0] = res->add_state(st(0))); states[0] = res->add_state(st(0));
nodes_to_process.insert(0);
for (int i = 1; i < n; ++i) for (int i = 1; i < n; ++i)
unreachable_nodes.insert(states[i] = res->add_state(st(i))); {
states[i] = res->add_state(st(i));
unreachable_nodes.insert(i);
}
// We want to connect each node to a number of successors between // We want to connect each node to a number of successors between
// 1 and n (with probability d). This follow // 1 and n (with probability d). This follow
@ -139,7 +145,7 @@ namespace spot
while (!nodes_to_process.empty()) while (!nodes_to_process.empty())
{ {
tgba_explicit::state* src = *nodes_to_process.begin(); tgba_explicit::state* src = states[*nodes_to_process.begin()];
nodes_to_process.erase(nodes_to_process.begin()); nodes_to_process.erase(nodes_to_process.begin());
// Choose a random number of successors (at least one), using // Choose a random number of successors (at least one), using
@ -163,7 +169,7 @@ namespace spot
std::advance(i, index); std::advance(i, index);
// Link it from src. // Link it from src.
random_labels(res, src, *i, props, props_n, t, accs, a); random_labels(res, src, states[*i], props, props_n, t, accs, a);
nodes_to_process.insert(*i); nodes_to_process.insert(*i);
unreachable_nodes.erase(i); unreachable_nodes.erase(i);
@ -182,10 +188,10 @@ namespace spot
random_labels(res, src, dest, props, props_n, t, accs, a); random_labels(res, src, dest, props, props_n, t, accs, a);
node_set::iterator j = unreachable_nodes.find(dest); node_set::iterator j = unreachable_nodes.find(index);
if (j != unreachable_nodes.end()) if (j != unreachable_nodes.end())
{ {
nodes_to_process.insert(dest); nodes_to_process.insert(index);
unreachable_nodes.erase(j); unreachable_nodes.erase(j);
saw_unreachable = true; saw_unreachable = true;
} }