diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index cbf7c91f9..ed1bbb663 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -1249,7 +1249,7 @@ lbtt: lbtt-header lbtt-body ENDAUT { auto& acc = res.h->aut->acc(); unsigned num = acc.num_sets(); - res.h->aut->set_acceptance_conditions(num); + res.h->aut->set_generalized_buchi(num); res.pos_acc_sets = acc.all_sets(); assert(!res.states_map.empty()); auto n = res.states_map.size(); @@ -1284,7 +1284,7 @@ lbtt: lbtt-header lbtt-body ENDAUT } | lbtt-header-states LBTT_EMPTY { - res.h->aut->set_acceptance_conditions($2); + res.h->aut->set_generalized_buchi($2); res.pos_acc_sets = res.h->aut->acc().all_sets(); } diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index fb92326b1..ffd1561c7 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -639,8 +639,10 @@ namespace spot acc_cond acc_; public: - auto get_acceptance() const - SPOT_RETURN(acc_.get_acceptance()); + acc_cond::acc_code get_acceptance() const + { + return acc_.get_acceptance(); + } void set_acceptance(unsigned num, const acc_cond::acc_code& c) { diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index b22fa10f4..607d91f8c 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -334,8 +334,7 @@ namespace spot return g_.trans_data(t); } - // FIXME: Should be renamed as set_generalized_buchi() - void set_acceptance_conditions(unsigned num) + void set_generalized_buchi(unsigned num) { if (num < acc_.num_sets()) { @@ -351,7 +350,7 @@ namespace spot acc_cond::mark_t set_single_acceptance_set() { - set_acceptance_conditions(1); + set_generalized_buchi(1); return acc_.mark(0); } @@ -378,7 +377,7 @@ namespace spot return g_.trans_storage(t); } - void set_acceptance_conditions(bdd all); + void set_generalized_buchi(bdd all); unsigned new_state() { diff --git a/src/tgbaalgos/compsusp.cc b/src/tgbaalgos/compsusp.cc index 06f17c728..a60ccac8c 100644 --- a/src/tgbaalgos/compsusp.cc +++ b/src/tgbaalgos/compsusp.cc @@ -226,7 +226,7 @@ namespace spot const acc_cond& la = left->acc(); const acc_cond& ra = right->acc(); - res->set_acceptance_conditions(la.num_sets() + ra.num_sets()); + res->set_generalized_buchi(la.num_sets() + ra.num_sets()); acc_cond::mark_t radd = ra.all_sets(); diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index 26167dcbd..dbfc0c661 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -779,7 +779,7 @@ namespace spot auto autdict = aut->get_dict(); auto a = make_tgba_digraph(autdict); a->copy_ap_of(aut); - a->set_acceptance_conditions(satdict.cand_nacc); + a->set_generalized_buchi(satdict.cand_nacc); a->new_states(satdict.cand_size); diff --git a/src/tgbaalgos/mask.cc b/src/tgbaalgos/mask.cc index 9a82a364e..3967130d4 100644 --- a/src/tgbaalgos/mask.cc +++ b/src/tgbaalgos/mask.cc @@ -31,7 +31,7 @@ namespace spot unsigned na = inacc.num_sets(); unsigned tr = to_remove.count(); assert(tr <= na); - res->set_acceptance_conditions(na - tr); + res->set_generalized_buchi(na - tr); transform_accessible(in, res, [&](unsigned, bdd& cond, acc_cond::mark_t& acc, diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index 898e5b8ec..52fafff6a 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -134,7 +134,7 @@ namespace spot for (auto i: *ap) props[pi++] = dict->register_proposition(i, res); - res->set_acceptance_conditions(n_accs); + res->set_generalized_buchi(n_accs); // Using std::unordered_set instead of std::set for these sets is 3 // times slower (tested on a 50000 nodes example). diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 5340bab7b..fb2b5015f 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -275,7 +275,7 @@ namespace spot inout.push_back(-1U); filtered-> - set_acceptance_conditions(filter.accsets(aut->acc().num_sets())); + set_generalized_buchi(filter.accsets(aut->acc().num_sets())); filtered->new_states(out_n); for (unsigned isrc = 0; isrc < in_n; ++isrc) { diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 69bd2e89f..2b7714828 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -628,7 +628,7 @@ namespace spot delete gb; res->prop_copy(original_, { false, // state-based acc forced below - false, // single acc set by set_acceptance_conditions + false, // single acc set by set_generalized_buchi true, // weakness preserved, false, // determinism checked and set below }); diff --git a/src/tgbaalgos/stripacc.cc b/src/tgbaalgos/stripacc.cc index 2225a82f1..841e3d275 100644 --- a/src/tgbaalgos/stripacc.cc +++ b/src/tgbaalgos/stripacc.cc @@ -28,6 +28,6 @@ namespace spot for (unsigned s = 0; s < n; ++s) for (auto& t: a->out(s)) t.acc = 0U; - a->set_acceptance_conditions(0); + a->set_generalized_buchi(0); } }