From 450ec22bc3bea7d6a7af80dab91058b7574e947d Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Wed, 6 Mar 2013 15:50:37 +0100 Subject: [PATCH] Heuristics for SCC strength Provides 3 heurisitics to compute the strength of an SCC: inherent, structural and syntactic * src/tgbaalgos/isweakscc.cc: implementation * src/tgbaalgos/isweakscc.hh: definition --- src/tgbaalgos/isweakscc.cc | 108 +++++++++++++++++++++++++++++++++++-- src/tgbaalgos/isweakscc.hh | 45 +++++++++++++++- 2 files changed, 148 insertions(+), 5 deletions(-) diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index acb2f3151..da6d278ac 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -20,6 +20,8 @@ # define SPOT_TGBAALGOS_ISWEAKSCC_CC #include "cycles.hh" +#include "tgba/tgbaexplicit.hh" +#include "ltlast/formula.hh" namespace spot { @@ -62,18 +64,17 @@ namespace spot } }; - } bool - is_weak_scc(scc_map& map, unsigned scc) + is_weak_scc(scc_map& map, unsigned scc, bool easydetect) { // If no cycle is accepting, the SCC is weak. if (!map.accepting(scc)) return true; // If all transitions use all acceptance conditions, the SCC is weak. - if (map.useful_acc_of(scc) == - bdd_support(map.get_aut()->neg_acceptance_conditions())) + if (easydetect && map.useful_acc_of(scc) == + bdd_support(map.get_aut()->neg_acceptance_conditions())) return true; // If the SCC is accepting, but one cycle is not, the SCC is not // weak. @@ -82,7 +83,106 @@ namespace spot return w.result; } + bool + is_syntactic_weak_scc(const spot::tgba *a, scc_map& map, unsigned scc) + { + const std::list states = map.states_of(scc); + std::list::const_iterator it; + for (it = states.begin(); it != states.end(); it++) + { + const state_explicit_formula *s = + dynamic_cast(*it); + const ltl::formula *f = dynamic_cast + (((const tgba_explicit_formula*) a)->get_label(s)); + if ((f->is_syntactic_obligation() || + f->is_syntactic_persistence() || + f->is_syntactic_safety())) + return true; + + } + return false; + } + + bool + is_syntactic_terminal_scc(const spot::tgba *a, scc_map& map, unsigned scc) + { + const std::list states = map.states_of(scc); + std::list::const_iterator it; + for (it = states.begin(); it != states.end(); it++) + { + const state_explicit_formula *s = + dynamic_cast(*it); + const ltl::formula *f = dynamic_cast + (((const tgba_explicit_formula*) a)->get_label(s)); + + if (f->is_syntactic_guarantee()) + return true; + + } + return false; + } + + bool + is_weak_heuristic(scc_map& map, unsigned scc) + { + if (!map.accepting (scc)) + return true; + if (map.useful_acc_of(scc) == + bdd_support(map.get_aut()->neg_acceptance_conditions())) + return true; + return false; + } + + bool + is_complete_scc(const spot::tgba *a, scc_map& map, unsigned scc) + { + const std::list states = map.states_of(scc); + std::list::const_iterator it; + for (it = states.begin(); it != states.end(); it++) + { + const state *s = (*it); + tgba_succ_iterator* it = a->succ_iter(s); + it->first(); + + // No successors cannot be complete + if (it->done()) + { + delete it; + return false; + } + + bdd sumall = bddfalse; + while (!it->done()) + { + const state *next = it->current_state(); + unsigned sccnum = map.scc_of_state(next); + + // check it's the same scc + if (sccnum == scc) + sumall |= it->current_condition(); + next->destroy(); + it->next(); + } + delete it; + + if (sumall != bddtrue) + { + return false; + } + } + return true; + } + + bool + is_terminal_heuristic (const tgba *a, scc_map& map, unsigned scc) + { + // If all transitions use all acceptance conditions, the SCC is weak. + if (map.useful_acc_of(scc) == + bdd_support(map.get_aut()->neg_acceptance_conditions())) + return is_complete_scc(a, map, scc); + return false; + } } #endif // SPOT_TGBAALGOS_ISWEAKSCC_CC diff --git a/src/tgbaalgos/isweakscc.hh b/src/tgbaalgos/isweakscc.hh index 6eb196e83..bc55be008 100644 --- a/src/tgbaalgos/isweakscc.hh +++ b/src/tgbaalgos/isweakscc.hh @@ -38,7 +38,50 @@ namespace spot /// necessarily weak. /// For other accepting SCCs, this function enumerates all cycles in /// the given SCC (it stops if it find a non-accepting cycle). - bool is_weak_scc(scc_map& map, unsigned scc); + bool is_weak_scc(scc_map& map, unsigned scc, bool easydetect = true); + + /// \brief Whether the SCC number \a scc in \a map is complete + /// + /// A SCC is complete iff for all states for all label there exist + /// a transition that stay into this SCC. + bool + is_complete_scc(const tgba *a, scc_map& map, unsigned scc); + + /// \brief Whether the SCC number \a scc in \a map is syntactically weak. + /// + /// An SCC is syntactically weak iff the lowest label of states inside + /// this SCC corresponds to an obligation label + /// + /// Work only on tgba where labels are formula + /// + /// The scc_map \a map should have been built already. The absence + /// of accepting cycle is easy to check (the scc_map can tell + /// whether the SCC is non-accepting already). Similarly, an SCC in + /// which all transitions belong to all acceptance sets is + /// necessarily weak. + /// For other accepting SCCs, this function enumerates all cycles in + /// the given SCC (it stops if it find a non-accepting cycle). + bool is_syntactic_weak_scc(const tgba *a, scc_map& map, unsigned scc); + + /// \brief wether a SCC is syntactically characterized by a gurarantee + /// formula + /// + /// Work only on tgba where labels are formula + bool is_syntactic_terminal_scc(const tgba *a, scc_map& map, unsigned scc); + + /// \brief wether a SCC is terminal using an heuristic + /// + /// The heuristic try to characterize the SCC by loking if the SCC + /// is complete and all cycle are fully accepting ( all transitions + /// have all acceptance conditions) + bool + is_terminal_heuristic (const tgba *a, scc_map& map, unsigned scc); + + /// \brief wether a SCC is weak using an heuristic + /// + /// The heuristic looks if all path are fully accepting + bool + is_weak_heuristic(scc_map& map, unsigned scc); /// @} }