diff --git a/src/twa/twa.hh b/src/twa/twa.hh index 18492cb94..1d5956e25 100644 --- a/src/twa/twa.hh +++ b/src/twa/twa.hh @@ -658,6 +658,11 @@ namespace spot } public: + unsigned num_sets() const + { + return acc_.num_sets(); + } + const acc_cond::acc_code& get_acceptance() const { return acc_.get_acceptance(); diff --git a/src/twa/twagraph.hh b/src/twa/twagraph.hh index 5ad66f5c4..ed3d43a49 100644 --- a/src/twa/twagraph.hh +++ b/src/twa/twagraph.hh @@ -438,7 +438,7 @@ namespace spot acc_cond::mark_t state_acc_sets(unsigned s) const { - assert(has_state_based_acc() || acc_.num_sets() == 0); + assert(has_state_based_acc() || num_sets() == 0); for (auto& t: g_.out(s)) // Stop at the first transition, since the remaining should be // labeled identically. @@ -448,7 +448,7 @@ namespace spot bool state_is_accepting(unsigned s) const { - assert(has_state_based_acc() || acc_.num_sets() == 0); + assert(has_state_based_acc() || num_sets() == 0); for (auto& t: g_.out(s)) // Stop at the first transition, since the remaining should be // labeled identically. @@ -465,7 +465,7 @@ namespace spot { if (num_states() != aut.num_states() || num_transitions() != aut.num_transitions() || - acc().num_sets() != aut.acc().num_sets()) + num_sets() != aut.num_sets()) return false; auto& trans1 = transition_vector(); auto& trans2 = aut.transition_vector(); diff --git a/src/twa/twaproduct.cc b/src/twa/twaproduct.cc index 5de3c44ef..949a2465f 100644 --- a/src/twa/twaproduct.cc +++ b/src/twa/twaproduct.cc @@ -310,12 +310,12 @@ namespace spot d->register_all_propositions_of(&left_, this); d->register_all_propositions_of(&right_, this); - assert(acc_.num_sets() == 0); - auto left_num = left->acc().num_sets(); + assert(num_sets() == 0); + auto left_num = left->num_sets(); auto right_acc = right->get_acceptance(); right_acc.shift_left(left_num); right_acc.append_and(left->get_acceptance()); - set_acceptance(left_num + right->acc().num_sets(), right_acc); + set_acceptance(left_num + right->num_sets(), right_acc); } twa_product::~twa_product() diff --git a/src/twa/twaproxy.cc b/src/twa/twaproxy.cc index d24001156..21f2ae4ca 100644 --- a/src/twa/twaproxy.cc +++ b/src/twa/twaproxy.cc @@ -25,7 +25,7 @@ namespace spot : twa(original->get_dict()), original_(original) { get_dict()->register_all_variables_of(original, this); - acc_.add_sets(original->acc().num_sets()); + acc_.add_sets(original->num_sets()); } twa_proxy::~twa_proxy() diff --git a/src/twaalgos/degen.cc b/src/twaalgos/degen.cc index 518d82ac2..d4e5b2371 100644 --- a/src/twaalgos/degen.cc +++ b/src/twaalgos/degen.cc @@ -226,7 +226,7 @@ namespace spot // used in the automaton. (This surprising fact is probably // related to the order in which we declare the BDD variables // during the translation.) - unsigned n = a->acc().num_sets(); + unsigned n = a->num_sets(); for (unsigned i = n; i > 0; --i) order.push_back(i - 1); } diff --git a/src/twaalgos/dot.cc b/src/twaalgos/dot.cc index 15e2ee4bf..8f4ee374c 100644 --- a/src/twaalgos/dot.cc +++ b/src/twaalgos/dot.cc @@ -277,7 +277,7 @@ namespace spot if (opt_html_labels_) std::tie(inf_sets_, fin_sets_) = aut_->get_acceptance().used_inf_fin_sets(); - if (opt_bullet && aut_->acc().num_sets() <= MAX_BULLET) + if (opt_bullet && aut_->num_sets() <= MAX_BULLET) opt_all_bullets = true; os_ << "digraph G {\n"; if (opt_horizontal_) @@ -366,7 +366,7 @@ namespace spot { if (mark_states_ && ((opt_bullet && !opt_bullet_but_buchi) - || aut_->acc().num_sets() != 1)) + || aut_->num_sets() != 1)) { acc_cond::mark_t acc = 0U; for (auto& t: aut_->out(s)) diff --git a/src/twaalgos/dtgbacomp.cc b/src/twaalgos/dtgbacomp.cc index 6555804f4..afe41dfca 100644 --- a/src/twaalgos/dtgbacomp.cc +++ b/src/twaalgos/dtgbacomp.cc @@ -174,7 +174,7 @@ namespace spot // Simply complete the automaton, and complement its // acceptance. auto res = cleanup_acceptance_here(tgba_complete(aut)); - res->set_acceptance(res->acc().num_sets(), + res->set_acceptance(res->num_sets(), res->get_acceptance().complement()); return res; } diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc index 67a930164..81096dea9 100644 --- a/src/twaalgos/dtgbasat.cc +++ b/src/twaalgos/dtgbasat.cc @@ -472,7 +472,7 @@ namespace spot } d.all_ref_acc.push_back(0U); - unsigned ref_nacc = aut->acc().num_sets(); + unsigned ref_nacc = aut->num_sets(); for (unsigned n = 0; n < ref_nacc; ++n) { auto c = aut->acc().mark(n); @@ -1233,7 +1233,7 @@ namespace spot // Assume we are going to use the input automaton acceptance... bool user_supplied_acc = false; acc_cond::acc_code target_acc = a->get_acceptance(); - int nacc = a->acc().num_sets(); + int nacc = a->num_sets(); if (accstr == "same") accstr.clear(); diff --git a/src/twaalgos/gv04.cc b/src/twaalgos/gv04.cc index b16f0d037..6c394b1b1 100644 --- a/src/twaalgos/gv04.cc +++ b/src/twaalgos/gv04.cc @@ -70,7 +70,7 @@ namespace spot gv04(const const_twa_ptr& a, option_map o) : emptiness_check(a, o) { - assert(a->acc().num_sets() <= 1); + assert(a->num_sets() <= 1); } ~gv04() @@ -383,7 +383,7 @@ namespace spot const state* bfs_start = data.stack[scc_root].s; const state* bfs_end = bfs_start; - if (a_->acc().num_sets() > 0) + if (a_->num_sets() > 0) { first_bfs b1(this, scc_root); bfs_start = b1.search(bfs_start, res->cycle); diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc index b03b0c722..39d511563 100644 --- a/src/twaalgos/hoa.cc +++ b/src/twaalgos/hoa.cc @@ -97,7 +97,7 @@ namespace spot bool complete = true; bool state_acc = true; bool nodeadend = true; - bool colored = aut->acc().num_sets() >= 1; + bool colored = aut->num_sets() >= 1; for (unsigned src = 0; src < ns; ++src) { bdd sum = bddfalse; @@ -296,7 +296,7 @@ namespace spot } os << nl; - unsigned num_acc = aut->acc().num_sets(); + unsigned num_acc = aut->num_sets(); acc_cond::acc_code acc_c = aut->acc().get_acceptance(); if (aut->acc().is_generalized_buchi()) { diff --git a/src/twaalgos/lbtt.cc b/src/twaalgos/lbtt.cc index 1366ce8f5..9eb069c2b 100644 --- a/src/twaalgos/lbtt.cc +++ b/src/twaalgos/lbtt.cc @@ -115,9 +115,9 @@ namespace spot { os_ << seen.size() << ' '; if (sba_format_) - os_ << aut_->acc().num_sets(); + os_ << aut_->num_sets(); else - os_ << aut_->acc().num_sets() << 't'; + os_ << aut_->num_sets() << 't'; os_ << '\n' << body_.str() << "-1" << std::endl; } diff --git a/src/twaalgos/magic.cc b/src/twaalgos/magic.cc index 5d6555b4a..0e4981dd2 100644 --- a/src/twaalgos/magic.cc +++ b/src/twaalgos/magic.cc @@ -59,7 +59,7 @@ namespace spot : emptiness_check(a, o), h(size) { - assert(a->acc().num_sets() <= 1); + assert(a->num_sets() <= 1); } virtual ~magic_search_() diff --git a/src/twaalgos/mask.cc b/src/twaalgos/mask.cc index eb3675728..7fa799a97 100644 --- a/src/twaalgos/mask.cc +++ b/src/twaalgos/mask.cc @@ -27,7 +27,7 @@ namespace spot auto res = make_twa_graph(in->get_dict()); res->copy_ap_of(in); res->prop_copy(in, { true, true, true, false }); - unsigned na = in->acc().num_sets(); + unsigned na = in->num_sets(); unsigned tr = to_remove.count(); assert(tr <= na); res->set_acceptance(na - tr, diff --git a/src/twaalgos/ndfs_result.hxx b/src/twaalgos/ndfs_result.hxx index 315f398e0..4c272a826 100644 --- a/src/twaalgos/ndfs_result.hxx +++ b/src/twaalgos/ndfs_result.hxx @@ -119,7 +119,7 @@ namespace spot start = stb.front().s->clone(); if (!str.empty()) { - if (a_->acc().num_sets() == 0) + if (a_->num_sets() == 0) { // take arbitrarily the last transition on the red stack stack_type::const_iterator i, j; diff --git a/src/twaalgos/postproc.cc b/src/twaalgos/postproc.cc index ff96d3be1..5e8047ee0 100644 --- a/src/twaalgos/postproc.cc +++ b/src/twaalgos/postproc.cc @@ -41,7 +41,7 @@ namespace spot static twa_graph_ptr ensure_ba(twa_graph_ptr& a) { - if (a->acc().num_sets() == 0) + if (a->num_sets() == 0) { auto m = a->set_buchi(); for (auto& t: a->transitions()) @@ -153,7 +153,7 @@ namespace spot if (type_ == Generic || type_ == TGBA || (type_ == BA && a->is_sba()) - || (type_ == Monitor && a->acc().num_sets() == 0)) + || (type_ == Monitor && a->num_sets() == 0)) { if (COMP_) a = tgba_complete(a); @@ -171,7 +171,7 @@ namespace spot if (type_ == BA || SBACC_) state_based_ = true; - int original_acc = a->acc().num_sets(); + int original_acc = a->num_sets(); // Remove useless SCCs. if (type_ == Monitor) @@ -301,7 +301,7 @@ namespace spot if (PREF_ == Deterministic && f && f->is_syntactic_recurrence() - && sim->acc().num_sets() > 1) + && sim->num_sets() > 1) tmpd = degeneralize_tba(sim); auto in = tmpd ? tmpd : sim; @@ -370,7 +370,7 @@ namespace spot // because the input TBA might be smaller. if (state_based_) in = degeneralize(dba); - else if (dba->acc().num_sets() != 1) + else if (dba->num_sets() != 1) in = degeneralize_tba(dba); else in = dba; @@ -423,7 +423,7 @@ namespace spot // Degeneralize the dba resulting from tba-determinization or // sat-minimization (which is a TBA) if requested and needed. if (dba && !dba_is_wdba && type_ == BA - && !(dba_is_minimal && state_based_ && dba->acc().num_sets() == 1)) + && !(dba_is_minimal && state_based_ && dba->num_sets() == 1)) dba = degeneralize(dba); if (dba && sim) diff --git a/src/twaalgos/powerset.cc b/src/twaalgos/powerset.cc index 52daabbe6..ea66f3e84 100644 --- a/src/twaalgos/powerset.cc +++ b/src/twaalgos/powerset.cc @@ -410,7 +410,7 @@ namespace spot { if (f == 0 && neg_aut == 0) return 0; - if (aut->acc().num_sets() > 1) + if (aut->num_sets() > 1) return 0; auto det = tba_determinize(aut, threshold_states, threshold_cycles); diff --git a/src/twaalgos/product.cc b/src/twaalgos/product.cc index d21d91f24..b4e1b6a01 100644 --- a/src/twaalgos/product.cc +++ b/src/twaalgos/product.cc @@ -52,11 +52,11 @@ namespace spot auto res = make_twa_graph(left->get_dict()); res->copy_ap_of(left); res->copy_ap_of(right); - auto left_num = left->acc().num_sets(); + auto left_num = left->num_sets(); auto right_acc = right->get_acceptance(); right_acc.shift_left(left_num); right_acc.append_and(left->get_acceptance()); - res->set_acceptance(left_num + right->acc().num_sets(), right_acc); + res->set_acceptance(left_num + right->num_sets(), right_acc); auto v = new product_states; res->set_named_prop("product-states", v); diff --git a/src/twaalgos/remfin.cc b/src/twaalgos/remfin.cc index fe660399a..d84b5b9d9 100644 --- a/src/twaalgos/remfin.cc +++ b/src/twaalgos/remfin.cc @@ -264,7 +264,7 @@ namespace spot res->copy_ap_of(aut); res->prop_copy(aut, { false, false, false, true }); res->new_states(nst); - res->set_acceptance(aut->acc().num_sets() + extra_sets, new_code); + res->set_acceptance(aut->num_sets() + extra_sets, new_code); res->set_init_state(aut->get_init_state_number()); unsigned nscc = si.scc_count(); diff --git a/src/twaalgos/se05.cc b/src/twaalgos/se05.cc index 9659c2e60..ec16d4ffa 100644 --- a/src/twaalgos/se05.cc +++ b/src/twaalgos/se05.cc @@ -59,7 +59,7 @@ namespace spot : emptiness_check(a, o), h(size) { - assert(a->acc().num_sets() <= 1); + assert(a->num_sets() <= 1); } virtual ~se05_search() diff --git a/src/twaalgos/simulation.cc b/src/twaalgos/simulation.cc index 42bf1f3e1..1a04f5147 100644 --- a/src/twaalgos/simulation.cc +++ b/src/twaalgos/simulation.cc @@ -258,7 +258,7 @@ namespace spot unsigned set_num = a_->get_dict() ->register_anonymous_variables(size_a_ + 1, this); - unsigned n_acc = a_->acc().num_sets(); + unsigned n_acc = a_->num_sets(); acc_vars = a_->get_dict() ->register_anonymous_variables(n_acc, this); diff --git a/src/twaalgos/stats.cc b/src/twaalgos/stats.cc index 12d211676..f516f3937 100644 --- a/src/twaalgos/stats.cc +++ b/src/twaalgos/stats.cc @@ -183,7 +183,7 @@ namespace spot } if (has('a')) - acc_ = aut->acc().num_sets(); + acc_ = aut->num_sets(); if (has('c') || has('S')) scc_ = scc_info(aut).scc_count(); diff --git a/src/twaalgos/stutter.cc b/src/twaalgos/stutter.cc index 985f55196..e6179e620 100644 --- a/src/twaalgos/stutter.cc +++ b/src/twaalgos/stutter.cc @@ -213,7 +213,7 @@ namespace spot { get_dict()->register_all_propositions_of(&a_, this); assert(acc_.num_sets() == 0); - acc_.add_sets(a_->acc().num_sets()); + acc_.add_sets(a_->num_sets()); acc_.set_generalized_buchi(); } diff --git a/src/twaalgos/tau03.cc b/src/twaalgos/tau03.cc index d499d2227..531e41793 100644 --- a/src/twaalgos/tau03.cc +++ b/src/twaalgos/tau03.cc @@ -58,7 +58,7 @@ namespace spot : emptiness_check(a, o), h(size) { - assert(a->acc().num_sets() > 0); + assert(a->num_sets() > 0); } virtual ~tau03_search() diff --git a/src/twaalgos/tau03opt.cc b/src/twaalgos/tau03opt.cc index a6187e11e..14f687327 100644 --- a/src/twaalgos/tau03opt.cc +++ b/src/twaalgos/tau03opt.cc @@ -159,7 +159,7 @@ namespace spot return acc; // FIXME: This should be improved. std::vector res; - unsigned max = a_->acc().num_sets(); + unsigned max = a_->num_sets(); for (unsigned n = 0; n < max && a_->acc().has(acc, n); ++n) res.push_back(n); return a_->acc().marks(res.begin(), res.end()); diff --git a/src/twaalgos/totgba.cc b/src/twaalgos/totgba.cc index 8bf320b94..2f1e412b3 100644 --- a/src/twaalgos/totgba.cc +++ b/src/twaalgos/totgba.cc @@ -70,7 +70,7 @@ namespace spot if (cnf.empty() || (cnf.size() == 2 && cnf.back().op == acc_cond::acc_op::Inf)) { - res->set_acceptance(res->acc().num_sets(), cnf); + res->set_acceptance(res->num_sets(), cnf); cleanup_acceptance_here(res); return res; }