From 42b05c7a05b9a318afdaac2745676daf163a2f5b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 3 Nov 2004 11:59:58 +0000 Subject: [PATCH] * tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc (tgba_reachable_iterator::process_link): Take the state* as arguments in addition to the state numbers. * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc (tgba_explicit::copy_acceptance_conditions_of): New method. * tgbaalgos/dupexp.cc (dupexp_iter::dupexp_iter): Call copy_acceptance_conditions_of. (dupexp_iter::process_state, duplex_iter::declare_state, dupexp_iter::name_): Remove. (dupexp_iter::process_link): Adjust prototype, and format the state here rather than in process_state. * tgbaalgos/stats.cc, tgbaalgos/dotty.cc: Adjust prototype of process_link. --- ChangeLog | 16 +++++++++++++ src/tgba/tgbaexplicit.cc | 10 ++++++++ src/tgba/tgbaexplicit.hh | 9 ++++++- src/tgbaalgos/dotty.cc | 3 ++- src/tgbaalgos/dupexp.cc | 48 +++++++------------------------------- src/tgbaalgos/reachiter.cc | 8 ++++--- src/tgbaalgos/reachiter.hh | 12 ++++++++-- src/tgbaalgos/stats.cc | 3 ++- 8 files changed, 62 insertions(+), 47 deletions(-) diff --git a/ChangeLog b/ChangeLog index cb89d2c43..fca954c03 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,19 @@ +2004-11-03 Alexandre Duret-Lutz + + * tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc + (tgba_reachable_iterator::process_link): Take the state* as arguments + in addition to the state numbers. + * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc + (tgba_explicit::copy_acceptance_conditions_of): New method. + * tgbaalgos/dupexp.cc (dupexp_iter::dupexp_iter): Call + copy_acceptance_conditions_of. + (dupexp_iter::process_state, duplex_iter::declare_state, + dupexp_iter::name_): Remove. + (dupexp_iter::process_link): Adjust prototype, and format + the state here rather than in process_state. + * tgbaalgos/stats.cc, tgbaalgos/dotty.cc: Adjust prototype + of process_link. + 2004-11-02 Alexandre Duret-Lutz * src/ltlvisit/reduce.hh (is_eventual, is_universal): More doc. diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 91ceda214..5fe0b5f93 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -208,6 +208,16 @@ namespace spot all_acceptance_conditions_computed_ = false; } + void + tgba_explicit::copy_acceptance_conditions_of(const tgba *a) + { + assert(neg_acceptance_conditions_ == bddtrue); + assert(all_acceptance_conditions_computed_ == false); + bdd f = a->neg_acceptance_conditions(); + dict_->register_acceptance_variables(f, this); + neg_acceptance_conditions_ = f; + } + void tgba_explicit::complement_all_acceptance_conditions() { diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index d6a513b5d..58bf1f53c 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -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. // @@ -59,6 +59,13 @@ namespace spot /// This assumes that all variables in \a f are known from dict. void add_conditions(transition* t, bdd f); void declare_acceptance_condition(const ltl::formula* f); + + /// \brief Copy the acceptance conditions of a tgba. + /// + /// If used, this function should be called before creating any + /// transition. + void copy_acceptance_conditions_of(const tgba *a); + bool has_acceptance_condition(const ltl::formula* f) const; void add_acceptance_condition(transition* t, const ltl::formula* f); /// This assumes that all acceptance conditions in \a f are known from dict. diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index cb4bf0e0f..0f0c50f96 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -60,7 +60,8 @@ namespace spot } void - process_link(int in, int out, const tgba_succ_iterator* si) + process_link(const state*, int in, + const state*, int out, const tgba_succ_iterator* si) { os_ << " " << in << " -> " << out << " [label=\""; escape_str(os_, bdd_format_formula(automata_->get_dict(), diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc index e81e72300..850198c90 100644 --- a/src/tgbaalgos/dupexp.cc +++ b/src/tgbaalgos/dupexp.cc @@ -36,6 +36,7 @@ namespace spot dupexp_iter(const tgba* a) : T(a), out_(new tgba_explicit(a->get_dict())) { + out_->copy_acceptance_conditions_of(a); } tgba_explicit* @@ -45,54 +46,23 @@ namespace spot } void - process_state(const state* s, int n, tgba_succ_iterator*) + process_link(const state* in_s, int in, + const state* out_s, int out, + const tgba_succ_iterator* si) { - std::ostringstream os; - os << "(#" << n << ") " << this->automata_->format_state(s); - name_[n] = os.str(); - } - - std::string - declare_state(const state* s, int n) - { - std::string str; - name_map_::const_iterator i = name_.find(n); - if (i == name_.end()) - { - std::ostringstream os; - os << "(#" << n << ") " << this->automata_->format_state(s); - name_[n] = str = os.str(); - } - else - { - str = i->second; - } - delete s; - return str; - } - - void - process_link(int in, int out, const tgba_succ_iterator* si) - { - // We might need to format out before process_state is called. - name_map_::const_iterator i = name_.find(out); - if (i == name_.end()) - { - const state* s = si->current_state(); - process_state(s, out, 0); - delete s; - } + std::ostringstream in_name; + in_name << "(#" << in << ") " << this->automata_->format_state(in_s); + std::ostringstream out_name; + out_name << "(#" << out << ") " << this->automata_->format_state(out_s); tgba_explicit::transition* t = - out_->create_transition(name_[in], name_[out]); + out_->create_transition(in_name.str(), out_name.str()); out_->add_conditions(t, si->current_condition()); out_->add_acceptance_conditions(t, si->current_acceptance_conditions()); } private: tgba_explicit* out_; - typedef std::map name_map_; - std::map name_; }; } // anonymous diff --git a/src/tgbaalgos/reachiter.cc b/src/tgbaalgos/reachiter.cc index 312665bed..d45776d5a 100644 --- a/src/tgbaalgos/reachiter.cc +++ b/src/tgbaalgos/reachiter.cc @@ -67,11 +67,11 @@ namespace spot { seen[current] = ++n; add_state(current); - process_link(tn, n, si); + process_link(t, tn, current, n, si); } else { - process_link(tn, s->second, si); + process_link(t, tn, s->first, s->second, si); delete current; } } @@ -97,7 +97,9 @@ namespace spot } void - tgba_reachable_iterator::process_link(int, int, const tgba_succ_iterator*) + tgba_reachable_iterator::process_link(const state*, int, + const state*, int, + const tgba_succ_iterator*) { } diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh index e7ed0b76d..cb94879ae 100644 --- a/src/tgbaalgos/reachiter.hh +++ b/src/tgbaalgos/reachiter.hh @@ -63,16 +63,24 @@ namespace spot /// Called by run() to process a state. /// /// \param s The current state. - /// \param n An unique number assigned to \a s. + /// \param n A unique number assigned to \a s. /// \param si The spot::tgba_succ_iterator for \a s. virtual void process_state(const state* s, int n, tgba_succ_iterator* si); /// Called by run() to process a transition. /// + /// \param in_s The source state /// \param in The source state number. + /// \param out_s The destination state /// \param out The destination state number. /// \param si The spot::tgba_succ_iterator positionned on the current /// transition. - virtual void process_link(int in, int out, const tgba_succ_iterator* si); + /// + /// The in_s and out_s states are owned by the + /// spot::tgba_reachable_iterator instance and destroyed when the + /// instance is destroyed. + virtual void process_link(const state* in_s, int in, + const state* out_s, int out, + const tgba_succ_iterator* si); protected: const tgba* automata_; ///< The spot::tgba to explore. diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index 353b86108..b8883ea3e 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -42,7 +42,8 @@ namespace spot } void - process_link(int, int, const tgba_succ_iterator*) + process_link(const state*, int, const state*, int, + const tgba_succ_iterator*) { ++s_.transitions; }