diff --git a/ChangeLog b/ChangeLog index e7b57da20..6fa5a9e2e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2009-05-28 Alexandre Duret-Lutz + + Implement spot::future_conditions_collector. + + * src/tgba/futurecondcol.hh, src/tgba/futurecondcol.cc: + New files. + * src/tgba/Makefile.am: Adjust. + * src/tgbatest/ltl2tgba.cc: Add option -FC. + 2009-05-28 Alexandre Duret-Lutz * src/tgbaalgos/scc.cc (dump_scc_dot): Use a bit vector instead of diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 16fdc44ca..9f664c58b 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -28,6 +28,7 @@ tgba_HEADERS = \ bdddict.hh \ bddprint.hh \ formula2bdd.hh \ + futurecondcol.hh \ public.hh \ state.hh \ statebdd.hh \ @@ -49,6 +50,7 @@ libtgba_la_SOURCES = \ bdddict.cc \ bddprint.cc \ formula2bdd.cc \ + futurecondcol.cc \ statebdd.cc \ succiterconcrete.cc \ tgba.cc \ diff --git a/src/tgba/futurecondcol.cc b/src/tgba/futurecondcol.cc new file mode 100644 index 000000000..563fadb9a --- /dev/null +++ b/src/tgba/futurecondcol.cc @@ -0,0 +1,150 @@ +// Copyright (C) 2009 Laboratoire de recherche et développement 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. + +#include +#include "futurecondcol.hh" +#include "bddprint.hh" + +namespace spot +{ + + void + future_conditions_collector::map_builder_(unsigned src) + { + // The future conditions of a SCC are the conditions of the SCC + // augmented with the future conditions of any descendent SCC. + cond_set res(scc_map_.cond_set_of(src)); + const scc_map::succ_type& next = scc_map_.succ(src); + for (scc_map::succ_type::const_iterator i = next.begin(); + i != next.end(); ++i) + { + unsigned dest = i->first; + map_builder_(dest); + res.insert(i->second); + res.insert(future_conds_[dest].begin(), future_conds_[dest].end()); + } + future_conds_[src] = res; + } + + future_conditions_collector::future_conditions_collector(const tgba* aut, + bool show) + : aut_(aut), scc_map_(aut), show_(show) + { + scc_map_.build_map(); + // Initialize future_conds_ with as much empty "cond_set"s as + // there are SCCs. + future_conds_ = fc_map(scc_map_.scc_count()); + // Fill future_conds by recursively visiting the (acyclic) graph + // of SCCs. + map_builder_(scc_map_.initial()); + } + + future_conditions_collector::~future_conditions_collector() + { + } + + const future_conditions_collector::cond_set& + future_conditions_collector::future_conditions(const spot::state* st) const + { + // The future conditions of a state are the future conditions of + // the SCC the state belongs to. + unsigned s = scc_map_.scc_of_state(st); + return future_conds_[s]; + } + + state* + future_conditions_collector::get_init_state() const + { + return aut_->get_init_state(); + } + + tgba_succ_iterator* + future_conditions_collector::succ_iter(const state* local_state, + const state* global_state, + const tgba* global_automaton) const + { + return aut_->succ_iter(local_state, global_state, global_automaton); + } + + bdd_dict* + future_conditions_collector::get_dict() const + { + return aut_->get_dict(); + } + + std::string + future_conditions_collector::format_state(const state* state) const + { + if (!show_) + return aut_->format_state(state); + + std::ostringstream str; + str << aut_->format_state(state); + str << "\\n["; + const cond_set& c = future_conditions(state); + for (cond_set::const_iterator i = c.begin(); i != c.end(); ++i) + { + if (i != c.begin()) + str << ", "; + bdd_print_formula(str, get_dict(), *i); + } + str << "]"; + return str.str(); + } + + std::string + future_conditions_collector::transition_annotation + (const tgba_succ_iterator* t) const + { + return aut_->transition_annotation(t); + } + + state* + future_conditions_collector::project_state(const state* s, + const tgba* t) const + { + return aut_->project_state(s, t); + } + + bdd + future_conditions_collector::all_acceptance_conditions() const + { + return aut_->all_acceptance_conditions(); + } + + bdd + future_conditions_collector::neg_acceptance_conditions() const + { + return aut_->neg_acceptance_conditions(); + } + + bdd + future_conditions_collector::compute_support_conditions + (const state* state) const + { + return aut_->support_conditions(state); + } + + bdd + future_conditions_collector::compute_support_variables + (const state* state) const + { + return aut_->support_variables(state); + } +} diff --git a/src/tgba/futurecondcol.hh b/src/tgba/futurecondcol.hh new file mode 100644 index 000000000..b0aeab524 --- /dev/null +++ b/src/tgba/futurecondcol.hh @@ -0,0 +1,93 @@ +// Copyright (C) 2009 Laboratoire de recherche et développement 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. + +#ifndef SPOT_TGBA_FUTURECONDCOL_HH +# define SPOT_TGBA_FUTURECONDCOL_HH + +#include "tgbaexplicit.hh" +#include "tgbaalgos/scc.hh" + +namespace spot +{ + + /// \brief Wrap a tgba to offer information about upcoming conditions. + /// \ingroup tgba + /// + /// This class is a spot::tgba wrapper that simply add a new method, + /// future_conditions(), to any spot::tgba. + /// + /// This new methods returns a set of conditions that can be + /// seen on a transitions accessible (maybe indirectly) from + /// the given state. + class future_conditions_collector : public tgba + { + public: + typedef scc_map::cond_set cond_set; + typedef std::vector fc_map; + + /// \brief Create a future_conditions_collector wrapper for \a aut. + /// + /// If \a show is set to true, then the format_state() method will + /// include the set of conditions computed for the given state in + /// its output string. + future_conditions_collector(const tgba* aut, bool show = false); + virtual ~future_conditions_collector(); + + const cond_set& future_conditions(const spot::state* s) const; + + /// \brief Format a state for output. + /// + /// If the constructor was called with \a show set to true, then + /// this method will include the set of conditions computed for \a + /// state by future_conditions() in the output string. + virtual std::string format_state(const state* state) const; + + // The following methods simply delegate their work to the wrapped + // tgba. + + virtual state* get_init_state() const; + virtual tgba_succ_iterator* + succ_iter(const state* local_state, + const state* global_state = 0, + const tgba* global_automaton = 0) const; + virtual bdd_dict* get_dict() const; + + virtual std::string + transition_annotation(const tgba_succ_iterator* t) const; + virtual state* project_state(const state* s, const tgba* t) const; + virtual bdd all_acceptance_conditions() const; + virtual bdd neg_acceptance_conditions() const; + + virtual bdd compute_support_conditions(const state* state) const; + virtual bdd compute_support_variables(const state* state) const; + + private: + void map_builder_(unsigned s); + + const tgba* aut_; // The wrapped TGBA. + fc_map future_conds_; // The map of future conditions for each + // strongly connected component. + scc_map scc_map_; // SCC informations. + bool show_; // Wether to show future conditions + // in the output of format_state(). + }; + +} + +#endif // SPOT_TGBA_FUTURECONDCOL_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 445fa40b4..7e2185c6e 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -39,6 +39,7 @@ #include "tgbaalgos/lbtt.hh" #include "tgba/tgbatba.hh" #include "tgba/tgbaproduct.hh" +#include "tgba/futurecondcol.hh" #include "tgbaalgos/reducerun.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/dupexp.hh" @@ -87,6 +88,8 @@ syntax(char* prog) << " -fr7 use -r7 (see below) at each step of FM" << std::endl << " -fr8 use -r8 (see below) at each step of FM" << std::endl << " -F read the formula from the file" << std::endl + << " -FC dump the automaton showing future conditions on states" + << std::endl << " -g graph the accepting run on the automaton (requires -e)" << std::endl << " -G graph the accepting run seen as an automaton " @@ -189,6 +192,7 @@ main(int argc, char** argv) bool graph_run_tgba_opt = false; bool opt_reduce = false; bool containment = false; + bool show_fc = false; spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* unobservables = 0; spot::tgba_explicit* system = 0; @@ -317,6 +321,10 @@ main(int argc, char** argv) { file_opt = true; } + else if (!strcmp(argv[formula_index], "-FC")) + { + show_fc = true; + } else if (!strcmp(argv[formula_index], "-g")) { graph_run_opt = true; @@ -695,6 +703,11 @@ main(int argc, char** argv) } } + if (show_fc) + { + a = new spot::future_conditions_collector(a, true); + } + switch (output) { case -1: @@ -864,6 +877,8 @@ main(int argc, char** argv) delete ec; } + if (show_fc) + delete a; if (f) spot::ltl::destroy(f); delete product_degeneralized;