From 55db24e00eaa0fcc80973b9cabdf14298e95dfc4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 30 Mar 2019 11:03:03 +0100 Subject: [PATCH] scc_info: introduce scc_and_mark_filter * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Here. * spot/twaalgos/genem.cc: Use it. * python/spot/impl.i, python/spot/__init__.py: Add bindings. * tests/python/genem.py: Test it. * NEWS: Mention it. --- NEWS | 6 ++ python/spot/__init__.py | 9 +++ python/spot/impl.i | 1 - spot/twaalgos/genem.cc | 28 ++------- spot/twaalgos/sccinfo.cc | 19 ++++++ spot/twaalgos/sccinfo.hh | 127 +++++++++++++++++++++++++++++++++++++++ tests/python/genem.py | 114 ++++++++++++++++++++++++++++------- 7 files changed, 256 insertions(+), 48 deletions(-) diff --git a/NEWS b/NEWS index 8554b7225..8b0b94c82 100644 --- a/NEWS +++ b/NEWS @@ -29,6 +29,12 @@ New in spot 2.7.2.dev (not yet released) allows "autfilt [-D] --small" to minimize very-weak automata whenever they are found to represent obligation properties.) + - There is a new spot::scc_and_mark_filter objet that simplify the + creation of filters to restrict spot::scc_info to some particular + SCC while cutting new SCCs on given acceptance sets. This is used + by spot::generic_emptiness_check() when processing SCCs + recursively, and makes it easier to write similar code in Python. + Bugs fixed: - When processing CSV files with MSDOS-style \r\n line endings, diff --git a/python/spot/__init__.py b/python/spot/__init__.py index dc7b9efbc..aabf0c4c3 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1244,3 +1244,12 @@ class twa_word: """ from IPython.display import SVG return SVG(self.as_svg()) + + +# Make scc_and_mark filter usable as context manager +@_extend(scc_and_mark_filter) +class scc_and_mark_filter: + def __enter__(self): + return self + def __exit__(self, exc_type, exc_value, traceback): + self.restore_acceptance() diff --git a/python/spot/impl.i b/python/spot/impl.i index f8597d528..492fe27c8 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -832,7 +832,6 @@ def state_is_accepting(self, src) -> "bool": std::string __str__() { return spot::str_psl(*self); } } - %runtime %{ #include diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index c6e35039d..94ad8cfdf 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -57,36 +57,16 @@ namespace spot twa_run_ptr run, acc_cond::mark_t tocut)) { - struct filter_data_t { - const scc_info& lower_si; - unsigned lower_scc; - acc_cond::mark_t cut_sets; - } - data = {si, scc, tocut}; - - scc_info::edge_filter filter = - [](const twa_graph::edge_storage_t& e, unsigned dst, - void* filter_data) -> scc_info::edge_filter_choice - { - auto& data = *reinterpret_cast(filter_data); - if (data.lower_si.scc_of(dst) != data.lower_scc) - return scc_info::edge_filter_choice::ignore; - if (data.cut_sets & e.acc) - return scc_info::edge_filter_choice::cut; - return scc_info::edge_filter_choice::keep; - }; - // We want to remove tocut from the acceptance condition right // now, because hopefully this will convert the acceptance // condition into a Fin-less one, and then we do not have to // recurse it. - acc_cond::mark_t sets = si.acc_sets_of(scc) - tocut; auto& autacc = si.get_aut()->acc(); - acc_cond acc = autacc.restrict_to(sets); + acc_cond acc = autacc.restrict_to(si.acc_sets_of(scc) - tocut); acc = acc.remove(si.common_sets_of(scc), false); - temporary_acc_set tmp(si.get_aut(), acc); - scc_info upper_si(si.get_aut(), si.one_state_of(scc), filter, &data, - scc_info_options::STOP_ON_ACC); + scc_and_mark_filter filt(si, scc, tocut); + filt.override_acceptance(acc); + scc_info upper_si(filt, scc_info_options::STOP_ON_ACC); const int accepting_scc = upper_si.one_accepting_scc(); if (accepting_scc >= 0) diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 2bb344d74..d50794ef3 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -75,6 +75,12 @@ namespace spot }; } + scc_info::scc_info(scc_and_mark_filter& filt, scc_info_options options) + : scc_info(filt.get_aut(), filt.start_state(), + filt.get_filter(), &filt, options) + { + } + scc_info::scc_info(const_twa_graph_ptr aut, unsigned initial_state, edge_filter filter, @@ -716,6 +722,19 @@ namespace spot unsigned dst) { cur[src] = seen[src] = true; + // if (filter_) + // { + // twa_graph::edge_storage_t e; + // e.cond = cond; + // e.src = src; + // e.dst = dst; + // if (filter_(e, dst, filter_data_) + // != edge_filter_choice::keep) + // { + // cond = bddfalse; + // return; + // } + // } if (scc_of(dst) != scc || (m & sets) || (seen[dst] && !cur[dst])) diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 9ccf58a2b..0cd100ac1 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -350,6 +350,8 @@ namespace spot | static_cast(right)); } + class SPOT_API scc_and_mark_filter; + /// \ingroup twa_misc /// \brief Compute an SCC map and gather assorted information. /// @@ -449,11 +451,31 @@ namespace spot } /// @} + /// @{ + /// \brief Create an scc_info map from some filter. + /// + /// This is usually used to prevent some edges from being + /// considered as part of cycles, and can additionally restrict + /// to exploration to some SCC discovered by another SCC. + scc_info(scc_and_mark_filter& filt, + scc_info_options options = scc_info_options::ALL); + /// @} + const_twa_graph_ptr get_aut() const { return aut_; } + scc_info_options get_options() const + { + return options_; + } + + const void* get_filter_data() const + { + return filter_data_; + } + unsigned scc_count() const { return node_.size(); @@ -687,6 +709,111 @@ namespace spot }; + /// \brief Create a filter for SCC and marks. + /// + /// An scc_and_mark_filter can be passed to scc_info to explore only + /// a specific SCC of the original automaton, and to prevent some + /// acceptance sets from being considered as part of SCCs. + class SPOT_API scc_and_mark_filter + { + protected: + const scc_info* lower_si_; + unsigned lower_scc_; + acc_cond::mark_t cut_sets_; + const_twa_graph_ptr aut_; + acc_cond old_acc_; + bool restore_old_acc_ = false; + + static scc_info::edge_filter_choice + filter_scc_and_mark_(const twa_graph::edge_storage_t& e, + unsigned dst, void* data) + { + auto& d = *reinterpret_cast(data); + if (d.lower_si_->scc_of(dst) != d.lower_scc_) + return scc_info::edge_filter_choice::ignore; + if (d.cut_sets_ & e.acc) + return scc_info::edge_filter_choice::cut; + return scc_info::edge_filter_choice::keep; + }; + + static scc_info::edge_filter_choice + filter_mark_(const twa_graph::edge_storage_t& e, unsigned, void* data) + { + auto& d = *reinterpret_cast(data); + if (d.cut_sets_ & e.acc) + return scc_info::edge_filter_choice::cut; + return scc_info::edge_filter_choice::keep; + }; + + public: + /// \brief Specify how to restrict scc_info to some SCC and acceptance sets + /// + /// \param lower_si the original scc_info that specifies the SCC + /// \param lower_scc the SCC number in lower_si + /// \param cut_sets the acceptance sets that should not be part of SCCs. + scc_and_mark_filter(const scc_info& lower_si, + unsigned lower_scc, + acc_cond::mark_t cut_sets) + : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets), + aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance()) + { + const void* data = lower_si.get_filter_data(); + if (data) + { + auto& d = *reinterpret_cast(data); + cut_sets_ |= d.cut_sets_; + } + } + + /// \brief Specify how to restrict scc_info to some acceptance sets + /// + /// \param aut the automaton to filter + /// \param cut_sets the acceptance sets that should not be part of SCCs. + scc_and_mark_filter(const const_twa_graph_ptr& aut, + acc_cond::mark_t cut_sets) + : lower_si_(nullptr), cut_sets_(cut_sets), aut_(aut), + old_acc_(aut_->get_acceptance()) + { + } + + ~scc_and_mark_filter() + { + restore_acceptance(); + } + + void override_acceptance(const acc_cond& new_acc) + { + std::const_pointer_cast(aut_)->set_acceptance(new_acc); + restore_old_acc_ = true; + } + + void restore_acceptance() + { + if (!restore_old_acc_) + return; + std::const_pointer_cast(aut_)->set_acceptance(old_acc_); + restore_old_acc_ = false; + } + + const_twa_graph_ptr get_aut() const + { + return aut_; + } + + unsigned start_state() const + { + if (lower_si_) + return lower_si_->one_state_of(lower_scc_); + return aut_->get_init_state_number(); + } + + scc_info::edge_filter get_filter() + { + return lower_si_ ? filter_scc_and_mark_ : filter_mark_; + } + }; + + /// \brief Dump the SCC graph of \a aut on \a out. /// /// If \a sccinfo is not given, it will be computed. diff --git a/tests/python/genem.py b/tests/python/genem.py index fc0c26614..d579097c0 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -107,25 +107,12 @@ HOA: v1 States: 2 Acceptance: 6 (Fin(0)|Fin(1))&(Fin(2)|Fin(3))& 1 {1 4} State: 1 [t] 0 {2 5} [t] 1 {3 0 1} --END--""") # From issue #360. -a360 = spot.automaton("""HOA: v1 -States: 2 -Start: 0 -AP: 2 "a" "b" -Acceptance: 8 Fin(5) & (Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0))))) & - (Inf(6) | Inf(7)) & (Fin(6)|Fin(7)) -properties: trans-labels explicit-labels trans-acc complete -properties: deterministic ---BODY-- -State: 0 -[0&1] 0 {4 6 7} -[0&!1] 1 {0 6} -[!0&1] 0 {3 7} -[!0&!1] 0 {0} -State: 1 -[0&1] 0 {4 6 7} -[0&!1] 1 {3 6} -[!0&1] 0 {4 7} -[!0&!1] 1 {0} +a360 = spot.automaton("""HOA: v1 States: 2 Start: 0 AP: 2 "a" +"b" Acceptance: 8 Fin(5) & (Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & +Inf(0))))) & (Inf(6) | Inf(7)) & (Fin(6)|Fin(7)) properties: trans-labels +explicit-labels trans-acc complete properties: deterministic --BODY-- +State: 0 [0&1] 0 {4 6 7} [0&!1] 1 {0 6} [!0&1] 0 {3 7} [!0&!1] 0 {0} +State: 1 [0&1] 0 {4 6 7} [0&!1] 1 {3 6} [!0&1] 0 {4 7} [!0&!1] 1 {0} --END--""") @@ -172,7 +159,7 @@ def generic_emptiness2_rec(aut): return False return True -# The python version of spot.generic_emptiness_check() +# A very old python version of spot.generic_emptiness_check() def generic_emptiness2(aut): old_a = spot.acc_cond(aut.acc()) res = generic_emptiness2_rec(aut) @@ -180,16 +167,97 @@ def generic_emptiness2(aut): aut.set_acceptance(old_a) return res +# A more modern python version of spot.generic_emptiness_check() +def is_empty1(g): + si = spot.scc_info(g, spot.scc_info_options_NONE) + for scc_num in range(si.scc_count()): + if si.is_trivial(scc_num): + continue + if not is_scc_empty1(si, scc_num): + return False + return True + +def is_scc_empty1(si, scc_num, acc=None): + if acc is None: # acceptance isn't forced, get it from the automaton + acc = si.get_aut().acc() + occur, common = si.acc_sets_of(scc_num), si.common_sets_of(scc_num) + acc = acc.restrict_to(occur) + acc = acc.remove(common, False) + if acc.is_t(): return False + if acc.is_f(): return True + if acc.accepting(occur): return False + for cl in acc.top_disjuncts(): + fu = cl.fin_unit() # Is there Fin at the top level + if fu: + with spot.scc_and_mark_filter(si, scc_num, fu) as filt: + filt.override_acceptance(cl.remove(fu, True)) + if not is_empty1(filt): + return False + else: + # Pick some Fin term anywhere in the formula + fo = cl.fin_one() + # Try to solve assuming Fin(fo)=True + with spot.scc_and_mark_filter(si, scc_num, [fo]) as filt: + filt.override_acceptance(cl.remove([fo], True)) + if not is_empty1(filt): + return False + # Try to solve assuming Fin(fo)=False + if not is_scc_empty1(si, scc_num, acc.force_inf([fo])): + return False + return True + +def is_empty2(g): + si = spot.scc_info(g, spot.scc_info_options_STOP_ON_ACC) + if si.one_accepting_scc() >= 0: + return False + for scc_num in range(si.scc_count()): + if si.is_rejecting_scc(scc_num): # this includes trivial SCCs + continue + if not is_scc_empty2(si, scc_num): + return False + return True + +def is_scc_empty2(si, scc_num, acc=None): + if acc is None: # acceptance isn't forced, get it from the automaton + acc = si.get_aut().acc() + occur, common = si.acc_sets_of(scc_num), si.common_sets_of(scc_num) + acc = acc.restrict_to(occur) + acc = acc.remove(common, False) + # 3 stop conditions removed here, because they are caught by + # one_accepting_scc() or is_rejecting_scc() in is_empty2() + for cl in acc.top_disjuncts(): + fu = cl.fin_unit() # Is there Fin at the top level + if fu: + with spot.scc_and_mark_filter(si, scc_num, fu) as filt: + filt.override_acceptance(cl.remove(fu, True)) + if not is_empty1(filt): + return False + else: + # Pick some Fin term anywhere in the formula + fo = cl.fin_one() + # Try to solve assuming Fin(fo)=True + with spot.scc_and_mark_filter(si, scc_num, [fo]) as filt: + filt.override_acceptance(cl.remove([fo], True)) + if not is_empty2(filt): + return False + # Try to solve assuming Fin(fo)=False + if not is_scc_empty2(si, scc_num, acc.force_inf([fo])): + return False + return True + def run_bench(automata): for aut in automata: # Make sure our three implementation behave identically + res5 = is_empty2(aut) + res4 = is_empty1(aut) res3 = spot.generic_emptiness_check(aut) res2 = spot.remove_fin(aut).is_empty() res1 = generic_emptiness2(aut) - res = str(res1)[0] + str(res2)[0] + str(res3)[0] + res = (str(res1)[0] + str(res2)[0] + str(res3)[0] + + str(res4)[0] + str(res5)[0]) print(res) - assert res in ('TTT', 'FFF') - if res == 'FFF': + assert res in ('TTTTT', 'FFFFF') + if res == 'FFFFF': run3 = spot.generic_accepting_run(aut) assert run3.replay(spot.get_cout()) is True