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.
This commit is contained in:
parent
2dbef514bd
commit
47d9a2d57c
10 changed files with 11 additions and 11 deletions
|
|
@ -225,7 +225,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
out_->copy_ap_of(a->aut);
|
out_->copy_ap_of(a->aut);
|
||||||
out_->prop_state_based_acc();
|
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_->new_states(num_states_ * (a->accpair_count + 1));
|
||||||
out_->set_init_state(a->aut->get_init_state_number());
|
out_->set_init_state(a->aut->get_init_state_number());
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -45,7 +45,7 @@ namespace spot
|
||||||
num_states_(a->aut->num_states())
|
num_states_(a->aut->num_states())
|
||||||
{
|
{
|
||||||
out_->copy_ap_of(aut);
|
out_->copy_ap_of(aut);
|
||||||
out_->set_single_acceptance_set();
|
out_->set_buchi();
|
||||||
out_->prop_state_based_acc();
|
out_->prop_state_based_acc();
|
||||||
out_->new_states(num_states_ * (d_->accpair_count + 1));
|
out_->new_states(num_states_ * (d_->accpair_count + 1));
|
||||||
// This converts the initial state of aut (not a->aut) into a
|
// This converts the initial state of aut (not a->aut) into a
|
||||||
|
|
|
||||||
|
|
@ -1042,7 +1042,7 @@ incorrectly-labeled-edge: trans-label unlabeled-edge
|
||||||
/**********************************************************************/
|
/**********************************************************************/
|
||||||
|
|
||||||
never: "never" { res.namer = res.h->aut->create_namer<std::string>();
|
never: "never" { res.namer = res.h->aut->create_namer<std::string>();
|
||||||
res.h->aut->set_single_acceptance_set();
|
res.h->aut->set_buchi();
|
||||||
res.h->aut->prop_state_based_acc();
|
res.h->aut->prop_state_based_acc();
|
||||||
res.acc_state = State_Acc;
|
res.acc_state = State_Acc;
|
||||||
res.pos_acc_sets = res.h->aut->acc().all_sets();
|
res.pos_acc_sets = res.h->aut->acc().all_sets();
|
||||||
|
|
|
||||||
|
|
@ -348,7 +348,7 @@ namespace spot
|
||||||
acc_.set_generalized_buchi();
|
acc_.set_generalized_buchi();
|
||||||
}
|
}
|
||||||
|
|
||||||
acc_cond::mark_t set_single_acceptance_set()
|
acc_cond::mark_t set_buchi()
|
||||||
{
|
{
|
||||||
set_generalized_buchi(1);
|
set_generalized_buchi(1);
|
||||||
return acc_.mark(0);
|
return acc_.mark(0);
|
||||||
|
|
|
||||||
|
|
@ -31,7 +31,7 @@ namespace spot
|
||||||
// We cannot safely complete an automaton if it has no
|
// We cannot safely complete an automaton if it has no
|
||||||
// acceptance set as the added sink would become accepting.
|
// acceptance set as the added sink would become accepting.
|
||||||
// In this case, add an acceptance set to all transitions.
|
// 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())
|
for (auto& t: aut->transition_vector())
|
||||||
t.acc = allacc;
|
t.acc = allacc;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -201,7 +201,7 @@ namespace spot
|
||||||
// The result automaton is an SBA.
|
// The result automaton is an SBA.
|
||||||
auto res = make_tgba_digraph(dict);
|
auto res = make_tgba_digraph(dict);
|
||||||
res->copy_ap_of(a);
|
res->copy_ap_of(a);
|
||||||
res->set_single_acceptance_set();
|
res->set_buchi();
|
||||||
if (want_sba)
|
if (want_sba)
|
||||||
res->prop_state_based_acc();
|
res->prop_state_based_acc();
|
||||||
// Preserve determinism, weakness, and stutter-invariance
|
// Preserve determinism, weakness, and stutter-invariance
|
||||||
|
|
|
||||||
|
|
@ -638,7 +638,7 @@ namespace spot
|
||||||
auto autdict = aut->get_dict();
|
auto autdict = aut->get_dict();
|
||||||
auto a = make_tgba_digraph(autdict);
|
auto a = make_tgba_digraph(autdict);
|
||||||
a->copy_ap_of(aut);
|
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)
|
if (state_based)
|
||||||
a->prop_state_based_acc();
|
a->prop_state_based_acc();
|
||||||
a->new_states(satdict.cand_size);
|
a->new_states(satdict.cand_size);
|
||||||
|
|
|
||||||
|
|
@ -40,7 +40,7 @@ namespace spot
|
||||||
// We will modify res in place, and the resulting
|
// We will modify res in place, and the resulting
|
||||||
// automaton will only have one acceptance set.
|
// automaton will only have one acceptance set.
|
||||||
// This changes aut->acc();
|
// This changes aut->acc();
|
||||||
res->set_single_acceptance_set();
|
res->set_buchi();
|
||||||
// The resulting automaton is weak.
|
// The resulting automaton is weak.
|
||||||
res->prop_inherently_weak();
|
res->prop_inherently_weak();
|
||||||
res->prop_state_based_acc();
|
res->prop_state_based_acc();
|
||||||
|
|
@ -127,7 +127,7 @@ namespace spot
|
||||||
|
|
||||||
// We will modify res in place, and the resulting
|
// We will modify res in place, and the resulting
|
||||||
// automaton will only have one acceptance set.
|
// 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();
|
res->prop_state_based_acc();
|
||||||
|
|
||||||
unsigned sink = res->num_states();
|
unsigned sink = res->num_states();
|
||||||
|
|
|
||||||
|
|
@ -141,7 +141,7 @@ namespace spot
|
||||||
// transition in res.
|
// transition in res.
|
||||||
|
|
||||||
if (!final->empty())
|
if (!final->empty())
|
||||||
res->set_single_acceptance_set();
|
res->set_buchi();
|
||||||
|
|
||||||
for (sit = sets.begin(); sit != sets.end(); ++sit)
|
for (sit = sets.begin(); sit != sets.end(); ++sit)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -40,7 +40,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
if (a->acc().num_sets() == 0)
|
if (a->acc().num_sets() == 0)
|
||||||
{
|
{
|
||||||
auto m = a->set_single_acceptance_set();
|
auto m = a->set_buchi();
|
||||||
for (auto& t: a->transitions())
|
for (auto& t: a->transitions())
|
||||||
t.acc = m;
|
t.acc = m;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue