diff --git a/ChangeLog b/ChangeLog index 1ca20b704..556befc24 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2004-01-05 Alexandre Duret-Lutz + * src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::run) + Reuse s->second to avoid a hash lookup. + * src/tgbaalgos/save.cc (save_bfs::process_state): Delete dest. + * src/ltlparse/Makefile.am ($(FROM_LTLPARSE_YY_MAIN)): Use $(FROM_LTLPARSE_YY_MAIN), not $@, because $@ can contains VPATH and we do not want Bison to see absolute paths. diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 2269beca9..966a11eb2 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -32,6 +32,7 @@ tgbaalgos_HEADERS = \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ magic.hh \ + powerset.hh \ reachiter.hh \ save.hh @@ -44,5 +45,6 @@ libtgbaalgos_la_SOURCES = \ ltl2tgba_fm.cc \ ltl2tgba_lacim.cc \ magic.cc \ + powerset.cc \ reachiter.cc \ save.cc diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc new file mode 100644 index 000000000..b8bff6976 --- /dev/null +++ b/src/tgbaalgos/powerset.cc @@ -0,0 +1,136 @@ +// 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 +#include +#include "misc/hash.hh" +#include "tgbaalgos/powerset.hh" +#include "bdd.h" + +namespace spot +{ + tgba_explicit* + tgba_powerset(const tgba* aut) + { + typedef Sgi::hash_set state_set; + typedef std::set power_state; + typedef std::map power_set; + typedef std::deque todo_list; + + power_set seen; + todo_list todo; + tgba_explicit* res = new tgba_explicit(aut->get_dict()); + + state_set states; + + { + power_state ps; + state* s = aut->get_init_state(); + states.insert(s); + ps.insert(s); + todo.push_back(ps); + seen[ps] = "1"; + } + + unsigned state_num = 1; + + while (! todo.empty()) + { + power_state src = todo.front(); + todo.pop_front(); + // Compute all variables occurring on outgoing arcs. + bdd all_vars = bddtrue; + power_state::const_iterator i; + + for (i = src.begin(); i != src.end(); ++i) + all_vars &= aut->support_variables(*i); + + // Compute all possible combinations of these variables. + bdd all_conds = bddtrue; + while (all_conds != bddfalse) + { + bdd cond = bdd_satoneset(all_conds, all_vars, bddtrue); + all_conds -= cond; + + // Construct the set of all states reachable via COND. + power_state dest; + for (i = src.begin(); i != src.end(); ++i) + { + tgba_succ_iterator *si = aut->succ_iter(*i); + for (si->first(); ! si->done(); si->next()) + if ((cond >> si->current_condition()) == bddtrue) + { + const state* s = si->current_state(); + state_set::const_iterator i = states.find(s); + if (i != states.end()) + { + delete s; + s = *i; + } + else + { + states.insert(s); + } + dest.insert(s); + } + delete si; + } + if (dest.empty()) + continue; + + // Add that transition. + power_set::const_iterator i = seen.find(dest); + std::string dest_name; + if (i != seen.end()) + { + dest_name = i->second; + } + else + { + std::ostringstream str; + str << ++state_num; + dest_name = str.str(); + seen[dest] = dest_name; + todo.push_back(dest); + } + tgba_explicit::transition* t = + res->create_transition(seen[src], dest_name); + res->add_conditions(t, cond); + } + } + res->merge_transitions(); + + // Release all states. + state_set::const_iterator i = states.begin(); + while (i != states.end()) + { + // Advance the iterator before deleting the key. + const state* s = *i; + ++i; + delete s; + } + + return res; + } +} diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh new file mode 100644 index 000000000..57ca22925 --- /dev/null +++ b/src/tgbaalgos/powerset.hh @@ -0,0 +1,37 @@ +// 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_POWERSET_HH +# define SPOT_TGBAALGOS_POWERSET_HH + +# include "tgba/tgbaexplicit.hh" + +namespace spot +{ + /// \brief Build a deterministic automaton, ignoring acceptance conditions. + /// + /// This create a deterministic automaton that recognize the + /// same language as \a aut would if its acceptance conditions + /// were ignored. This is the classical powerset algorithm. + tgba_explicit* tgba_powerset(const tgba* aut); +} + +#endif // SPOT_TGBAALGOS_POWERSET_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index ea36b1900..cdbd21d5b 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -28,10 +28,12 @@ check_SCRIPTS = defs check_PROGRAMS = \ bddprod \ explicit \ + expldot \ explprod \ ltl2tgba \ ltlprod \ mixprod \ + powerset \ readsave \ tgbaread \ tripprod @@ -40,10 +42,13 @@ check_PROGRAMS = \ bddprod_SOURCES = ltlprod.cc bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT explicit_SOURCES = explicit.cc +expldot_SOURCES = powerset.cc +expldot_CXXFLAGS = -DDOTTY explprod_SOURCES = explprod.cc ltl2tgba_SOURCES = ltl2tgba.cc ltlprod_SOURCES = ltlprod.cc mixprod_SOURCES = mixprod.cc +powerset_SOURCES = powerset.cc readsave_SOURCES = readsave.cc tgbaread_SOURCES = tgbaread.cc tripprod_SOURCES = tripprod.cc diff --git a/src/tgbatest/powerset.cc b/src/tgbatest/powerset.cc new file mode 100644 index 000000000..16b237671 --- /dev/null +++ b/src/tgbatest/powerset.cc @@ -0,0 +1,50 @@ +#include +#include +#include "tgba/tgbaexplicit.hh" +#include "tgbaalgos/powerset.hh" +#include "tgbaparse/public.hh" +#include "tgbaalgos/save.hh" +#include "ltlast/allnodes.hh" +#include "tgbaalgos/dotty.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " file" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc != 2) + syntax(argv[0]); + + spot::bdd_dict* dict = new spot::bdd_dict(); + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::tgba_parse_error_list pel; + spot::tgba_explicit* a = spot::tgba_parse(argv[1], pel, dict, env); + if (spot::format_tgba_parse_errors(std::cerr, pel)) + return 2; + + +#ifndef DOTTY + spot::tgba_explicit* e = spot::tgba_powerset(a); + spot::tgba_save_reachable(std::cout, e); + delete e; +#else + spot::dotty_reachable(std::cout, a); +#endif + + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + assert(spot::ltl::atomic_prop::instance_count() != 0); + delete a; + assert(spot::ltl::atomic_prop::instance_count() == 0); + delete dict; + return exit_code; +}