diff --git a/ChangeLog b/ChangeLog index 24e1b0bfe..9560b29c4 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2009-09-24 Guillaume Sadegh + + A wrapper around tgba to produce state-labeled automata. + + * src/tgba/tgbasgba.hh, src/tgba/tgbasgba.hh: Here. + * src/tgbatest/ltl2tgba.cc: New option `-lS' for state-labeled + automata. + * src/tgba/Makefile.am: Adjust and sort files in tgba_HEADERS + and libtgba_la_SOURCES. + 2009-09-21 Guillaume Sadegh Rename files related to Safra complementation. diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 64018a3c8..317d57f8a 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -40,13 +40,14 @@ tgba_HEADERS = \ tgbabddconcreteproduct.hh \ tgbabddcoredata.hh \ tgbabddfactory.hh \ - tgbascc.hh \ - tgbasafracomplement.hh \ tgbaexplicit.hh \ - tgbaproduct.hh \ - tgbatba.hh \ - tgbareduc.hh \ tgbafromfile.hh \ + tgbascc.hh \ + tgbaproduct.hh \ + tgbareduc.hh \ + tgbasgba.hh \ + tgbasafracomplement.hh \ + tgbatba.hh \ tgbaunion.hh noinst_LTLIBRARIES = libtgba.la @@ -55,18 +56,19 @@ libtgba_la_SOURCES = \ bddprint.cc \ formula2bdd.cc \ futurecondcol.cc \ - statebdd.cc \ succiterconcrete.cc \ + statebdd.cc \ tgba.cc \ tgbabddconcrete.cc \ tgbabddconcretefactory.cc \ tgbabddconcreteproduct.cc \ tgbabddcoredata.cc \ - tgbascc.cc \ - tgbasafracomplement.cc \ + tgbafromfile.cc \ tgbaexplicit.cc \ tgbaproduct.cc \ - tgbatba.cc \ tgbareduc.cc \ - tgbafromfile.cc \ + tgbasafracomplement.cc \ + tgbascc.cc \ + tgbasgba.cc \ + tgbatba.cc \ tgbaunion.cc diff --git a/src/tgba/tgbasgba.cc b/src/tgba/tgbasgba.cc new file mode 100644 index 000000000..1e96f9357 --- /dev/null +++ b/src/tgba/tgbasgba.cc @@ -0,0 +1,249 @@ +// Copyright (C) 2009 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 "tgbasgba.hh" +#include "bddprint.hh" +#include "ltlast/constant.hh" +#include "misc/hashfunc.hh" + +namespace spot +{ + namespace + { + /// \brief A state for spot::tgba_sgba_proxy. + class state_sgba_proxy: public state + { + public: + state_sgba_proxy(state* s, bdd acc) + : s_(s), acc_(acc) + { + } + + /// Copy constructor + state_sgba_proxy(const state_sgba_proxy& o) + : state(), + s_(o.real_state()->clone()), + acc_(o.acc_) + { + } + + virtual + ~state_sgba_proxy() + { + delete s_; + } + + state* + real_state() const + { + return s_; + } + + bdd + acceptance_cond() const + { + return acc_; + } + + virtual int + compare(const state* other) const + { + const state_sgba_proxy* o = + dynamic_cast(other); + assert(o); + int res = s_->compare(o->real_state()); + if (res != 0) + return res; + return acc_.id() - o->acc_.id(); + } + + virtual size_t + hash() const + { + return wang32_hash(s_->hash()) ^ wang32_hash(acc_.id()); + } + + virtual + state_sgba_proxy* clone() const + { + return new state_sgba_proxy(*this); + } + + private: + state* s_; + bdd acc_; + }; + + + /// \brief Iterate over the successors of tgba_sgba_proxy computed + /// on the fly. + class tgba_sgba_proxy_succ_iterator: public tgba_succ_iterator + { + public: + tgba_sgba_proxy_succ_iterator(tgba_succ_iterator* it) + : it_(it) + { + } + + virtual + ~tgba_sgba_proxy_succ_iterator() + { + delete it_; + } + + // iteration + + void + first() + { + it_->first(); + } + + void + next() + { + it_->next(); + } + + bool + done() const + { + return it_->done(); + } + + // inspection + + state_sgba_proxy* + current_state() const + { + return new state_sgba_proxy(it_->current_state(), + it_->current_acceptance_conditions()); + } + + bdd + current_condition() const + { + return it_->current_condition(); + } + + bdd + current_acceptance_conditions() const + { + return it_->current_acceptance_conditions(); + } + + protected: + tgba_succ_iterator* it_; + friend class ::spot::tgba_sgba_proxy; + }; + + } // anonymous + + tgba_sgba_proxy::tgba_sgba_proxy(const tgba* a) + : a_(a) + { + get_dict()->register_all_variables_of(a, this); + } + + tgba_sgba_proxy::~tgba_sgba_proxy() + { + get_dict()->unregister_all_my_variables(this); + } + + state* + tgba_sgba_proxy::get_init_state() const + { + return new state_sgba_proxy(a_->get_init_state(), bddfalse); + } + + tgba_succ_iterator* + tgba_sgba_proxy::succ_iter(const state* local_state, + const state* global_state, + const tgba* global_automaton) const + { + const state_sgba_proxy* s = + dynamic_cast(local_state); + assert(s); + + tgba_succ_iterator* it = a_->succ_iter(s->real_state(), + global_state, global_automaton); + + return new tgba_sgba_proxy_succ_iterator(it); + } + + bdd_dict* + tgba_sgba_proxy::get_dict() const + { + return a_->get_dict(); + } + + std::string + tgba_sgba_proxy::format_state(const state* state) const + { + const state_sgba_proxy* s = dynamic_cast(state); + assert(s); + std::string a = bdd_format_accset(get_dict(), s->acceptance_cond()); + if (a != "") + a = " " + a; + return a_->format_state(s->real_state()) + a; + } + + bdd + tgba_sgba_proxy::all_acceptance_conditions() const + { + return a_->all_acceptance_conditions(); + } + + bdd + tgba_sgba_proxy::neg_acceptance_conditions() const + { + return a_->neg_acceptance_conditions(); + } + + bdd + tgba_sgba_proxy::state_acceptance_conditions(const state* state) const + { + const state_sgba_proxy* s = + dynamic_cast(state); + assert(s); + return s->acceptance_cond(); + } + + bdd + tgba_sgba_proxy::compute_support_conditions(const state* state) const + { + const state_sgba_proxy* s = + dynamic_cast(state); + assert(s); + return a_->support_conditions(s->real_state()); + } + + bdd + tgba_sgba_proxy::compute_support_variables(const state* state) const + { + const state_sgba_proxy* s = + dynamic_cast(state); + assert(s); + return a_->support_variables(s->real_state()); + } + +} diff --git a/src/tgba/tgbasgba.hh b/src/tgba/tgbasgba.hh new file mode 100644 index 000000000..cfda0539f --- /dev/null +++ b/src/tgba/tgbasgba.hh @@ -0,0 +1,73 @@ +// Copyright (C) 2009 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_TGBA_TGBASGBA_HH +# define SPOT_TGBA_TGBASGBA_HH + +#include "tgba.hh" +#include "misc/bddlt.hh" + +namespace spot +{ + + /// \brief Change the labeling-mode of spot::tgba on the fly, producing a + /// state-based generalized Büchi automaton. + /// \ingroup tgba_on_the_fly_algorithms + /// + /// This class acts as a proxy in front of a spot::tgba, that should + /// label on states on-the-fly. The result is still a spot::tgba, + /// but acceptances conditions are also on states. + class tgba_sgba_proxy : public tgba + { + public: + tgba_sgba_proxy(const tgba* a); + + virtual ~tgba_sgba_proxy(); + + 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 format_state(const state* state) const; + + virtual bdd all_acceptance_conditions() const; + virtual bdd neg_acceptance_conditions() const; + + /// \brief Retrieve the acceptance condition of a state. + bdd state_acceptance_conditions(const state* state) const; + protected: + virtual bdd compute_support_conditions(const state* state) const; + virtual bdd compute_support_variables(const state* state) const; + + private: + const tgba* a_; + // Disallow copy. + tgba_sgba_proxy(const tgba_sgba_proxy&); + tgba_sgba_proxy& operator=(const tgba_sgba_proxy&); + }; + +} +#endif // SPOT_TGBA_TGBASGBA_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 7e2185c6e..58515ff5e 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -38,6 +38,7 @@ #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" #include "tgba/tgbatba.hh" +#include "tgba/tgbasgba.hh" #include "tgba/tgbaproduct.hh" #include "tgba/futurecondcol.hh" #include "tgbaalgos/reducerun.hh" @@ -100,6 +101,7 @@ syntax(char* prog) << " -KV verbosely dump the graph of SCCs in dot format" << std::endl << " -L fair-loop approximation (implies -f)" << std::endl + << " -lS label acceptance conditions on states" << std::endl << " -m try to reduce accepting runs, in a second pass" << std::endl << " -N display the never clain for Spin " @@ -169,6 +171,7 @@ main(int argc, char** argv) bool debug_opt = false; bool paper_opt = false; enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen; + enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled; bool fm_opt = false; int fm_red = spot::ltl::Reduce_None; bool fm_exprop_opt = false; @@ -350,6 +353,10 @@ main(int argc, char** argv) fair_loop_approx = true; fm_opt = true; } + else if (!strcmp(argv[formula_index], "-lS")) + { + labeling_opt = StateLabeled; + } else if (!strcmp(argv[formula_index], "-m")) { opt_reduce = true; @@ -581,6 +588,7 @@ main(int argc, char** argv) } spot::tgba_tba_proxy* degeneralized = 0; + spot::tgba_sgba_proxy* state_labeled = 0; unsigned int n_acc = a->number_of_acceptance_conditions(); if (echeck_inst @@ -592,6 +600,10 @@ main(int argc, char** argv) a = degeneralized = new spot::tgba_tba_proxy(a); else if (degeneralize_opt == DegenSBA) a = degeneralized = new spot::tgba_sba_proxy(a); + else if (labeling_opt == StateLabeled) + { + a = state_labeled = new spot::tgba_sgba_proxy(a); + } spot::tgba_reduc* aut_red = 0; if (reduc_aut != spot::Reduce_None) @@ -887,6 +899,7 @@ main(int argc, char** argv) delete expl; delete aut_red; delete degeneralized; + delete state_labeled; delete to_free; delete echeck_inst; }