From 2183276008859644631b8ecc640c83ae254b97c3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 23 Feb 2010 17:20:59 +0100 Subject: [PATCH] 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. --- ChangeLog | 20 ++++++++++++++++++++ src/tgbaalgos/randomgraph.cc | 24 ++++++++++++++++-------- src/tgbatest/Makefile.am | 3 ++- src/tgbatest/randtgba.test | 34 ++++++++++++++++++++++++++++++++++ 4 files changed, 72 insertions(+), 9 deletions(-) create mode 100755 src/tgbatest/randtgba.test diff --git a/ChangeLog b/ChangeLog index 89a1c5ebc..4704e4c93 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,23 @@ +2010-02-23 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. + 2010-02-17 Alexandre Duret-Lutz ltl2tgba cgi updates. diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index a06b68d1d..5c258a98e 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -108,6 +108,8 @@ namespace spot 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); std::list 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; } diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 65ea2eba0..9338091b8 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2009 Laboratoire de Recherche et Développement +## Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -91,6 +91,7 @@ TESTS = \ reduccmp.test \ reductgba.test \ scc.test \ + randtgba.test \ emptchk.test \ emptchke.test \ dfs.test \ diff --git a/src/tgbatest/randtgba.test b/src/tgbatest/randtgba.test new file mode 100755 index 000000000..47ff7d7c7 --- /dev/null +++ b/src/tgbatest/randtgba.test @@ -0,0 +1,34 @@ +#!/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