diff --git a/ChangeLog b/ChangeLog index 529bbd582..f9345b7ea 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2004-11-12 Alexandre Duret-Lutz + * src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: New files. + * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS) + (libtgbaalgos_la_SOURCES): Add them. + * src/tgba/tgbaexplicit.hh (tgba_explicit::add_state): Make it public. + * src/tgbatest/randtgba.cc: New file. + * src/tgbatest/Makefile.am (noinst_PROGRAMS, readsave_SOURCES): Add it. + * src/tgbatest/readsave.test: Check a random graph. + * misc/random.cc, misc/random.hh: New files. * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 58bf1f53c..b87e6be60 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -73,6 +73,10 @@ namespace spot void complement_all_acceptance_conditions(); void merge_transitions(); + /// Return the tgba_explicit::state for \a name, creating the state if + /// it does not exist. + state* add_state(const std::string& name); + // tgba interface virtual ~tgba_explicit(); virtual spot::state* get_init_state() const; @@ -90,7 +94,6 @@ namespace spot virtual bdd compute_support_conditions(const spot::state* state) const; virtual bdd compute_support_variables(const spot::state* state) const; - state* add_state(const std::string& name); bdd get_acceptance_condition(const ltl::formula* f); typedef Sgi::hash_map +#include +#include + +namespace spot +{ + + namespace + { + std::string + st(int n) + { + std::stringstream s; + s << n; + return "S" + s.str(); + } + + std::string + acc(int n) + { + std::stringstream s; + s << n; + return "a" + s.str(); + } + + void + random_labels(tgba_explicit* aut, + const std::string& src, const std::string& dest, + const std::list& props, float t, + const std::list& accs, float a) + { + bdd p = bddtrue; + for (std::list::const_iterator i = props.begin(); + i != props.end(); ++i) + p &= (drand() < t ? bdd_ithvar : bdd_nithvar)(*i); + + bdd ac = bddfalse; + for (std::list::const_iterator i = accs.begin(); + i != accs.end(); ++i) + if (drand() < a) + ac |= *i; + + tgba_explicit::transition* u = aut->create_transition(src, dest); + aut->add_conditions(u, p); + aut->add_acceptance_conditions(u, ac); + } + } + + tgba* + random_graph(int n, float d, + const ltl::atomic_prop_set* ap, bdd_dict* dict, + int n_acc, float a, float t, + ltl::environment* env) + { + tgba_explicit* res = new tgba_explicit(dict); + + std::list props; + for (ltl::atomic_prop_set::const_iterator i = ap->begin(); + i != ap->end(); ++i) + props.push_back(dict->register_proposition(*i, res)); + + std::list accs; + bdd allneg = bddtrue; + for (int i = 0; i < n_acc; ++i) + { + ltl::formula* f = env->require(acc(i)); + int v = dict->register_acceptance_variable(f, res); + ltl::destroy(f); + allneg &= bdd_nithvar(v); + bdd b = bdd_ithvar(v); + accs.push_back(b); + } + for (std::list::iterator i = accs.begin(); i != accs.end(); ++i) + *i &= bdd_exist(allneg, *i); + + typedef std::set node_set; + node_set nodes_to_process; + node_set unreachable_nodes; + + nodes_to_process.insert(st(0)); + + for (int i = 1; i < n; ++i) + unreachable_nodes.insert(st(i)); + + while (!nodes_to_process.empty()) + { + std::string src = *nodes_to_process.begin(); + nodes_to_process.erase(nodes_to_process.begin()); + + if (!unreachable_nodes.empty()) + { + // Pick a random unreachable node. + int index = mrand(unreachable_nodes.size()); + node_set::const_iterator i; + for (i = unreachable_nodes.begin(); index; ++i, --index) + assert(i != unreachable_nodes.end()); + + // Link it from src. + random_labels(res, src, *i, props, t, accs, a); + + nodes_to_process.insert(*i); + unreachable_nodes.erase(i); + } + // Randomly link node to another node (including itself). + for (int i = 0; i < n; ++i) + { + if (drand() >= d) + continue; + + std::string dest = st(i); + + random_labels(res, src, dest, props, t, accs, a); + + node_set::iterator j = unreachable_nodes.find(dest); + if (j != unreachable_nodes.end()) + { + nodes_to_process.insert(dest); + unreachable_nodes.erase(j); + } + } + + // Avoid dead ends. + if (res->add_state(src)->empty()) + random_labels(res, src, src, props, t, accs, a); + } + return res; + } + +} diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh new file mode 100644 index 000000000..9a711058f --- /dev/null +++ b/src/tgbaalgos/randomgraph.hh @@ -0,0 +1,76 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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. + +#ifndef SPOT_TGBAALGOS_RANDOMGRAPH_HH +# define SPOT_TGBAALGOS_RANDOMGRAPH_HH + +#include "ltlvisit/apcollect.hh" +#include "ltlenv/defaultenv.hh" + +namespace spot +{ + class bdd_dict; + class tgba; + + /// \brief Construct a tgba randomly. + /// + /// \param n The number of states wanted in the automata. All states + /// will be connected, and there will be no dead state. + /// \param d The density of the automata. This is the probability + /// (between 0.0 and 1.0), to add a transition between two + /// states. All states have at least one outgoing transition, + /// so \a d is considered only when adding the remaining transition. + /// A density of 1 means all states will be connected to each other. + /// \param ap The list of atomic property that should label the transition. + /// \param dict The bdd_dict to used for this automata. + /// \param n_acc The number of acceptance sets to use. + /// \param a The probability (between 0.0 and 1.0) that a transition belongs + /// to an acceptance set. + /// \param t The probability (between 0.0 and 1.0) that an atomic proposition + /// is true. + /// \param env The environment in which to declare the acceptance conditions. + /// + /// This algorithms is adapted from the one in Fig 6.2 page 48 of + /// \verbatim + /// @TechReport{ tauriainen.00.a66, + /// author = {Heikki Tauriainen}, + /// title = {Automated Testing of {B\"u}chi Automata Translators for + /// {L}inear {T}emporal {L}ogic}, + /// address = {Espoo, Finland}, + /// institution = {Helsinki University of Technology, Laboratory for + /// Theoretical Computer Science}, + /// number = {A66}, + /// year = {2000}, + /// url = {http://citeseer.nj.nec.com/tauriainen00automated.html}, + /// type = {Research Report}, + /// note = {Reprint of Master's thesis} + /// } + /// \endverbatim + /// The only difference is that labels are on transitions, and that + /// acceptance conditions are handled. Otherwise the logic is the same. + tgba* + random_graph(int n, float d, + const ltl::atomic_prop_set* ap, bdd_dict* dict, + int n_acc = 0, float a = 0.1, float t = 0.5, + ltl::environment* env = <l::default_environment::instance()); +} + +#endif // SPOT_TGBAALGOS_RANDOMGRAPH_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index b4c90e4db..a43d93491 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -23,9 +23,9 @@ AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = ../libspot.la -# This is the most used test program, and it's also useful -# to run manually outside the test suite. Always build it. -noinst_PROGRAMS = ltl2tgba +# These are the most used test programs, and they are also useful +# to run manually outside the test suite. Always build them. +noinst_PROGRAMS = ltl2tgba randtgba check_SCRIPTS = defs # Keep this sorted alphabetically. @@ -54,6 +54,7 @@ ltl2tgba_SOURCES = ltl2tgba.cc ltlprod_SOURCES = ltlprod.cc mixprod_SOURCES = mixprod.cc powerset_SOURCES = powerset.cc +randtgba_SOURCES = randtgba.cc readsave_SOURCES = readsave.cc reductgba_SOURCES = reductgba.cc reduccmp_SOURCES = reductgba.cc diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc new file mode 100644 index 000000000..b8ef45fd1 --- /dev/null +++ b/src/tgbatest/randtgba.cc @@ -0,0 +1,163 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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. + +#include +#include +#include "ltlvisit/apcollect.hh" +#include "ltlvisit/destroy.hh" +#include "tgbaalgos/randomgraph.hh" +#include "tgbaalgos/save.hh" +#include "ltlenv/defaultenv.hh" +#include "ltlast/atomic_prop.hh" +#include "tgbaalgos/dotty.hh" +#include "misc/random.hh" + +void +syntax(char* prog) +{ + std::cerr << "Usage: "<< prog << " [OPTIONS...] PROPS..." << std::endl + << std::endl + << "Options:" << std::endl + << " -a N F number of accepence conditions a propability that" + << " one is true [0 0.0]" << std::endl + << " -d F density of the graph [0.2]" << std::endl + << " -g output in dot format" << std::endl + << " -n N number of nodes of the graph [20]" << std::endl + << " -s N seed for the random number generator" << std::endl + << " -t F probability of the atomic propositions to be true" + << " [0.5]" + << std::endl + << "Where:" << std::endl + << " F are floats between 0.0 and 1.0 inclusive" << std::endl + << " N are positive integers" << std::endl + << " PROPS are the atomic properties to use on transitions" + << std::endl; + exit(2); +} + +int +to_int(const char* s) +{ + char* endptr; + int res = strtol(s, &endptr, 10); + if (*endptr) + { + std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl; + exit(1); + } + return res; +} + +float +to_float(const char* s) +{ + char* endptr; + float res = strtof(s, &endptr); + if (*endptr) + { + std::cerr << "Failed to parse `" << s << "' as a float." << std::endl; + exit(1); + } + return res; +} + +int +main(int argc, char** argv) +{ + int opt_n_acc = 0; + float opt_a = 0.0; + float opt_d = 0.2; + int opt_n = 20; + float opt_t = 0.5; + + bool opt_dot = false; + + int argn = 0; + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set; + + if (argc <= 1) + syntax(argv[0]); + + while (++argn < argc) + { + if (!strcmp(argv[argn], "-a")) + { + if (argc < argn + 3) + syntax(argv[0]); + opt_n_acc = to_int(argv[++argn]); + opt_a = to_float(argv[++argn]); + } + else if (!strcmp(argv[argn], "-d")) + { + if (argc < argn + 1) + syntax(argv[0]); + opt_d = to_float(argv[++argn]); + } + else if (!strcmp(argv[argn], "-g")) + { + opt_dot = true; + } + else if (!strcmp(argv[argn], "-n")) + { + if (argc < argn + 1) + syntax(argv[0]); + opt_n = to_int(argv[++argn]); + } + else if (!strcmp(argv[argn], "-s")) + { + if (argc < argn + 1) + syntax(argv[0]); + spot::srand(to_int(argv[++argn])); + } + else if (!strcmp(argv[argn], "-t")) + { + if (argc < argn + 1) + syntax(argv[0]); + opt_t = to_float(argv[++argn]); + } + else + { + ap->insert(static_cast + (env.require(argv[argn]))); + } + } + + spot::bdd_dict* dict = new spot::bdd_dict(); + + spot::tgba* a = spot::random_graph(opt_n, opt_d, ap, dict, + opt_n_acc, opt_a, opt_t, &env); + + if (opt_dot) + dotty_reachable(std::cout, a); + else + tgba_save_reachable(std::cout, a); + + for (spot::ltl::atomic_prop_set::iterator i = ap->begin(); + i != ap->end(); ++i) + spot::ltl::destroy(*i); + + delete a; + delete dict; + delete ap; + return 0; +} diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 83a9ad8c6..71ebc597b 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -56,4 +56,18 @@ sed 's/"d" "c"/"c" "d"/g;s/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout diff input stdout -rm input stdout expected +rm -f input stdout expected + + +# Likewise, with a randomly generated TGBA. +run 0 ./randtgba -t 1 -n 20 -d 0.2 a b -a 2 0.1 >input +sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' input > tmp_ && + mv tmp_ input +cat input +run 0 ./readsave input > stdout +sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' stdout > tmp_ && + mv tmp_ stdout + +diff input stdout + +rm -f input stdout