From a010ebc80545a4fb793f86d3bae459269bbb2605 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Sep 2012 15:10:12 +0200 Subject: [PATCH] Use more sba_explicit more often. * src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh (minimize_dfa, minimize_wdba): Return a sba_explicit_number automaton instead of tgba_explicit_number. * src/tgba/tgbaexplicit.hh (declare_acceptance_condition): Fix code so it works on sba as well. * src/tgbaalgos/dotty.cc, src/tgbaalgos/neverclaim.cc: Specialize for sba instead of tgba_sba_proxy. * src/tgbaalgos/neverclaim.hh: Point to degeneralize(). --- src/tgba/tgbaexplicit.hh | 2 +- src/tgbaalgos/dotty.cc | 5 +++-- src/tgbaalgos/minimize.cc | 20 ++++++++++---------- src/tgbaalgos/minimize.hh | 4 ++-- src/tgbaalgos/neverclaim.cc | 14 +++++++------- src/tgbaalgos/neverclaim.hh | 7 ++++--- 6 files changed, 27 insertions(+), 25 deletions(-) diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 8b44a0496..f4440ff42 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -598,7 +598,7 @@ namespace spot neg_acceptance_conditions_ &= neg; // Append neg to all acceptance conditions. - typename explicit_graph::ls_map::iterator i; + typename ls_map::iterator i; for (i = this->ls_.begin(); i != this->ls_.end(); ++i) { typename transitions_t::iterator i2; diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index f125dcb72..4b849b453 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -23,6 +23,7 @@ #include #include "tgba/tgba.hh" +#include "tgba/sba.hh" #include "dotty.hh" #include "dottydec.hh" #include "tgba/bddprint.hh" @@ -42,7 +43,7 @@ namespace spot dotty_decorator* dd) : tgba_reachable_iterator_breadth_first(a), os_(os), mark_accepting_states_(mark_accepting_states), dd_(dd), - sba_(dynamic_cast(a)) + sba_(dynamic_cast(a)) { } @@ -120,7 +121,7 @@ namespace spot std::ostream& os_; bool mark_accepting_states_; dotty_decorator* dd_; - const tgba_sba_proxy* sba_; + const sba* sba_; }; } diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 26bf0de13..f914b148b 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -114,7 +114,7 @@ namespace spot // From the base automaton and the list of sets, build the minimal // resulting automaton - tgba_explicit_number* build_result(const tgba* a, + sba_explicit_number* build_result(const tgba* a, std::list& sets, hash_set* final) { @@ -133,7 +133,7 @@ namespace spot ++num; } typedef state_explicit_number::transition trs; - tgba_explicit_number* res = new tgba_explicit_number(a->get_dict()); + sba_explicit_number* res = new sba_explicit_number(a->get_dict()); // For each transition in the initial automaton, add the corresponding // transition in res. if (!final->empty()) @@ -294,8 +294,8 @@ namespace spot } - tgba_explicit_number* minimize_dfa(const tgba_explicit_number* det_a, - hash_set* final, hash_set* non_final) + sba_explicit_number* minimize_dfa(const tgba_explicit_number* det_a, + hash_set* final, hash_set* non_final) { typedef std::list partition_t; partition_t cur_run; @@ -484,7 +484,7 @@ namespace spot #endif // Build the result. - tgba_explicit_number* res = build_result(det_a, done, final_copy); + sba_explicit_number* res = build_result(det_a, done, final_copy); // Free all the allocated memory. delete final_copy; @@ -503,7 +503,7 @@ namespace spot } - tgba_explicit_number* minimize_monitor(const tgba* a) + sba_explicit_number* minimize_monitor(const tgba* a) { hash_set* final = new hash_set; hash_set* non_final = new hash_set; @@ -521,7 +521,7 @@ namespace spot return minimize_dfa(det_a, final, non_final); } - tgba_explicit_number* minimize_wdba(const tgba* a) + sba_explicit_number* minimize_wdba(const tgba* a) { hash_set* final = new hash_set; hash_set* non_final = new hash_set; @@ -596,7 +596,7 @@ namespace spot if (wdba_scc_is_accepting(det_a, m, a, sm, pm)) { is_useless = false; - d[m] = (l | 1) - 1; // largest even number inferior or equal + d[m] = l & ~1; // largest even number inferior or equal } else { @@ -608,7 +608,7 @@ namespace spot if (!is_useless) { - hash_set* dest_set = (d[m]&1) ? non_final : final; + hash_set* dest_set = (d[m] & 1) ? non_final : final; const std::list& l = sm.states_of(m); std::list::const_iterator il; for (il = l.begin(); il != l.end(); ++il) @@ -625,7 +625,7 @@ namespace spot const ltl::formula* f, const tgba* aut_neg_f, bool reject_bigger) { - tgba_explicit_number* min_aut_f = minimize_wdba(aut_f); + sba_explicit_number* min_aut_f = minimize_wdba(aut_f); if (reject_bigger) { diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh index a237782c0..b7cd3fe31 100644 --- a/src/tgbaalgos/minimize.hh +++ b/src/tgbaalgos/minimize.hh @@ -59,7 +59,7 @@ namespace spot /// \param a the automaton to convert into a minimal deterministic monitor /// \pre Dead SCCs should have been removed from \a a before /// calling this function. - tgba_explicit_number* minimize_monitor(const tgba* a); + sba_explicit_number* minimize_monitor(const tgba* a); /// \brief Minimize a Büchi automaton in the WDBA class. /// @@ -95,7 +95,7 @@ namespace spot /// month = oct /// } /// \endverbatim - tgba_explicit_number* minimize_wdba(const tgba* a); + sba_explicit_number* minimize_wdba(const tgba* a); /// \brief Minimize an automaton if it represents an obligation property. /// diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index bcfdd11bc..070347496 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -24,7 +24,7 @@ #include #include #include "bdd.h" -#include "tgba/tgbatba.hh" +#include "tgba/sba.hh" #include "neverclaim.hh" #include "tgba/bddprint.hh" #include "reachiter.hh" @@ -43,7 +43,7 @@ namespace spot : tgba_reachable_iterator_breadth_first(a), os_(os), f_(f), accept_all_(-1), fi_needed_(false), comments_(comments), all_acc_conds_(a->all_acceptance_conditions()), - degen_(dynamic_cast(a)) + sba_(dynamic_cast(a)) { } @@ -75,10 +75,10 @@ namespace spot bool state_is_accepting(const state *s) { - // If the automaton is degeneralized on-the-fly, - // it's easier to just query the state_is_accepting() method. - if (degen_) - return degen_->state_is_accepting(s); + // If the automaton is a SBA, it's easier to just query the + // state_is_accepting() method. + if (sba_) + return sba_->state_is_accepting(s); // Otherwise, since we are dealing with a degeneralized // automaton nonetheless, the transitions leaving an accepting @@ -197,7 +197,7 @@ namespace spot state* init_; bool comments_; bdd all_acc_conds_; - const tgba_sba_proxy* degen_; + const sba* sba_; }; } // anonymous diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh index f082a4821..1c55e2898 100644 --- a/src/tgbaalgos/neverclaim.hh +++ b/src/tgbaalgos/neverclaim.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -37,7 +37,8 @@ namespace spot /// \param g The (state-based degeneralized) automaton to output. /// There should be only one acceptance condition, and /// all the transitions of a state should be either all accepting - /// or all unaccepting. + /// or all unaccepting. If your automaton does not satisfies + /// these requirements, call degeneralize() first. /// \param f The (optional) formula associated to the automaton. If given /// it will be output as a comment. /// \param comments Whether to comment each state of the never clause