diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index b935d4202..e405ef867 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -38,8 +38,7 @@ tgba_HEADERS = \ tgbaproxy.hh \ tgbaproduct.hh \ tgbasgba.hh \ - tgbasafracomplement.hh \ - wdbacomp.hh + tgbasafracomplement.hh noinst_LTLIBRARIES = libtgba.la libtgba_la_SOURCES = \ @@ -54,5 +53,4 @@ libtgba_la_SOURCES = \ tgbamask.cc \ tgbaproxy.cc \ tgbasafracomplement.cc \ - tgbasgba.cc \ - wdbacomp.cc + tgbasgba.cc diff --git a/src/tgba/wdbacomp.cc b/src/tgba/wdbacomp.cc deleted file mode 100644 index 0f4a6a689..000000000 --- a/src/tgba/wdbacomp.cc +++ /dev/null @@ -1,296 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014 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 3 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 this program. If not, see . - -#include "wdbacomp.hh" -#include "ltlast/constant.hh" - -namespace spot -{ - namespace - { - class state_wdba_comp_proxy : public state - { - public: - state_wdba_comp_proxy(state* s) : s_(s) - { - } - - /// Copy constructor - state_wdba_comp_proxy(const state_wdba_comp_proxy& o) - : state(), - s_(o.real_state()) - { - if (s_) - s_ = s_->clone(); - } - - virtual - ~state_wdba_comp_proxy() - { - if (s_) - s_->destroy(); - } - - state* - real_state() const - { - return s_; - } - - virtual int - compare(const state* other) const - { - const state_wdba_comp_proxy* o = - down_cast(other); - assert(o); - const state* oo = o->real_state(); - if (s_ == 0) - return oo ? 1 : 0; - if (oo == 0) - return -1; - - return s_->compare(oo); - } - - virtual size_t - hash() const - { - if (s_) - return s_->hash(); - return 0; - } - - virtual - state_wdba_comp_proxy* clone() const - { - return new state_wdba_comp_proxy(*this); - } - - private: - state* s_; // 0 if sink-state. - }; - - class tgba_wdba_comp_proxy_succ_iterator: public tgba_succ_iterator - { - public: - tgba_wdba_comp_proxy_succ_iterator(tgba_succ_iterator* it, - bdd the_acceptance_cond) - : it_(it), the_acceptance_cond_(the_acceptance_cond), left_(bddtrue) - { - } - - void recycle(const const_tgba_ptr& a, tgba_succ_iterator* it) - { - a->release_iter(it_); - it_ = it; - } - - virtual - ~tgba_wdba_comp_proxy_succ_iterator() - { - delete it_; - } - - // iteration - - bool - first() - { - left_ = bddtrue; - if (it_) - it_->first(); - // Return true even if it_ is done, because - // we have to build a sink state. - return true; - } - - bool - next() - { - if (!it_ || it_->done()) - { - left_ = bddfalse; - return false; - } - left_ -= it_->current_condition(); - if (left_ == bddfalse) - return false; - it_->next(); - // Return true even if it_ is done, because - // we have to build a sink state. - return true; - } - - bool - done() const - { - return left_ == bddfalse; - } - - // inspection - - state_wdba_comp_proxy* - current_state() const - { - if (!it_ || it_->done()) - return new state_wdba_comp_proxy(0); - return new state_wdba_comp_proxy(it_->current_state()); - } - - bdd - current_condition() const - { - if (!it_ || it_->done()) - return left_; - return it_->current_condition(); - } - - bdd - current_acceptance_conditions() const - { - if (!it_ || it_->done()) - // The sink state is accepting in the negated automaton. - return the_acceptance_cond_; - - if (it_->current_acceptance_conditions() == bddfalse) - return the_acceptance_cond_; - else - return bddfalse; - } - - protected: - tgba_succ_iterator* it_; - const bdd the_acceptance_cond_; - bdd left_; - }; - - class tgba_wdba_comp_proxy: public tgba - { - public: - tgba_wdba_comp_proxy(const const_tgba_ptr& a) - : a_(a), the_acceptance_cond_(a->all_acceptance_conditions()) - { - if (the_acceptance_cond_ == bddfalse) - { - int v = get_dict() - ->register_acceptance_variable(ltl::constant::true_instance(), - this); - the_acceptance_cond_ = bdd_ithvar(v); - } - } - - virtual ~tgba_wdba_comp_proxy() - { - get_dict()->unregister_all_my_variables(this); - } - - virtual state* get_init_state() const - { - return new state_wdba_comp_proxy(a_->get_init_state()); - } - - virtual tgba_succ_iterator* - succ_iter(const state* st) const - { - const state_wdba_comp_proxy* s = - down_cast(st); - assert(s); - - const state* o = s->real_state(); - tgba_succ_iterator* it = nullptr; - if (o) - it = a_->succ_iter(s->real_state()); - if (iter_cache_) - { - tgba_wdba_comp_proxy_succ_iterator* res = - down_cast(iter_cache_); - res->recycle(a_, it); - iter_cache_ = nullptr; - return res; - } - return new tgba_wdba_comp_proxy_succ_iterator(it, the_acceptance_cond_); - } - - virtual bdd_dict_ptr - get_dict() const - { - return a_->get_dict(); - } - - virtual std::string - format_state(const state* ostate) const - { - const state_wdba_comp_proxy* s = - down_cast(ostate); - assert(s); - const state* rs = s->real_state(); - if (rs) - return a_->format_state(s->real_state()); - else - return "(*)"; // sink state - } - - virtual state* - project_state(const state* s, const const_tgba_ptr& t) const - { - const state_wdba_comp_proxy* s2 = - down_cast(s); - assert(s2); - if (t.get() == this) - return s2->clone(); - return a_->project_state(s2->real_state(), t); - } - - virtual bdd - all_acceptance_conditions() const - { - return the_acceptance_cond_; - } - - virtual bdd - neg_acceptance_conditions() const - { - return !the_acceptance_cond_; - } - - protected: - virtual bdd - compute_support_conditions(const state*) const - { - // The automaton is complete, so we always support all variables. - return bddtrue; - } - - const_tgba_ptr a_; - private: - bdd the_acceptance_cond_; - - // Disallow copy. - tgba_wdba_comp_proxy(const tgba_wdba_comp_proxy&) SPOT_DELETED; - tgba_wdba_comp_proxy& operator=(const tgba_wdba_comp_proxy&) SPOT_DELETED; - }; - - } - - const_tgba_ptr - wdba_complement(const const_tgba_ptr& aut) - { - return std::make_shared(aut); - } -} diff --git a/src/tgba/wdbacomp.hh b/src/tgba/wdbacomp.hh deleted file mode 100644 index ba739df9a..000000000 --- a/src/tgba/wdbacomp.hh +++ /dev/null @@ -1,35 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014 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 3 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 this program. If not, see . - -#ifndef SPOT_TGBA_WDBACOMP_HH -# define SPOT_TGBA_WDBACOMP_HH - -#include "tgba.hh" - -namespace spot -{ - /// \ingroup tgba_on_the_fly_algorithms - /// \brief Complement a weak deterministic Büchi automaton - /// \param aut a weak deterministic Büchi automaton to complement - /// \return a new automaton that recognizes the complement language - SPOT_API const_tgba_ptr - wdba_complement(const const_tgba_ptr& aut); -} - -#endif diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc index b96dd7433..a2a795e7e 100644 --- a/src/tgbaalgos/dtgbacomp.cc +++ b/src/tgbaalgos/dtgbacomp.cc @@ -19,10 +19,11 @@ #include "dtgbacomp.hh" #include "dupexp.hh" +#include "sccinfo.hh" namespace spot { - tgba_digraph_ptr dtgba_complement(const const_tgba_ptr& aut) + tgba_digraph_ptr dtgba_complement_nonweak(const const_tgba_ptr& aut) { // Clone the original automaton. tgba_digraph_ptr res = tgba_dupexp_dfs(aut); @@ -50,7 +51,7 @@ namespace spot bdd missingcond = bddtrue; for (auto& t: res->out(src)) { - if (t.dst >= n) // Ignore transition we added. + if (t.dst >= n) // Ignore transitions we added. break; missingcond -= t.cond; bdd curacc = t.acc; @@ -121,4 +122,65 @@ namespace spot // FIXME: Remove unreachable states. return res; } + + tgba_digraph_ptr dtgba_complement_weak(const const_tgba_ptr& aut) + { + // Clone the original automaton. + tgba_digraph_ptr res = tgba_dupexp_dfs(aut); + + res->prop_copy(aut, + true, // state based + true, // single acc + true, // inherently_weak + true); // deterministic + + bdd oldaccs = aut->all_acceptance_conditions(); + bdd oldnegs = aut->neg_acceptance_conditions(); + + scc_info si(res); + + // We will modify res in place, and the resulting + // automaton will only have one acceptance set. + bdd all_acc = res->set_single_acceptance_set(); + res->prop_state_based_acc(); + + unsigned sink = res->num_states(); + + for (unsigned src = 0; src < sink; ++src) + { + bdd acc = bddfalse; + unsigned scc = si.scc_of(src); + if (!si.is_accepting_scc(scc) && !si.is_trivial(scc)) + acc = all_acc; + + // Keep track of all conditions on transition leaving state + // SRC, so we can complete it. + bdd missingcond = bddtrue; + for (auto& t: res->out(src)) + { + missingcond -= t.cond; + t.acc = acc; + } + // Complete the original automaton. + if (missingcond != bddfalse) + { + if (res->num_states() == sink) + { + res->new_state(); + res->new_acc_transition(sink, sink, bddtrue); + } + res->new_transition(src, sink, missingcond); + } + } + //res->merge_transitions(); + return res; + } + + tgba_digraph_ptr dtgba_complement(const const_tgba_ptr& aut) + { + if (aut->is_inherently_weak()) + return dtgba_complement_weak(aut); + else + return dtgba_complement_nonweak(aut); + } } diff --git a/src/tgbaalgos/dtgbacomp.hh b/src/tgbaalgos/dtgbacomp.hh index 0316b9fc2..6cad13e54 100644 --- a/src/tgbaalgos/dtgbacomp.hh +++ b/src/tgbaalgos/dtgbacomp.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -28,8 +28,9 @@ namespace spot /// /// The automaton \a aut should be deterministic. It does no need /// to be complete. Acceptance can be transition-based, or - /// state-based. The resulting automaton is very unlikely to be - /// deterministic. + /// state-based. Unless the input automaton is marked as weak (in + /// which case the output will also be weak and deterministic) the + /// resulting automaton is very unlikely to be deterministic. SPOT_API tgba_digraph_ptr dtgba_complement(const const_tgba_ptr& aut); } diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 1e4034fd9..04ea469af 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -37,7 +37,6 @@ #include "misc/hash.hh" #include "misc/bddlt.hh" #include "tgba/tgbaproduct.hh" -#include "tgba/wdbacomp.hh" #include "tgbaalgos/powerset.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/safety.hh" @@ -671,7 +670,8 @@ namespace spot if (product(min_aut_f, aut_neg_f)->is_empty()) { // Complement the minimized WDBA. - auto neg_min_aut_f = wdba_complement(min_aut_f); + assert(min_aut_f->is_inherently_weak()); + auto neg_min_aut_f = dtgba_complement(min_aut_f); if (product(aut_f, neg_min_aut_f)->is_empty()) // Finally, we are now sure that it was safe // to minimize the automaton.