From 69f31c89c6f2d08b100f51ff5a42beba82c928ed Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 18 Feb 2018 08:09:39 +0100 Subject: [PATCH] minor code cleanups * spot/twaalgos/cobuchi.cc, spot/twaalgos/totgba.cc: Here. --- spot/twaalgos/cobuchi.cc | 51 ++++++++++++++++++++++------------------ spot/twaalgos/totgba.cc | 31 ++++++++++++------------ 2 files changed, 43 insertions(+), 39 deletions(-) diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 2fc3cd3c6..3fb71a99e 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -183,7 +183,7 @@ namespace spot for (auto& e : res_->out(s)) { if (nca_info && e.acc && (si_.scc_of(e.dst) == src_scc - || state_based_)) + || state_based_)) m |= e.acc; e.acc = 0u; } @@ -219,8 +219,8 @@ namespace spot named_states_(named_states), res_(aug_subset_cons(ref_prod, ref_power, named_states_, pmap_)), res_map_(res_->get_named_prop("product-states")), - si_(scc_info(res_, scc_info_options::TRACK_STATES - | scc_info_options::TRACK_SUCCS)), + si_(res_, (scc_info_options::TRACK_STATES + | scc_info_options::TRACK_SUCCS)), nb_states_(res_->num_states()), was_rabin_(was_rabin), orig_num_st_(orig_num_st) @@ -405,7 +405,7 @@ namespace spot { protected: const_twa_graph_ptr aut_; // The given automaton. - vect_nca_info* nca_info_; // Info (cf Header). + vect_nca_info* nca_info_; // Info (cf Header). unsigned nb_copy_; // != 0 if was Rabin. bdd ap_; // All AP. std::vector num2bdd_; // Get bdd from AP num. @@ -474,7 +474,7 @@ namespace spot } } } - debug << "All_states:\n" << *bv_aut_trans_ << std::endl; + debug << "All_states:\n" << *bv_aut_trans_ << '\n'; twa_graph_ptr res = make_twa_graph(aut_->get_dict()); res->copy_ap_of(aut_); @@ -561,12 +561,16 @@ namespace spot bv_trans_mark->at(l) |= bv_aut_trans_->at(s * nc + l); toclean_.push_back(bv_trans_mark); - debug << "src:" << top.second << std::endl; + debug << "src:" << top.second; + if (named_states) + debug << ' ' << (*state_name)[top.second]; + debug << '\n'; + for (unsigned l = 0; l < nc; ++l) { - debug << "l:" - << bdd_format_formula(aut_->get_dict(), num2bdd_[l]) - << '\n'; + debug << "l: " + << bdd_format_formula(aut_->get_dict(), num2bdd_[l]) + << '\n'; auto bv_res = make_bitvect_array(ns, 2); toclean_.push_back(bv_res); @@ -591,8 +595,7 @@ namespace spot (top.first.first + 1) % (nb_copy_ + 1) : top.first.first; - debug << "dest\n" << *bv_res << "i: " << i - << std::endl; + debug << "dest\n" << *bv_res << "i: " << i << '\n'; res->new_edge(top.second, new_state(std::make_pair(i, bv_res)), num2bdd_[l]); @@ -600,15 +603,18 @@ namespace spot debug << '\n'; } - // Set accepting states. + // Set rejecting states. scc_info si(res); bool state_based = (bool)aut_->prop_state_acc(); unsigned res_size = res->num_states(); for (unsigned s = 0; s < res_size; ++s) - if (num_2_bv_[s].second->at(1).is_fully_clear()) - for (auto& edge : res->out(s)) - if (si.scc_of(edge.dst) == si.scc_of(s) || state_based) - edge.acc = acc_cond::mark_t({0}); + { + unsigned s_scc = si.scc_of(s); + if (num_2_bv_[s].second->at(1).is_fully_clear()) + for (auto& edge : res->out(s)) + if (state_based || si.scc_of(edge.dst) == s_scc) + edge.acc = acc_cond::mark_t({0}); + } // Delete all bitvect arrays allocated by this method (run). for (auto v: toclean_) @@ -624,7 +630,7 @@ namespace spot twa_graph_ptr nsa_to_dca(const_twa_graph_ptr aut, bool named_states) { - debug << "NSA_to_dca" << std::endl; + debug << "NSA_to_dca\n"; std::vector pairs; if (!aut->acc().is_streett_like(pairs) && !aut->acc().is_parity()) throw std::runtime_error("nsa_to_dca() only works with Streett-like or " @@ -640,10 +646,10 @@ namespace spot nsa_to_nca(aut, named_states, &nca_info); #if DEBUG - debug << "PRINTING INFO" << std::endl; + debug << "PRINTING INFO\n"; for (unsigned i = 0; i < nca_info.size(); ++i) debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num - << ',' << nca_info[i]->all_dst << '>' << std::endl; + << ',' << *nca_info[i]->all_dst << ">\n"; #endif dca_breakpoint_cons dca(aut, &nca_info, 0); @@ -654,9 +660,8 @@ namespace spot twa_graph_ptr dnf_to_dca(const_twa_graph_ptr aut, bool named_states) { - debug << "DNF_to_dca" << std::endl; + debug << "DNF_to_dca\n"; const acc_cond::acc_code& code = aut->get_acceptance(); - std::vector pairs; if (!code.is_dnf()) throw std::runtime_error("dnf_to_dca() only works with DNF (Rabin-like " "included) acceptance condition"); @@ -671,10 +676,10 @@ namespace spot dnf_to_nca(aut, false, &nca_info); #if DEBUG - debug << "PRINTING INFO" << std::endl; + debug << "PRINTING INFO\n"; for (unsigned i = 0; i < nca_info.size(); ++i) debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num - << ',' << nca_info[i]->all_dst << '>' << std::endl; + << ',' << *nca_info[i]->all_dst << ">\n"; #endif unsigned nb_copy = 0; diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index d3e89977b..af7eb9713 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -126,18 +126,18 @@ namespace spot for (unsigned i = 0; i < all_clauses_.size(); ++i) { debug << i << " Fin:" << all_clauses_[i].first << " Inf:" - << all_clauses_[i].second << std::endl; + << all_clauses_[i].second << '\n'; } #endif } // Compute all the acceptance sets that will be needed: // -Inf(x) will be converted to (Inf(x) | Fin(y)) with y appearing - // on every edge. + // on every edge of the associated clone. // -Fin(x) will be converted to (Inf(y) | Fin(x)) with y appearing // nowhere. - // - // All the previous 'y' are the new sets assigned. + // In the second form, Inf(y) with no occurrence of y, can be + // reused multiple times. It's called "missing_set" below. void assign_new_sets() { @@ -151,7 +151,7 @@ namespace spot { if ((int)missing_set < 0) { - while (all_m & acc_cond::mark_t({next_set})) + while (all_m.has(next_set)) ++next_set; missing_set = next_set++; } @@ -160,13 +160,13 @@ namespace spot } else if (all_inf_.has(set)) { - while (all_m & acc_cond::mark_t({next_set})) + while (all_m.has(next_set)) ++next_set; assigned_sets_[set] = next_set++; } - num_sets_res_ = next_set > max_set_in_ ? next_set : max_set_in_; + num_sets_res_ = std::max(next_set, max_set_in_); } // Precompute: @@ -239,15 +239,15 @@ namespace spot } } #if DEBUG - debug << "accepting clauses" << std::endl; + debug << "accepting clauses\n"; for (unsigned i = 0; i < res.size(); ++i) { debug << "scc(" << i << ") --> "; for (auto elt : res[i]) debug << elt << ','; - debug << std::endl; + debug << '\n' } - debug << std::endl; + debug << '\n'; #endif } @@ -257,7 +257,7 @@ namespace spot void add_state(unsigned st) { - debug << "add_state(" << st << ')' << std::endl; + debug << "add_state(" << st << ")\n"; if (st_repr_[st].empty()) { unsigned st_scc = si_.scc_of(st); @@ -270,7 +270,7 @@ namespace spot else st_repr_[st].emplace_back(-1U, res_->new_state()); - debug << "added" << std::endl; + debug << "added\n"; } } @@ -317,7 +317,7 @@ namespace spot init_st_in_(in->get_init_state_number()), init_reachable_(is_init_reachable()) { - debug << "State based ? " << state_based_ << std::endl; + debug << "State based ? " << state_based_ << '\n'; std::tie(all_inf_, all_fin_) = code.used_inf_fin_sets(); split_dnf_clauses(code); find_set_to_add(); @@ -346,8 +346,7 @@ namespace spot add_state(st); for (const auto& e : in_->out(st)) { - debug << "working_on_edge(" << st << ',' << e.dst << ')' - << std::endl; + debug << "working_on_edge(" << st << ',' << e.dst << ")\n"; unsigned dst_scc = si_.scc_of(e.dst); if (!si_.is_useful_scc(dst_scc)) @@ -368,7 +367,7 @@ namespace spot for (const auto& p_dst : st_repr_[e.dst]) { debug << "repr(" << p_src.second << ',' - << p_dst.second << ')' << std::endl; + << p_dst.second << ")\n"; if (same_scc && p_src.first == p_dst.first) res_->new_edge(p_src.second, p_dst.second, e.cond,