diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 1f5bb6edd..4715f0bf8 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2013 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. @@ -21,15 +21,23 @@ #include #include +#include +#include #include "powerset.hh" #include "misc/hash.hh" #include "tgbaalgos/powerset.hh" #include "bdd.h" +#include "tgbaalgos/scc.hh" +#include "tgbaalgos/cycles.hh" +#include "tgbaalgos/gtec/gtec.hh" +#include "tgba/tgbaproduct.hh" +#include "tgba/bddprint.hh" +#include "tgbaalgos/dotty.hh" namespace spot { tgba_explicit_number* - tgba_powerset(const tgba* aut, power_map& pm) + tgba_powerset(const tgba* aut, power_map& pm, bool merge) { typedef power_map::power_state power_state; typedef std::map power_set; @@ -104,7 +112,8 @@ namespace spot res->add_conditions(t, cond); } } - res->merge_transitions(); + if (merge) + res->merge_transitions(); return res; } @@ -114,4 +123,190 @@ namespace spot power_map pm; return tgba_powerset(aut, pm); } + + + namespace + { + + class fix_scc_acceptance: protected enumerate_cycles + { + public: + typedef dfs_stack::const_iterator cycle_iter; + typedef state_explicit_number::transition trans; + typedef std::set trans_set; + typedef std::vector set_set; + protected: + const tgba* ref_; + power_map& refmap_; + trans_set reject_; // set of rejecting transitions + set_set accept_; // set of cycles that are accepting + trans_set all_; // all non rejecting transitions + + public: + fix_scc_acceptance(const scc_map& sm, const tgba* ref, power_map& refmap) + : enumerate_cycles(sm), ref_(ref), refmap_(refmap) + { + } + + void fix_scc(const int m) + { + reject_.clear(); + accept_.clear(); + run(m); + +// std::cerr << "SCC #" << m << "\n"; +// std::cerr << "REJECT: "; +// print_set(std::cerr, reject_) << "\n"; +// std::cerr << "ALL: "; +// print_set(std::cerr, all_) << "\n"; +// for (set_set::const_iterator j = accept_.begin(); +// j != accept_.end(); ++j) +// { +// std::cerr << "ACCEPT: "; +// print_set(std::cerr, *j) << "\n"; +// } + + bdd acc = aut_->all_acceptance_conditions(); + for (trans_set::iterator i = all_.begin(); i != all_.end(); ++i) + { + (*i)->acceptance_conditions = acc; + } + } + + bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const + { + tgba_explicit_number* a = + down_cast(const_cast(aut_)); + // Build an automaton representing this loop. + tgba_explicit_number loop_a(aut_->get_dict()); + int loop_size = std::distance(begin, dfs_.end()); + int n; + cycle_iter i; + for (n = 1, i = begin; n <= loop_size; ++n, ++i) + { + trans* t = a->get_transition(i->succ); + loop_a.create_transition(n - 1, n % loop_size)->condition = + t->condition; + if (reject_.find(t) == reject_.end()) + ts.insert(t); + } + assert(i == dfs_.end()); + + const state* loop_a_init = loop_a.get_init_state(); + assert(loop_a.get_label(loop_a_init) == 0); + + // Check if the loop is accepting in the original automaton. + bool accepting = false; + + // Iterate on each original state corresponding to the + // start of the loop in the determinized automaton. + const power_map::power_state& ps = + refmap_.states_of(a->get_label(begin->ts->first)); + for (power_map::power_state::const_iterator it = ps.begin(); + it != ps.end() && !accepting; ++it) + { + // Construct a product between + // LOOP_A, and ORIG_A starting in *IT. + + tgba* p = new tgba_product_init(&loop_a, ref_, + loop_a_init, *it); + + //spot::dotty_reachable(std::cout, p); + + couvreur99_check* ec = down_cast(couvreur99(p)); + assert(ec); + emptiness_check_result* res = ec->check(); + if (res) + accepting = true; + delete res; + delete ec; + delete p; + } + + loop_a_init->destroy(); + return accepting; + } + + std::ostream& + print_set(std::ostream& o, const trans_set& s) const + { + o << "{ "; + for (trans_set::const_iterator i = s.begin(); i != s.end(); ++i) + o << *i << " "; + o << "}"; + return o; + } + + virtual bool + cycle_found(const state* start) + { + cycle_iter i = dfs_.begin(); + while (i->ts->first != start) + ++i; + trans_set ts; + bool is_acc = is_cycle_accepting(i, ts); + do + { + // std::cerr << aut_->format_state(i->ts->first) << " "; + ++i; + } + while (i != dfs_.end()); + // std::cerr << " acc=" << is_acc << " ("; + // bdd_print_accset(std::cerr, aut_->get_dict(), s) << ") "; + // print_set(std::cerr, ts) << "\n"; + if (is_acc) + { + accept_.push_back(ts); + all_.insert(ts.begin(), ts.end()); + } + else + { + for (trans_set::const_iterator i = ts.begin(); i != ts.end(); ++i) + { + trans* t = *i; + reject_.insert(t); + for (set_set::iterator j = accept_.begin(); + j != accept_.end(); ++j) + { + j->erase(t); + } + all_.erase(t); + } + } + + return true; + } + }; + + static void + fix_dba_acceptance(tgba_explicit_number* det, + const tgba* ref, power_map& refmap) + { + det->copy_acceptance_conditions_of(ref); + + scc_map sm(det); + sm.build_map(); + + unsigned scc_count = sm.scc_count(); + + fix_scc_acceptance fsa(sm, ref, refmap); + + for (unsigned m = 0; m < scc_count; ++m) + fsa.fix_scc(m); + } + + } + + tgba_explicit_number* + tba_determinize(const tgba* aut) + { + power_map pm; + // Do not merge transitions in the deterministic automaton. If we + // add two self-loops labeled by "a" and "!a", we do not want + // these to be merged as "1" before the acceptance has been fixed. + tgba_explicit_number* det = tgba_powerset(aut, pm, false); + fix_dba_acceptance(det, aut, pm); + det->merge_transitions(); + return det; + } } diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index 354d23409..512558c79 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -86,12 +86,44 @@ namespace spot /// /// If \a pm is supplied it will be filled with the set of original states /// associated to each state of the deterministic automaton. + /// The \a merge argument can be set to false to prevent merging of + /// transitions. //@{ SPOT_API tgba_explicit_number* - tgba_powerset(const tgba* aut, power_map& pm); + tgba_powerset(const tgba* aut, power_map& pm, bool merge = true); SPOT_API tgba_explicit_number* tgba_powerset(const tgba* aut); //@} + + + /// \brief Determinize a TBA using the powerset construction. + /// + /// The input automaton should have at most one acceptance + /// condition. Beware that not all Büchi automata can be + /// determinized, and this procedure does not ensure that the + /// produced automaton is equivalent to \a aut. + /// + /// The construction is adapted from Section 3.2 of: + /// \verbatim + /// @InProceedings{ dax.07.atva, + /// author = {Christian Dax and Jochen Eisinger and Felix Klaedtke}, + /// title = {Mechanizing the Powerset Construction for Restricted + /// Classes of {$\omega$}-Automata}, + /// year = 2007, + /// series = {Lecture Notes in Computer Science}, + /// publisher = {Springer-Verlag}, + /// volume = 4762, + /// booktitle = {Proceedings of the 5th International Symposium on + /// Automated Technology for Verification and Analysis + /// (ATVA'07)}, + /// editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino + /// and Yoshio Okamura}, + /// month = oct + /// } + /// \endverbatim + /// only adapted to work on TBA rather than BA. + SPOT_API tgba_explicit_number* + tba_determinize(const tgba* aut); } #endif // SPOT_TGBAALGOS_POWERSET_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index bb10ffa1a..46f903811 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -69,6 +69,7 @@ #include "kripkeparse/public.hh" #include "tgbaalgos/simulation.hh" #include "tgbaalgos/compsusp.hh" +#include "tgbaalgos/powerset.hh" #include "taalgos/tgba2ta.hh" #include "taalgos/dotty.hh" @@ -234,6 +235,7 @@ syntax(char* prog) << std::endl << " -RM attempt to WDBA-minimize the automaton unless the " << "result is bigger" << std::endl + << " -RQ determinize a TGBA (assuming it's legal!)" << std::endl << std::endl << "Automaton conversion:" << std::endl @@ -385,6 +387,7 @@ main(int argc, char** argv) bool graph_run_tgba_opt = false; bool opt_reduce = false; bool opt_minimize = false; + bool opt_determinize = false; bool reject_bigger = false; bool opt_bisim_ta = false; bool opt_monitor = false; @@ -784,6 +787,10 @@ main(int argc, char** argv) opt_minimize = true; reject_bigger = true; } + else if (!strcmp(argv[formula_index], "-RQ")) + { + opt_determinize = true; + } else if (!strcmp(argv[formula_index], "-RT")) { opt_bisim_ta = true; @@ -1425,6 +1432,15 @@ main(int argc, char** argv) // pointless. } + spot::tgba* determinized = 0; + if (opt_determinize && a->number_of_acceptance_conditions() <= 1 + && f->is_syntactic_recurrence()) + { + tm.start("determinization"); + a = determinized = tba_determinize(a); + tm.stop("determinization"); + } + const spot::tgba* expl = 0; switch (dupexp) { @@ -1878,6 +1894,7 @@ main(int argc, char** argv) delete expl; delete monitor; delete minimized; + delete determinized; delete degeneralized; delete aut_scc; delete to_free;