From 2bd2abd4c9de9b7f16bc679aed0db36645077b89 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 May 2024 10:20:45 +0200 Subject: [PATCH] pdegen & toparity: minor refactor * spot/twaalgos/degen.hh (is_partially_degeneralizable): Pass the forbid vector by reference, and document it. I hope that not passing forbid by copy will get rid of a spurious "potential nullptr" warning by gcc on Arch Linux. * spot/twaalgos/degen.cc: Adjust, and refactor the code a bit. * spot/twaalgos/toparity.cc: Likewise. --- spot/twaalgos/degen.cc | 27 ++--- spot/twaalgos/degen.hh | 9 +- spot/twaalgos/toparity.cc | 218 +++++++++++++++++++------------------- 3 files changed, 126 insertions(+), 128 deletions(-) diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 897062cb3..77790c5d3 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -872,7 +872,7 @@ namespace spot acc_cond::mark_t is_partially_degeneralizable(const const_twa_graph_ptr& aut, bool allow_inf, bool allow_fin, - std::vector forbid) + const std::vector& forbid) { auto& code = aut->get_acceptance(); @@ -881,16 +881,19 @@ namespace spot acc_cond::mark_t res = {}; unsigned res_sz = -1U; - auto update = [&](const acc_cond::mark_t& m) + + auto keep_smallest_mark = [&](const acc_cond::mark_t& m) { + if (std::find(forbid.begin(), forbid.end(), m) != forbid.end()) + return false; unsigned sz = m.count(); if (sz > 1 && sz < res_sz) { res_sz = sz; res = m; } - // If we have found a pair to degeneralize, we - // won't find + // If we have found a pair to degeneralize, we won't find a + // smaller one. return res_sz == 2; }; @@ -906,22 +909,14 @@ namespace spot case acc_cond::acc_op::Fin: case acc_cond::acc_op::FinNeg: pos -= 2; - if (allow_fin) - { - auto m = code[pos].mark; - if (!std::count(forbid.begin(), forbid.end(), m) && update(m)) - return res; - } + if (allow_fin && keep_smallest_mark(code[pos].mark)) + return res; break; case acc_cond::acc_op::Inf: case acc_cond::acc_op::InfNeg: pos -= 2; - if (allow_inf) - { - auto m = code[pos].mark; - if (!std::count(forbid.begin(), forbid.end(), m) && update(m)) - return res; - } + if (allow_inf && keep_smallest_mark(code[pos].mark)) + return res; break; } } diff --git a/spot/twaalgos/degen.hh b/spot/twaalgos/degen.hh index 643c1d219..833157bfa 100644 --- a/spot/twaalgos/degen.hh +++ b/spot/twaalgos/degen.hh @@ -158,11 +158,14 @@ namespace spot /// /// The optional arguments \a allow_inf and \a allow_fin, can be set /// to false to disallow one type of match. + /// + /// If you need to disallow certain marks from being returned, pass + /// them in the \a forbid vector. SPOT_API acc_cond::mark_t is_partially_degeneralizable(const const_twa_graph_ptr& aut, - bool allow_inf = true, - bool allow_fin = true, - std::vector forbid = {}); + bool allow_inf = true, bool allow_fin = true, + const std::vector& + forbid = {}); /// \ingroup twa_algorithms /// \brief Propagate marks around the automaton diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index 960f4daaa..a8a42dc57 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -2198,17 +2198,17 @@ namespace spot return true; std::vector pairs; if (deg->acc().is_rabin_like(pairs)) - { - remove_duplicates(pairs); - if (pairs.size() < nb_col_orig) - return true; - } + { + remove_duplicates(pairs); + if (pairs.size() < nb_col_orig) + return true; + } if (deg->acc().is_streett_like(pairs)) - { - remove_duplicates(pairs); - if (pairs.size() < nb_col_orig) - return true; - } + { + remove_duplicates(pairs); + if (pairs.size() < nb_col_orig) + return true; + } return false; } @@ -2223,118 +2223,118 @@ namespace spot max_color_scc_ = 0; // If the sub_automaton is "empty", we don't need to apply an algorithm. if (sub_aut->num_edges() == 0) - { - apply_copy(sub_aut, {}, none_algo); - return; - } + { + apply_copy(sub_aut, {}, none_algo); + return; + } bool tried_emptiness = false; bool changed_structure = true; while (true) - { - auto cond_before_simpl = sub_aut->acc(); - if (opt_.acc_clean) - simplify_acceptance_here(sub_aut); - if (opt_.propagate_col) { - propagate_marks_here(sub_aut); + auto cond_before_simpl = sub_aut->acc(); if (opt_.acc_clean) simplify_acceptance_here(sub_aut); - } - if (opt_.datas && sub_aut->acc() != cond_before_simpl) - algo_used_ |= algorithm::ACC_CLEAN; - - if (opt_.parity_equiv || opt_.parity_prefix) - { - // If we don't try to find a parity prefix, we can stop - // to construct the tree when it has not parity shape. - zielonka_tree_options zopt = zielonka_tree_options::MERGE_SUBTREES - | zielonka_tree_options::CHECK_PARITY; - if (!opt_.parity_prefix) - zopt = zopt | zielonka_tree_options::ABORT_WRONG_SHAPE; - auto tree = zielonka_tree(sub_aut->acc(), zopt); - // If it is not parity shape, tree.nodes_ will be empty - if (tree.num_branches() != 0 && opt_.parity_equiv - && try_parity_equivalence(tree, sub_aut)) - return; - if (opt_.parity_prefix && try_parity_prefix(tree, sub_aut)) - return; - } - - if (changed_structure && opt_.parity_prefix_general - && try_parity_prefix_general(sub_aut)) - return; - - if (opt_.generic_emptiness && !tried_emptiness - && try_emptiness(sub_aut, tried_emptiness)) - return; - - // Buchi_type_to_buchi is more general that Rabin_to_buchi so - // we just call rabin_to_buchi if buchi_type_to_buchi is false. - if (!opt_.buchi_type_to_buchi && !opt_.parity_type_to_parity - && opt_.rabin_to_buchi - && try_rabin_to_buchi(sub_aut)) - return; - - // As parity_type_to_parity is stronger, we don't - // try if this option is used. - if (opt_.buchi_type_to_buchi && !opt_.parity_type_to_parity - && try_buchi_type(sub_aut)) - return; - - // We don't do it if parity_prefix_general is true as on a parity-type - // automaton parity_prefix_general removes all the transitions and - // we also get a parity-type automaton. - if (!opt_.parity_prefix_general && opt_.parity_type_to_parity - && try_parity_type(sub_aut)) - return; - - if (opt_.partial_degen - && is_partially_degeneralizable(sub_aut, true, true)) - { - auto deg = sub_aut; - std::vector forbid; - auto m = is_partially_degeneralizable(sub_aut, true, true, forbid); - bool changed = false; - while (m) - { - auto tmp = partial_degeneralize(deg, m); - simplify_acceptance_here(tmp); - if (keep_deg(deg, tmp)) + if (opt_.propagate_col) { - algo_used_ |= algorithm::PARTIAL_DEGEN; - deg = tmp; - changed = true; - changed_structure = true; + propagate_marks_here(sub_aut); + if (opt_.acc_clean) + simplify_acceptance_here(sub_aut); } - else - forbid.emplace_back(m); - m = is_partially_degeneralizable(deg, true, true, forbid); - } + if (opt_.datas && sub_aut->acc() != cond_before_simpl) + algo_used_ |= algorithm::ACC_CLEAN; - if (changed) - { - sub_aut = deg; - continue; - } + if (opt_.parity_equiv || opt_.parity_prefix) + { + // If we don't try to find a parity prefix, we can stop + // to construct the tree when it has not parity shape. + zielonka_tree_options zopt = + zielonka_tree_options::MERGE_SUBTREES + | zielonka_tree_options::CHECK_PARITY; + if (!opt_.parity_prefix) + zopt = zopt | zielonka_tree_options::ABORT_WRONG_SHAPE; + auto tree = zielonka_tree(sub_aut->acc(), zopt); + // If it is not parity shape, tree.nodes_ will be empty + if (tree.num_branches() != 0 && opt_.parity_equiv + && try_parity_equivalence(tree, sub_aut)) + return; + if (opt_.parity_prefix && try_parity_prefix(tree, sub_aut)) + return; + } + + if (changed_structure && opt_.parity_prefix_general + && try_parity_prefix_general(sub_aut)) + return; + + if (opt_.generic_emptiness + && !tried_emptiness && try_emptiness(sub_aut, tried_emptiness)) + return; + + // Buchi_type_to_buchi is more general that Rabin_to_buchi so + // we just call rabin_to_buchi if buchi_type_to_buchi is false. + if (!opt_.buchi_type_to_buchi + && !opt_.parity_type_to_parity && opt_.rabin_to_buchi + && try_rabin_to_buchi(sub_aut)) + return; + + // As parity_type_to_parity is stronger, we don't + // try if this option is used. + if (opt_.buchi_type_to_buchi + && !opt_.parity_type_to_parity && try_buchi_type(sub_aut)) + return; + + // We don't do it if parity_prefix_general is true as on a parity-type + // automaton parity_prefix_general removes all the transitions and + // we also get a parity-type automaton. + if (!opt_.parity_prefix_general && opt_.parity_type_to_parity + && try_parity_type(sub_aut)) + return; + + if (opt_.partial_degen) + { + twa_graph_ptr deg = sub_aut; + std::vector forbid; + bool changed = false; + while (acc_cond::mark_t m = + is_partially_degeneralizable(deg, true, true, forbid)) + { + twa_graph_ptr tmp = partial_degeneralize(deg, m); + simplify_acceptance_here(tmp); + if (keep_deg(deg, tmp)) + { + algo_used_ |= algorithm::PARTIAL_DEGEN; + deg = tmp; + changed = true; + changed_structure = true; + } + else + { + forbid.emplace_back(m); + } + } + if (changed) + { + sub_aut = deg; + continue; + } + } + break; } - break; - } if (opt_.use_generalized_rabin) - { - auto gen_rab = to_generalized_rabin(sub_aut); - // to_generalized_rabin does not propagate original-states. - auto sub_aut_orig = + { + auto gen_rab = to_generalized_rabin(sub_aut); + // to_generalized_rabin does not propagate original-states. + auto sub_aut_orig = sub_aut->get_named_prop>("original-states"); - assert(sub_aut_orig); - auto orig = new std::vector(); - const auto sub_aut_num_states = sub_aut->num_states(); - orig->reserve(sub_aut_num_states); - gen_rab->set_named_prop("original-states", orig); - for (unsigned i = 0; i < sub_aut_num_states; ++i) - orig->push_back((*sub_aut_orig)[i]); - sub_aut = partial_degeneralize(gen_rab); - } + assert(sub_aut_orig); + auto orig = new std::vector(); + const auto sub_aut_num_states = sub_aut->num_states(); + orig->reserve(sub_aut_num_states); + gen_rab->set_named_prop("original-states", orig); + for (unsigned i = 0; i < sub_aut_num_states; ++i) + orig->push_back((*sub_aut_orig)[i]); + sub_aut = partial_degeneralize(gen_rab); + } std::vector pairs; algorithm algo = choose_lar(sub_aut->acc(), pairs, sub_aut->num_edges()); if (opt_.datas)