Commit 21832760 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Fix random_graph() not to generate dead states.

This is actually the third time I fix random_graph().  On
2007-02-06 I changed the function not to generated dead states,
but in a way that made it non-deterministic.  On 2010-01-20 I made
the function deterministic again, but it started to generate dead
states as a side effect.  This time, I'm making sure that dead
states won't come again with a test-case that we should have had
from the beginning.

* src/tgbaalgos/randomgraph.cc (random_graph): Add an extra
indirection array, state_randomizer[], so that we can reorder
states indices after a random selection without actually changing
the value of the indices used by unreachable_states and
nodes_to_process.
* src/tgbatest/randtgba.test: New file.
* src/tgbatest/Makefile.am: Add randtgba.test.
parent 72b7deec
2010-02-23 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix random_graph() not to generate dead states.
This is actually the third time I fix random_graph(). On
2007-02-06 I changed the function not to generated dead states,
but in a way that made it non-deterministic. On 2010-01-20 I made
the function deterministic again, but it started to generate dead
states as a side effect. This time, I'm making sure that dead
states won't come again with a test-case that we should have had
from the beginning.
* src/tgbaalgos/randomgraph.cc (random_graph): Add an extra
indirection array, state_randomizer[], so that we can reorder
states indices after a random selection without actually changing
the value of the indices used by unreachable_states and
nodes_to_process.
* src/tgbatest/randtgba.test: New file.
* src/tgbatest/Makefile.am: Add randtgba.test.
2010-02-17 Alexandre Duret-Lutz <adl@lrde.epita.fr>
ltl2tgba cgi updates.
......
......@@ -108,6 +108,8 @@ namespace spot
props[pi++] = dict->register_proposition(*i, res);
std::vector<tgba_explicit::state*> states(n);
// Indirect access to state[] to help random selection of successors.
std::vector<int> state_randomizer(n);
std::list<bdd> accs;
bdd allneg = bddtrue;
......@@ -134,11 +136,13 @@ namespace spot
node_set unreachable_nodes;
states[0] = res->add_state(st(0));
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);
}
......@@ -163,6 +167,8 @@ namespace spot
int possibilities = n;
while (nsucc--)
{
// No connection to unreachable successors so far. This
// is our last chance, so force it now.
if (nsucc == 0
&& !saw_unreachable
&& !unreachable_nodes.empty())
......@@ -180,21 +186,23 @@ namespace spot
}
else
{
// Pick a random node.
// Pick the index of a random node.
int index = mrand(possibilities--);
tgba_explicit::state* dest = states[index];
// Permute the state with states[possibilities], so we
// cannot pick it again.
states[index] = states[possibilities];
states[possibilities] = dest;
// Permute it with state_randomizer[possibilities], so
// we cannot pick it again.
int x = state_randomizer[index];
state_randomizer[index] = state_randomizer[possibilities];
state_randomizer[possibilities] = x;
tgba_explicit::state* dest = states[x];
random_labels(res, src, dest, props, props_n, t, accs, a);
node_set::iterator j = unreachable_nodes.find(possibilities);
node_set::iterator j = unreachable_nodes.find(x);
if (j != unreachable_nodes.end())
{
nodes_to_process.insert(possibilities);
nodes_to_process.insert(x);
unreachable_nodes.erase(j);
saw_unreachable = true;
}
......
## Copyright (C) 2009 Laboratoire de Recherche et Dveloppement
## Copyright (C) 2009, 2010 Laboratoire de Recherche et Dveloppement
## de l'Epita (LRDE).
## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
## Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
......@@ -91,6 +91,7 @@ TESTS = \
reduccmp.test \
reductgba.test \
scc.test \
randtgba.test \
emptchk.test \
emptchke.test \
dfs.test \
......
#!/bin/sh
# Copyright (C) 2010 Laboratoire de Recherche et Development de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with Spot; see the file COPYING. If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.
. ./defs
set -e
for n in 10 20 30 40 50 60 70 80 90 100 200 500 1000; do
# Make sure graph generated by randtgba have successors for each
# of their $n nodes.
r=`../randtgba -n $n a b c | sed -n 's/^"S\([0-9]*\)".*/\1/p' |
sort -u | wc -l`
if test "$r" -eq "$n"; then :; else
echo "test failed for n=$n"
exit 1
fi
done
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment