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

Remove some non-determinism in random_graph()

Browse source 
* src/tgbaalgos/randomgraph.cc (random_graph): Revert the part of
the patch from 2007-02-06 which silently replaced the use of state
index by state pointers.  Storing states pointer in this map cause
some non-determinism because of the memory layout.  It was almost
impossible to reproduce bugs found by tests based on randtgba.
This commit is contained in:
Alexandre Duret-Lutz 2010-01-20 15:23:32 +01:00
parent 9fb8701667
commit dcf7eed11f
2 changed files with 23 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,3 +1,13 @@
2010-01-20 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Remove some non-determinism in random_graph()
* src/tgbaalgos/randomgraph.cc (random_graph): Revert the part of
the patch from 2007-02-06 which silently replaced the use of state
index by state pointers. Storing states pointer in this map cause
some non-determinism because of the memory layout. It was almost
impossible to reproduce bugs found by tests based on randtgba.
2010-01-18 Damien Lefortier <dam@lrde.epita.fr> 2010-01-18 Damien Lefortier <dam@lrde.epita.fr>
* src/tgbaalgos/ltl2taa.cc: Fix the previous patch. * src/tgbaalgos/ltl2taa.cc: Fix the previous patch.

29
src/tgbaalgos/randomgraph.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004, 2005, 2007, 2008, 2009 Laboratoire d'Informatique de // Copyright (C) 2004, 2005, 2007, 2008, 2009, 2010 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
@ -125,32 +125,29 @@ 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). Use an int // times slower (tested on a 50000 nodes example). Use an int
// (the index into states[]), not the tgba_explicit::state* // (the index into states[]), not the tgba_explicit::state*
// directly, because the later would yield different graph // directly, because the later would yield different graphs
// depending on the memory layout. // depending on the memory layout.
typedef std::set<tgba_explicit::state*> node_set; typedef std::set<int> node_set;
node_set nodes_to_process; node_set nodes_to_process;
node_set unreachable_nodes; node_set unreachable_nodes;
{ states[0] = res->add_state(st(0));
tgba_explicit::state* init = res->add_state(st(0)); nodes_to_process.insert(0);
states[0] = init;
nodes_to_process.insert(init);
}
for (int i = 1; i < n; ++i) for (int i = 1; i < n; ++i)
{ {
tgba_explicit::state* s = res->add_state(st(i)); states[i] = res->add_state(st(i));
states[i] = s; unreachable_nodes.insert(i);
unreachable_nodes.insert(s);
} }
// 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. If the probability to connect to each successor is d,
// the number of connected successors follows a binomial distribution.
barand<nrand> bin(n - 1, d); barand<nrand> bin(n - 1, d);
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
@ -174,7 +171,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);
break; break;
@ -192,10 +189,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(possibilities);
if (j != unreachable_nodes.end()) if (j != unreachable_nodes.end())
{ {
nodes_to_process.insert(dest); nodes_to_process.insert(possibilities);
unreachable_nodes.erase(j); unreachable_nodes.erase(j);
saw_unreachable = true; saw_unreachable = true;
} }