From 47d9a2d57c176e32055a0002e77150505cf5e536 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 18 Mar 2015 20:27:37 +0100 Subject: [PATCH] rename set_single_acceptance_set() to set_buchi() Fixes #66. * src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc, src/hoaparse/hoaparse.yy, src/tgba/tgbagraph.hh, src/tgbaalgos/complete.cc, src/tgbaalgos/degen.cc, src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/minimize.cc, src/tgbaalgos/postproc.cc: Here. --- src/dstarparse/dra2ba.cc | 2 +- src/dstarparse/nra2nba.cc | 2 +- src/hoaparse/hoaparse.yy | 2 +- src/tgba/tgbagraph.hh | 2 +- src/tgbaalgos/complete.cc | 2 +- src/tgbaalgos/degen.cc | 2 +- src/tgbaalgos/dtbasat.cc | 2 +- src/tgbaalgos/dtgbacomp.cc | 4 ++-- src/tgbaalgos/minimize.cc | 2 +- src/tgbaalgos/postproc.cc | 2 +- 10 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index 7bd241844..effc454c7 100644 --- a/src/dstarparse/dra2ba.cc +++ b/src/dstarparse/dra2ba.cc @@ -225,7 +225,7 @@ namespace spot { out_->copy_ap_of(a->aut); out_->prop_state_based_acc(); - acc_ = out_->set_single_acceptance_set(); + acc_ = out_->set_buchi(); out_->new_states(num_states_ * (a->accpair_count + 1)); out_->set_init_state(a->aut->get_init_state_number()); diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc index 37796bbd4..fa1900866 100644 --- a/src/dstarparse/nra2nba.cc +++ b/src/dstarparse/nra2nba.cc @@ -45,7 +45,7 @@ namespace spot num_states_(a->aut->num_states()) { out_->copy_ap_of(aut); - out_->set_single_acceptance_set(); + out_->set_buchi(); out_->prop_state_based_acc(); out_->new_states(num_states_ * (d_->accpair_count + 1)); // This converts the initial state of aut (not a->aut) into a diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index ed1bbb663..2f356214f 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -1042,7 +1042,7 @@ incorrectly-labeled-edge: trans-label unlabeled-edge /**********************************************************************/ never: "never" { res.namer = res.h->aut->create_namer(); - res.h->aut->set_single_acceptance_set(); + res.h->aut->set_buchi(); res.h->aut->prop_state_based_acc(); res.acc_state = State_Acc; res.pos_acc_sets = res.h->aut->acc().all_sets(); diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 510720008..4c00b9108 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -348,7 +348,7 @@ namespace spot acc_.set_generalized_buchi(); } - acc_cond::mark_t set_single_acceptance_set() + acc_cond::mark_t set_buchi() { set_generalized_buchi(1); return acc_.mark(0); diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc index e8d302e29..4802ae6e4 100644 --- a/src/tgbaalgos/complete.cc +++ b/src/tgbaalgos/complete.cc @@ -31,7 +31,7 @@ namespace spot // We cannot safely complete an automaton if it has no // acceptance set as the added sink would become accepting. // In this case, add an acceptance set to all transitions. - allacc = aut->set_single_acceptance_set(); + allacc = aut->set_buchi(); for (auto& t: aut->transition_vector()) t.acc = allacc; } diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index e52013c85..5ebe9dfbc 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -201,7 +201,7 @@ namespace spot // The result automaton is an SBA. auto res = make_tgba_digraph(dict); res->copy_ap_of(a); - res->set_single_acceptance_set(); + res->set_buchi(); if (want_sba) res->prop_state_based_acc(); // Preserve determinism, weakness, and stutter-invariance diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index cb47abaa9..9dcc87e3a 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -638,7 +638,7 @@ namespace spot auto autdict = aut->get_dict(); auto a = make_tgba_digraph(autdict); a->copy_ap_of(aut); - acc_cond::mark_t acc = a->set_single_acceptance_set(); + acc_cond::mark_t acc = a->set_buchi(); if (state_based) a->prop_state_based_acc(); a->new_states(satdict.cand_size); diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc index f4bd3f08f..1a05bc0fc 100644 --- a/src/tgbaalgos/dtgbacomp.cc +++ b/src/tgbaalgos/dtgbacomp.cc @@ -40,7 +40,7 @@ namespace spot // We will modify res in place, and the resulting // automaton will only have one acceptance set. // This changes aut->acc(); - res->set_single_acceptance_set(); + res->set_buchi(); // The resulting automaton is weak. res->prop_inherently_weak(); res->prop_state_based_acc(); @@ -127,7 +127,7 @@ namespace spot // We will modify res in place, and the resulting // automaton will only have one acceptance set. - acc_cond::mark_t all_acc = res->set_single_acceptance_set(); + acc_cond::mark_t all_acc = res->set_buchi(); res->prop_state_based_acc(); unsigned sink = res->num_states(); diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 07d32c334..69d5d7bd4 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -141,7 +141,7 @@ namespace spot // transition in res. if (!final->empty()) - res->set_single_acceptance_set(); + res->set_buchi(); for (sit = sets.begin(); sit != sets.end(); ++sit) { diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index c9fec4684..b608998a3 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -40,7 +40,7 @@ namespace spot { if (a->acc().num_sets() == 0) { - auto m = a->set_single_acceptance_set(); + auto m = a->set_buchi(); for (auto& t: a->transitions()) t.acc = m; }