diff --git a/ChangeLog b/ChangeLog index bc474da0f..58b00292d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2009-10-01 Guillaume Sadegh + + The sgba proxy adds an acceptance condition to every states when + the original automaton has no acceptance condition. + + * src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh: New option: + when the original automaton has no accepting condition, it + explicitly considers that every state is accepting. + 2009-09-30 Guillaume Sadegh * src/tgba/tgbacomplement.cc: Move functions related to diff --git a/src/tgba/tgbasgba.cc b/src/tgba/tgbasgba.cc index 1e96f9357..6379c0d75 100644 --- a/src/tgba/tgbasgba.cc +++ b/src/tgba/tgbasgba.cc @@ -93,17 +93,22 @@ namespace spot 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) + : it_(it), emulate_acc_cond_(false) { } + tgba_sgba_proxy_succ_iterator(tgba_succ_iterator* it, bdd acc) + : it_(it), emulate_acc_cond_(true) + { + acceptance_condition_ = acc; + } + virtual ~tgba_sgba_proxy_succ_iterator() { @@ -136,7 +141,7 @@ namespace spot current_state() const { return new state_sgba_proxy(it_->current_state(), - it_->current_acceptance_conditions()); + it_->current_acceptance_conditions()); } bdd @@ -148,19 +153,32 @@ namespace spot bdd current_acceptance_conditions() const { + if (emulate_acc_cond_) + return acceptance_condition_; return it_->current_acceptance_conditions(); } protected: tgba_succ_iterator* it_; - friend class ::spot::tgba_sgba_proxy; + // If the automaton has no acceptance condition, + // every state is accepting. + bool emulate_acc_cond_; + bdd acceptance_condition_; }; } // anonymous - tgba_sgba_proxy::tgba_sgba_proxy(const tgba* a) - : a_(a) + tgba_sgba_proxy::tgba_sgba_proxy(const tgba* a, bool no_zero_acc) + : a_(a), emulate_acc_cond_(false) { + if (no_zero_acc && a_->number_of_acceptance_conditions() == 0) + { + emulate_acc_cond_ = true; + int v = get_dict() + ->register_acceptance_variable(ltl::constant::true_instance(), this); + acceptance_condition_ = bdd_ithvar(v); + } + get_dict()->register_all_variables_of(a, this); } @@ -201,7 +219,11 @@ namespace spot { const state_sgba_proxy* s = dynamic_cast(state); assert(s); - std::string a = bdd_format_accset(get_dict(), s->acceptance_cond()); + std::string a; + if (!emulate_acc_cond_) + a = bdd_format_accset(get_dict(), s->acceptance_cond()); + else + a = bdd_format_accset(get_dict(), acceptance_condition_); if (a != "") a = " " + a; return a_->format_state(s->real_state()) + a; @@ -210,12 +232,16 @@ namespace spot bdd tgba_sgba_proxy::all_acceptance_conditions() const { + if (emulate_acc_cond_) + return acceptance_condition_; return a_->all_acceptance_conditions(); } bdd tgba_sgba_proxy::neg_acceptance_conditions() const { + if (emulate_acc_cond_) + return bdd_nithvar(bdd_var(acceptance_condition_)); return a_->neg_acceptance_conditions(); } @@ -225,6 +251,8 @@ namespace spot const state_sgba_proxy* s = dynamic_cast(state); assert(s); + if (emulate_acc_cond_) + return acceptance_condition_; return s->acceptance_cond(); } @@ -234,6 +262,9 @@ namespace spot const state_sgba_proxy* s = dynamic_cast(state); assert(s); + + if (emulate_acc_cond_) + return acceptance_condition_; return a_->support_conditions(s->real_state()); } @@ -243,6 +274,9 @@ namespace spot const state_sgba_proxy* s = dynamic_cast(state); assert(s); + + if (emulate_acc_cond_) + return bdd_support(acceptance_condition_); return a_->support_variables(s->real_state()); } diff --git a/src/tgba/tgbasgba.hh b/src/tgba/tgbasgba.hh index cfda0539f..814fb430b 100644 --- a/src/tgba/tgbasgba.hh +++ b/src/tgba/tgbasgba.hh @@ -38,7 +38,7 @@ namespace spot class tgba_sgba_proxy : public tgba { public: - tgba_sgba_proxy(const tgba* a); + tgba_sgba_proxy(const tgba* a, bool no_zero_acc = true); virtual ~tgba_sgba_proxy(); @@ -64,6 +64,10 @@ namespace spot private: const tgba* a_; + // If the automaton has no acceptance condition, + // every state is accepting. + bool emulate_acc_cond_; + bdd acceptance_condition_; // Disallow copy. tgba_sgba_proxy(const tgba_sgba_proxy&); tgba_sgba_proxy& operator=(const tgba_sgba_proxy&);