diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 69b2f55e2..ae7359b99 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -658,7 +658,6 @@ namespace spot { set_num_sets_(num); acc_.set_acceptance(c); - prop_single_acc_set(!acc_.uses_fin_acceptance() && num == 1); if (num == 0) prop_state_based_acc(); } @@ -668,7 +667,6 @@ namespace spot { acc_ = a->acc(); unsigned num = acc_.num_sets(); - prop_single_acc_set(!acc_.uses_fin_acceptance() && num == 1); if (num == 0) prop_state_based_acc(); } @@ -682,7 +680,6 @@ namespace spot { set_num_sets_(num); acc_.set_generalized_buchi(); - prop_single_acc_set(num == 1); if (num == 0) prop_state_based_acc(); } @@ -706,7 +703,6 @@ namespace spot // holds, but false means the property is unknown. struct bprop { - bool single_acc_set:1; // A single acceptance set. bool state_based_acc:1; // State-based acceptance. bool inherently_weak:1; // Weak automaton. bool deterministic:1; // Deterministic automaton. @@ -748,16 +744,6 @@ namespace spot } #endif - bool has_single_acc_set() const - { - return is.single_acc_set; - } - - void prop_single_acc_set(bool val = true) - { - is.single_acc_set = val; - } - bool has_state_based_acc() const { return is.state_based_acc; @@ -770,7 +756,7 @@ namespace spot bool is_sba() const { - return has_state_based_acc() && has_single_acc_set(); + return has_state_based_acc() && acc().is_buchi(); } bool is_inherently_weak() const @@ -806,14 +792,13 @@ namespace spot struct prop_set { bool state_based; - bool single_acc; bool inherently_weak; bool deterministic; bool stutter_inv; static prop_set all() { - return { true, true, true, true, true }; + return { true, true, true, true }; } }; @@ -823,8 +808,6 @@ namespace spot { if (p.state_based) prop_state_based_acc(other->has_state_based_acc()); - if (p.single_acc) - prop_single_acc_set(other->has_single_acc_set()); if (p.inherently_weak) prop_inherently_weak(other->is_inherently_weak()); if (p.deterministic) @@ -837,8 +820,6 @@ namespace spot { if (!p.state_based) prop_state_based_acc(false); - if (!p.single_acc) - prop_single_acc_set(false); if (!p.inherently_weak) prop_inherently_weak(false); if (!p.deterministic) diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc index 4802ae6e4..c5d56cfbe 100644 --- a/src/tgbaalgos/complete.cc +++ b/src/tgbaalgos/complete.cc @@ -106,7 +106,6 @@ namespace spot { auto res = make_tgba_digraph(aut, { true, // state based - true, // single acc true, // inherently_weak true, // deterministic true, // stutter inv. diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index 5ebe9dfbc..7a0271171 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -205,7 +205,7 @@ namespace spot if (want_sba) res->prop_state_based_acc(); // Preserve determinism, weakness, and stutter-invariance - res->prop_copy(a, { false, false, true, true, true }); + res->prop_copy(a, { false, true, true, true }); // Create an order of acceptance conditions. Each entry in this // vector correspond to an acceptance set. Each index can @@ -567,7 +567,7 @@ namespace spot { // If this already a degeneralized digraph, there is nothing we // can improve. - if (a->has_single_acc_set()) + if (a->acc().is_buchi()) return std::const_pointer_cast(a); return degeneralize_aux(a, use_z_lvl, use_cust_acc_orders, diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc index 1a05bc0fc..2069cd29e 100644 --- a/src/tgbaalgos/dtgbacomp.cc +++ b/src/tgbaalgos/dtgbacomp.cc @@ -29,7 +29,6 @@ namespace spot // Clone the original automaton. auto res = make_tgba_digraph(aut, { false, // state based - false, // single acc false, // inherently_weak false, // deterministic true, // stutter inv. @@ -118,7 +117,6 @@ namespace spot // Clone the original automaton. auto res = make_tgba_digraph(aut, { true, // state based - true, // single acc true, // inherently weak true, // determinisitic true, // stutter inv. diff --git a/src/tgbaalgos/mask.cc b/src/tgbaalgos/mask.cc index e431745ac..4218bf04a 100644 --- a/src/tgbaalgos/mask.cc +++ b/src/tgbaalgos/mask.cc @@ -26,7 +26,7 @@ namespace spot { auto res = make_tgba_digraph(in->get_dict()); res->copy_ap_of(in); - res->prop_copy(in, { true, false, true, true, false }); + res->prop_copy(in, { true, true, true, false }); unsigned na = in->acc().num_sets(); unsigned tr = to_remove.count(); assert(tr <= na); @@ -54,7 +54,7 @@ namespace spot auto res = make_tgba_digraph(in->get_dict()); res->copy_ap_of(in); - res->prop_copy(in, { true, true, true, true, false }); + res->prop_copy(in, { true, true, true, false }); res->copy_acceptance_of(in); transform_copy(in, res, [&](unsigned src, bdd& cond, diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 69d5d7bd4..87903faf1 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -485,7 +485,7 @@ namespace spot // final is empty: there is no acceptance condition build_state_set(det_a, non_final); auto res = minimize_dfa(det_a, final, non_final); - res->prop_copy(a, { false, false, false, false, true }); + res->prop_copy(a, { false, false, false, true }); res->prop_deterministic(); res->prop_inherently_weak(); res->prop_state_based_acc(); @@ -589,7 +589,7 @@ namespace spot } auto res = minimize_dfa(det_a, final, non_final); - res->prop_copy(a, { false, false, false, false, true }); + res->prop_copy(a, { false, false, false, true }); res->prop_deterministic(); res->prop_inherently_weak(); return res; diff --git a/src/tgbaalgos/remfin.cc b/src/tgbaalgos/remfin.cc index b391fabee..63edcd59e 100644 --- a/src/tgbaalgos/remfin.cc +++ b/src/tgbaalgos/remfin.cc @@ -262,7 +262,7 @@ namespace spot unsigned nst = aut->num_states(); auto res = make_tgba_digraph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { false, false, false, false, true }); + 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_init_state(aut->get_init_state_number()); diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index cdda763d1..790dc81d9 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -317,7 +317,7 @@ namespace spot scc_filter_states(const const_tgba_digraph_ptr& aut, scc_info* given_si) { auto res = scc_filter_apply>(aut, given_si); - res->prop_copy(aut, { true, true, true, true, true }); + res->prop_copy(aut, { true, true, true, true }); return res; } @@ -340,7 +340,6 @@ namespace spot true, true, true, - true, }); return res; } @@ -370,7 +369,6 @@ namespace spot res->merge_transitions(); res->prop_copy(aut, { false, // state-based acceptance is not preserved - true, true, false, // determinism may not be preserved false, // stutter inv. of suspvars probably altered diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 0a538cb4e..4a0c130a8 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -632,7 +632,6 @@ namespace spot delete gb; res->prop_copy(original_, { false, // state-based acc forced below - false, // single acc set by set_generalized_buchi true, // weakness preserved, false, // determinism checked and set below true, // stutter inv. diff --git a/src/tgbaalgos/stutter.cc b/src/tgbaalgos/stutter.cc index 700fdad65..634938711 100644 --- a/src/tgbaalgos/stutter.cc +++ b/src/tgbaalgos/stutter.cc @@ -429,7 +429,6 @@ namespace spot } if (num_states != a->num_states()) a->prop_keep({true, // state_based - true, // single_acc false, // inherently_weak false, // deterministic false, // stutter inv. @@ -450,7 +449,6 @@ namespace spot closure(tgba_digraph_ptr&& a) { a->prop_keep({false, // state_based - true, // single_acc false, // inherently_weak false, // deterministic false, // stutter inv. @@ -518,7 +516,7 @@ namespace spot tgba_digraph_ptr closure(const const_tgba_digraph_ptr& a) { - return closure(make_tgba_digraph(a, {true, true, true, true, false})); + return closure(make_tgba_digraph(a, {true, true, true, false})); } // The stutter check algorithm to use can be overridden via an