diff --git a/NEWS b/NEWS index a4d426531..9b3744699 100644 --- a/NEWS +++ b/NEWS @@ -56,6 +56,19 @@ New in spot 1.0.2a (not released): with the favor_event_univ option of ltl_simplifier. As always please check doc/tl/tl.tex for the list of rules. + - Several functions have been introduced to check the + strength of an SCC. + is_inherently_weak_scc() + is_weak_scc() + is_syntactic_weak_scc() + is_complete_scc() + is_terminal_scc() + is_syntactic_terminal_scc() + + Beware that the costly is_weak_scc() function introduced in Spot + 1.0, which is based on a cycle enumeration, has been renammed to + is_inherently_weak_scc() to match established vocabulary. + * Command-line tools: - ltl2tgba and ltl2tgta now honor a new --extra-options (or -x) diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index da6d278ac..1777840da 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2012 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -67,15 +67,11 @@ namespace spot } bool - is_weak_scc(scc_map& map, unsigned scc, bool easydetect) + is_inherently_weak_scc(scc_map& map, unsigned scc) { // 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 (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. weak_checker w(map); @@ -84,104 +80,106 @@ namespace spot } bool - is_syntactic_weak_scc(const spot::tgba *a, scc_map& map, unsigned scc) + is_weak_scc(scc_map& map, unsigned scc) { + // 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. + return (map.useful_acc_of(scc) + == bdd_support(map.get_aut()->neg_acceptance_conditions())); + } + + bool + is_syntactic_weak_scc(scc_map& map, unsigned scc) + { + const tgba_explicit_formula* aut = + dynamic_cast(map.get_aut()); + if (!aut) + return false; + const std::list states = map.states_of(scc); std::list::const_iterator it; - for (it = states.begin(); it != states.end(); 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())) + const state_explicit_formula* s = + down_cast(*it); + assert(s); + if (aut->get_label(s)->is_syntactic_persistence()) return true; - } return false; } bool - is_syntactic_terminal_scc(const spot::tgba *a, scc_map& map, unsigned scc) + is_syntactic_terminal_scc(scc_map& map, unsigned scc) { + const tgba_explicit_formula* aut = + dynamic_cast(map.get_aut()); + if (!aut) + return false; + const std::list states = map.states_of(scc); std::list::const_iterator it; - for (it = states.begin(); it != states.end(); 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()) + const state_explicit_formula* s = + down_cast(*it); + assert(s); + if (aut->get_label(s)->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) + is_complete_scc(scc_map& map, unsigned scc) { + const spot::tgba *a = map.get_aut(); const std::list states = map.states_of(scc); std::list::const_iterator it; - for (it = states.begin(); it != states.end(); it++) + for (it = states.begin(); it != states.end(); ++it) { - const state *s = (*it); + const state *s = *it; tgba_succ_iterator* it = a->succ_iter(s); it->first(); - // No successors cannot be complete + // If a state has no successors, the SCC is not complete. if (it->done()) { delete it; return false; } + // Sum guards on all outgoing transitions. bdd sumall = bddfalse; - while (!it->done()) + do { const state *next = it->current_state(); - unsigned sccnum = map.scc_of_state(next); - // check it's the same scc - if (sccnum == scc) + if (map.scc_of_state(next) == scc) sumall |= it->current_condition(); next->destroy(); + if (sumall == bddtrue) + break; it->next(); } + while (!it->done()); delete it; if (sumall != bddtrue) - { - return false; - } + return false; } return true; } bool - is_terminal_heuristic (const tgba *a, scc_map& map, unsigned scc) + is_terminal_scc(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; + return ((map.useful_acc_of(scc) == + bdd_support(map.get_aut()->neg_acceptance_conditions())) + && is_complete_scc(map, scc)); } } diff --git a/src/tgbaalgos/isweakscc.hh b/src/tgbaalgos/isweakscc.hh index bc55be008..85aa6d424 100644 --- a/src/tgbaalgos/isweakscc.hh +++ b/src/tgbaalgos/isweakscc.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2012 Laboratoire de Recherche et Developpement de +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,62 +26,68 @@ namespace spot /// \addtogroup tgba_misc /// @{ + /// \brief Whether the SCC number \a scc in \a map is inherently + /// weak. + /// + /// An SCC is inherently weak if either its cycles are all + /// accepting, or they are all non-accepting. + /// + /// Note the terminal SCCs are also inherently weak with that + /// definition. + /// + /// 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_inherently_weak_scc(scc_map& map, unsigned scc); + /// \brief Whether the SCC number \a scc in \a map is weak. /// - /// An SCC is weak if either its cycles are all accepting, or they - /// are all non-accepting. + /// An SCC is weak if its non-accepting, or if all its transition + /// are fully accepting (i.e., the belong to all acceptance sets). /// - /// 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_weak_scc(scc_map& map, unsigned scc, bool easydetect = true); + /// Note that terminal SCCs are also weak with that definition. + /// + /// The scc_map \a map should have been built already. + bool is_weak_scc(scc_map& map, unsigned scc); - /// \brief Whether the SCC number \a scc in \a map is complete + /// \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); + /// An SCC is complete iff for all states and all label there exists + /// a transition that stays into this SCC. + /// + /// The scc_map \a map should have been built already. + bool is_complete_scc(scc_map& map, unsigned scc); - /// \brief Whether the SCC number \a scc in \a map is syntactically weak. + /// \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 + /// This works only on tgba whose labels are formulas. An SCC is + /// syntactically weak if one of its states is labeled by a + /// syntactic-persistence formula. /// - /// 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); + /// The scc_map \a map should have been built already. + bool is_syntactic_weak_scc(scc_map& map, unsigned scc); - /// \brief wether a SCC is syntactically characterized by a gurarantee - /// formula + /// \brief Whether the SCC number \a scc in \a map is syntactically + /// terminal. /// - /// 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 + /// This works only on tgba whose labels are formulas. An SCC is + /// syntactically terminal if one of its states is labeled by a + /// syntactic-guarantee formula. /// - /// 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); + /// The scc_map \a map should have been built already. + bool is_syntactic_terminal_scc(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); + /// \brief Whether the SCC number \a scc in \a map is terminal. + /// + /// An SCC is terminal if it is weak, complete, and accepting. + /// + /// The scc_map \a map should have been built already. + bool is_terminal_scc(scc_map& map, unsigned scc); /// @} }