diff --git a/NEWS b/NEWS index 8c17eecfc..be3d100f6 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,8 @@ New in spot 1.99.6a (not yet released) Command-line tools: + * autfilt has a new option: --is-inherently-weak. + Library: * Installed headers now assume that they will be included as @@ -23,6 +25,10 @@ New in spot 1.99.6a (not yet released) of $includedir/spot/iface/, so that installed and non-installed directories can be used similarly. + * is_inherently_weak_automaton() is a new function, and + check_strength() has been modified to also check inherently weak + automata. + Python: Documentation: diff --git a/doc/org/hoa.org b/doc/org/hoa.org index c14f98597..cd01deebd 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -666,7 +666,7 @@ particular: | =stutter-sensitive= | trusted | yes | as stored | can be checked with =--check=stuttering= | | =terminal= | trusted | yes | as stored | can be checked with =--check=strength= | | =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | can be checked with =--check=strength= | -| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | | +| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | can be checked with =--check=strength= | | =colored= | ignored | no | checked | | ** Named properties @@ -942,4 +942,5 @@ bits section above), and property that are trivial to compute. Command-line tools with a HOA output all have a =--check= option that can be used to request additional checks such as testing whether the -automaton is stutter-invariant, unambiguous, weak, and terminal. +automaton is stutter-invariant, unambiguous, (inherently) weak, and +terminal. diff --git a/spot/bin/autfilt.cc b/spot/bin/autfilt.cc index 807db2098..c1da0479e 100644 --- a/spot/bin/autfilt.cc +++ b/spot/bin/autfilt.cc @@ -89,6 +89,7 @@ enum { OPT_IS_UNAMBIGUOUS, OPT_IS_TERMINAL, OPT_IS_WEAK, + OPT_IS_INHERENTLY_WEAK, OPT_KEEP_STATES, OPT_MASK_ACC, OPT_MERGE, @@ -200,6 +201,8 @@ static const argp_option options[] = "keep only terminal automata", 0 }, { "is-weak", OPT_IS_WEAK, nullptr, 0, "keep only weak automata", 0 }, + { "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0, + "keep only inherently weak automata", 0 }, { "intersect", OPT_INTERSECT, "FILENAME", 0, "keep automata whose languages have an non-empty intersection with" " the automaton from FILENAME", 0 }, @@ -268,6 +271,7 @@ static bool opt_is_deterministic = false; static bool opt_is_unambiguous = false; static bool opt_is_terminal = false; static bool opt_is_weak = false; +static bool opt_is_inherently_weak = false; static bool opt_invert = false; static range opt_states = { 0, std::numeric_limits::max() }; static range opt_edges = { 0, std::numeric_limits::max() }; @@ -379,6 +383,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_IS_EMPTY: opt_is_empty = true; break; + case OPT_IS_INHERENTLY_WEAK: + opt_is_inherently_weak = true; + break; case OPT_IS_UNAMBIGUOUS: opt_is_unambiguous = true; break; @@ -594,6 +601,8 @@ namespace matched &= is_terminal_automaton(aut); else if (opt_is_weak) matched &= is_weak_automaton(aut); + else if (opt_is_inherently_weak) + matched &= is_inherently_weak_automaton(aut); if (opt->are_isomorphic) matched &= opt->isomorphism_checker->is_isomorphic(aut); if (opt_is_empty) diff --git a/spot/tests/readsave.test b/spot/tests/readsave.test index 08cf14dbf..4fba986e6 100755 --- a/spot/tests/readsave.test +++ b/spot/tests/readsave.test @@ -737,6 +737,7 @@ State: 2 {0 1} [0] 2 EOF test `$autfilt --is-weak -c input4` = 1 +test `$autfilt --is-inherently-weak -c input4` = 1 test `$autfilt --is-terminal -c input4` = 0 $autfilt -H --small --high input4 >output4 @@ -837,3 +838,62 @@ State: [0] 2 {0} EOF diff output6 expect6 + + +cat >input7 <output7 +cat >expected7 <input8 <. -#include #include #include +#include namespace spot { - namespace + bool + scc_has_rejecting_cycle(scc_info& map, unsigned scc) { - // Look for a non-accepting cycle. - class weak_checker final : public enumerate_cycles - { - public: - bool result; - - weak_checker(const scc_info& map) - : enumerate_cycles(map), result(true) - { - } - - virtual bool - cycle_found(unsigned start) override - { - dfs_stack::const_reverse_iterator i = dfs_.rbegin(); - acc_cond::mark_t acc = 0U; - for (;;) - { - acc |= aut_->edge_storage(i->succ).acc; - if (i->s == start) - break; - ++i; - // The const cast is here to please old g++ versions. - // At least version 4.0 needs it. - assert(i != const_cast(dfs_).rend()); - } - if (!aut_->acc().accepting(acc)) - { - // We have found an non-accepting cycle, so the SCC is not - // weak. - result = false; - return false; - } - return true; - } - - }; + // We check that by cloning the SCC and complementing its + // acceptance condition. + auto aut = map.get_aut(); + std::vector keep(aut->num_states(), false); + auto& states = map.states_of(scc); + for (auto s: states) + keep[s] = true; + auto sccaut = mask_keep_states(aut, keep, states.front()); + sccaut->set_acceptance(sccaut->acc().num_sets(), + sccaut->get_acceptance().complement()); + return !sccaut->is_empty(); } bool @@ -70,11 +45,10 @@ namespace spot // Weak SCCs are inherently weak. if (is_weak_scc(map, scc)) return true; - // If the SCC is accepting, but one cycle is not, the SCC is not - // weak. - weak_checker w(map); - w.run(scc); - return w.result; + // If we reach this place, we now the SCC has an accepting cycle. + // The question is now to find whether is also contains a + // rejecting cycle. + return !scc_has_rejecting_cycle(map, scc); } bool diff --git a/spot/twaalgos/isweakscc.hh b/spot/twaalgos/isweakscc.hh index ba019c651..d2a473396 100644 --- a/spot/twaalgos/isweakscc.hh +++ b/spot/twaalgos/isweakscc.hh @@ -26,6 +26,11 @@ namespace spot /// \addtogroup twa_misc /// @{ + /// \brief Whether the SCC number \a scc in \a map has a rejecting + /// cycle. + SPOT_API bool + scc_has_rejecting_cycle(scc_info& map, unsigned scc); + /// \brief Whether the SCC number \a scc in \a map is inherently /// weak. /// @@ -34,13 +39,6 @@ namespace spot /// /// Note the terminal SCCs are also inherently weak with that /// definition. - /// - /// The absence of accepting cycle is easy to check (the scc_info - /// object 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). SPOT_API bool is_inherently_weak_scc(scc_info& map, unsigned scc); diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 787a95368..6367ef016 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -27,7 +27,7 @@ namespace spot { namespace { - template + template bool is_type_automaton(const twa_graph_ptr& aut, scc_info* si) { // Create an scc_info if the user did not give one to us. @@ -36,6 +36,7 @@ namespace spot si = new scc_info(aut); si->determine_unknown_acceptance(); + bool is_inweak = true; bool is_weak = true; bool is_term = true; unsigned n = si->scc_count(); @@ -45,21 +46,32 @@ namespace spot continue; bool first = true; acc_cond::mark_t m = 0U; - for (auto src: si->states_of(i)) - for (auto& t: aut->out(src)) - if (si->scc_of(t.dst) == i) + if (is_weak) + for (auto src: si->states_of(i)) + for (auto& t: aut->out(src)) + if (si->scc_of(t.dst) == i) + { + if (first) + { + first = false; + m = t.acc; + } + else if (m != t.acc) + { + is_weak = false; + if (!inweak) + goto exit; + } + } + if (!is_weak && si->is_accepting_scc(i)) + { + assert(inweak); + if (scc_has_rejecting_cycle(*si, i)) { - if (first) - { - first = false; - m = t.acc; - } - else if (m != t.acc) - { - is_weak = false; - goto exit; - } + is_inweak = false; + break; } + } if (terminal && si->is_accepting_scc(i) && !is_complete_scc(*si, i)) { is_term = false; @@ -75,7 +87,10 @@ namespace spot if (terminal) aut->prop_terminal(is_term && is_weak); aut->prop_weak(is_weak); + aut->prop_inherently_weak(is_inweak); } + if (inweak) + return is_inweak; return is_weak && is_term; } } @@ -96,9 +111,17 @@ namespace spot si)); } + bool + is_inherently_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si) + { + return (aut->prop_inherently_weak() || + is_type_automaton + (std::const_pointer_cast(aut), si)); + } + void check_strength(const twa_graph_ptr& aut, scc_info* si) { - is_type_automaton(aut, si); + is_type_automaton(aut, si); } bool is_safety_mwdba(const const_twa_graph_ptr& aut) diff --git a/spot/twaalgos/strength.hh b/spot/twaalgos/strength.hh index a455f2b2a..94ae3b919 100644 --- a/spot/twaalgos/strength.hh +++ b/spot/twaalgos/strength.hh @@ -38,7 +38,7 @@ namespace spot /// \brief Whether an automaton is weak. /// - /// An automaton is weak if if any given SCC, all transitions belong + /// An automaton is weak if in any given SCC, all transitions belong /// to the same acceptance sets. /// /// \param aut the automaton to check @@ -48,6 +48,19 @@ namespace spot SPOT_API bool is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr); + /// \brief Whether an automaton is inherently weak. + /// + /// An automaton is inherently weak if in any given SCC, there + /// are only accepting cycles, or only rejecting cycles. + /// + /// \param aut the automaton to check + /// + /// \param sm an scc_info object for the automaton if available (it + /// will be built otherwise). + SPOT_API bool + is_inherently_weak_automaton(const const_twa_graph_ptr& aut, + scc_info* sm = nullptr); + /// \brief Whether a minimized WDBA represents a safety property. /// /// A minimized WDBA (as returned by a successful run of