diff --git a/NEWS b/NEWS index a1bf329de..6ce684802 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,9 @@ New in spot 1.99.5a (not yet released) + Command-line tools: + + * autfilt has two now filters: --is-weak and --is-terminal. + Library: * Properties of automata (like the "properties:" line of the HOA diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 80b6cf9bb..a37009377 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -57,6 +57,7 @@ #include "twaalgos/cleanacc.hh" #include "twaalgos/dtgbasat.hh" #include "twaalgos/complement.hh" +#include "twaalgos/strength.hh" static const char argp_program_doc[] ="\ Convert, transform, and filter omega-automata.\v\ @@ -85,6 +86,8 @@ enum { OPT_IS_DETERMINISTIC, OPT_IS_EMPTY, OPT_IS_UNAMBIGUOUS, + OPT_IS_TERMINAL, + OPT_IS_WEAK, OPT_KEEP_STATES, OPT_MASK_ACC, OPT_MERGE, @@ -189,6 +192,10 @@ static const argp_option options[] = "keep automata with an empty language", 0 }, { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0, "keep only unambiguous automata", 0 }, + { "is-terminal", OPT_IS_TERMINAL, nullptr, 0, + "keep only terminal automata", 0 }, + { "is-weak", OPT_IS_WEAK, nullptr, 0, + "keep only weak automata", 0 }, { "intersect", OPT_INTERSECT, "FILENAME", 0, "keep automata whose languages have an non-empty intersection with" " the automaton from FILENAME", 0 }, @@ -255,6 +262,8 @@ static bool opt_merge = false; static bool opt_is_complete = false; 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_invert = false; static range opt_states = { 0, std::numeric_limits::max() }; static range opt_edges = { 0, std::numeric_limits::max() }; @@ -365,6 +374,12 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_IS_UNAMBIGUOUS: opt_is_unambiguous = true; break; + case OPT_IS_TERMINAL: + opt_is_terminal = true; + break; + case OPT_IS_WEAK: + opt_is_weak = true; + break; case OPT_MERGE: opt_merge = true; break; @@ -567,6 +582,10 @@ namespace matched &= is_deterministic(aut); else if (opt_is_unambiguous) matched &= is_unambiguous(aut); + if (opt_is_terminal) + matched &= is_terminal_automaton(aut); + else if (opt_is_weak) + matched &= is_weak_automaton(aut); if (opt->are_isomorphic) matched &= opt->isomorphism_checker->is_isomorphic(aut); if (opt_is_empty) diff --git a/src/tests/readsave.test b/src/tests/readsave.test index 082bb9866..aa271dbd3 100755 --- a/src/tests/readsave.test +++ b/src/tests/readsave.test @@ -51,6 +51,8 @@ EOF run 0 $autfilt --hoa input > stdout diff stdout input +test `$autfilt -c --is-weak input` = 0 + # Transition merging cat >input <<\EOF HOA: v1 @@ -714,6 +716,9 @@ State: 2 {0 1} [0] 2 --END-- EOF +test `$autfilt --is-weak -c input4` = 1 +test `$autfilt --is-terminal -c input4` = 0 + $autfilt -H --small --high input4 >output4 $autfilt -H --small input4 >output4b $autfilt -H --high input4 >output4c @@ -742,6 +747,12 @@ diff output4b expect4 diff output4c expect4 $autfilt -Hv --small input4 >output5 +test `$autfilt --is-weak -c output4` = 1 +test `$autfilt --is-terminal -c output4` = 0 + +sed 's/\[0\]/[t]/g' expect4 > output4d +test `$autfilt --is-terminal -c output4d` = 1 + cat >expect5< namespace spot { + namespace + { + template + bool is_type_automaton(const const_twa_graph_ptr& aut, scc_info* si) + { + // Create an scc_info if the user did not give one to us. + bool need_si = !si; + if (need_si) + si = new scc_info(aut); + si->determine_unknown_acceptance(); + + bool result = true; + unsigned n = si->scc_count(); + for (unsigned i = 0; i < n; ++i) + { + if (si->is_trivial(i)) + 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 (first) + { + first = false; + m = t.acc; + } + else if (m != t.acc) + { + result = false; + goto exit; + } + } + if (terminal && si->is_accepting_scc(i) && !is_complete_scc(*si, i)) + { + result = false; + break; + } + } + exit: + if (need_si) + delete si; + return result; + } + } + bool is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si) { - if (aut->prop_terminal()) - return true; - // Create an scc_info if the user did not give one to us. - bool need_si = !si; - if (need_si) - si = new scc_info(aut); - si->determine_unknown_acceptance(); + return aut->prop_terminal() || is_type_automaton(aut, si); + } - bool result = true; - - for (auto& scc: *si) - { - if (scc.is_rejecting()) - continue; - // Accepting SCCs should have only one state. - auto& st = scc.states(); - if (st.size() != 1) - { - result = false; - break; - } - // The state should have only one edge that is a - // self-loop labelled by true. - auto src = st.front(); - auto out = aut->out(src); - auto it = out.begin(); - assert(it != out.end()); - result = - (it->cond == bddtrue) && (it->dst == src) && (++it == out.end()); - if (!result) - break; - } - - if (need_si) - delete si; - return result; + bool + is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si) + { + return aut->prop_weak() || is_type_automaton(aut, si); } bool is_safety_mwdba(const const_twa_graph_ptr& aut) diff --git a/src/twaalgos/strength.hh b/src/twaalgos/strength.hh index 3ca1ee7c7..6bc197cb1 100644 --- a/src/twaalgos/strength.hh +++ b/src/twaalgos/strength.hh @@ -25,9 +25,8 @@ namespace spot { /// \brief Whether an automaton is terminal. /// - /// An automaton is terminal if any accepting path ends on an - /// accepting state with only one transition that is a self-loop - /// labelled by true. + /// An automaton is terminal if it is weak, and all accepting SCCs + /// are complete. /// /// \param aut the automaton to check /// @@ -36,6 +35,19 @@ namespace spot SPOT_API bool is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr); + + /// \brief Whether an automaton is weak. + /// + /// An automaton is weak if if any given SCC, all transitions belong + /// to the same acceptance sets. + /// + /// \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_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