From ad08a585af93de5e0f5a257c1cbb82bf3524f28b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 3 Mar 2016 18:16:25 +0100 Subject: [PATCH] rename two confusing methods of emptiness_check_instantiator * spot/twaalgos/emptiness.hh (emptiness_check_instantiator): rename min_acceptance_conditions and max_acceptance_conditions to min_sets and max_sets. * spot/twaalgos/emptiness.cc, python/ajax/spotcgi.in, tests/core/ikwiad.cc, tests/core/emptchk.cc, tests/core/randtgba.cc: Adjust. * doc/org/upgrade2.org, NEWS: Mention the change. --- NEWS | 4 ++ doc/org/upgrade2.org | 111 +++++++++++++++++++------------------ python/ajax/spotcgi.in | 4 +- spot/twaalgos/emptiness.cc | 4 +- spot/twaalgos/emptiness.hh | 6 +- tests/core/emptchk.cc | 4 +- tests/core/ikwiad.cc | 10 ++-- tests/core/randtgba.cc | 3 +- 8 files changed, 76 insertions(+), 70 deletions(-) diff --git a/NEWS b/NEWS index 224346ac2..445c02701 100644 --- a/NEWS +++ b/NEWS @@ -3,6 +3,10 @@ New in spot 1.99.8a (not yet released) Library: * twa::ap_var() renamed to twa::ap_vars(). + * emptiness_check_instantiator::min_acceptance_conditions() and + emptiness_check_instantiator::max_acceptance_conditions() renamed + to emptiness_check_instantiator::min_sets() and + emptiness_check_instantiator::max_sets(). Documentation: diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org index 14599bea1..372ef5b2e 100644 --- a/doc/org/upgrade2.org +++ b/doc/org/upgrade2.org @@ -609,57 +609,60 @@ for (auto i: aut->succ(s)) The following is a non-exhaustive list of functions or classes that have been renamed. -| old name | new name | comment | -|-------------------------------------------------------+---------------------------------------------+-----------------------------------------------------------| -| ~dstar_parse()~ | ~parse_aut()~ | single parser for all automata | -| ~dtgba_complement()~ | ~dtwa_complement()~ | | -| ~dupexp_bfs()~ | | deleted | -| ~dupexp_dfs()~ | ~copy()~ | | -| ~format_parse_aut_errors()~ | ~parsed_aut::format_errors()~ | | -| ~hoaf_reachable()~ | ~print_hoa()~ | | -| ~is_guarantee_automaton()~ | ~is_terminal_automaton()~ | | -| ~kripke_parse()~ | ~parse_aut()~ | single parser for all automata | -| ~kripke_save_reachable()~ | ~print_hoa()~ | adhoc output format replaced by HOA | -| ~kripke_save_reachable_renumbered()~ | ~print_hoa()~ | adhoc output format replaced by HOA | -| ~lbtt_parse()~ | ~parse_aut()~ | single parser for all automata | -| ~lbtt_reachable()~ | ~print_lbtt()~ | | -| ~ltl::formula::is_X_free()~ | ~formula::is_syntactic_stutter_invariant()~ | | -| ~ltl::ltl_simplifier~ | ~tl_simplifier~ | | -| ~ltl::parse_boolean()~ | ~parse_infix_boolean()~ | | -| ~ltl::parse_lbt()~ | ~parse_prefix_ltl()~ | | -| ~ltl::parse()~ | ~parse_infix_psl()~ | | -| ~ltl::parse_sere()~ | ~parse_infix_sere()~ | | -| ~ltl::to_latex_string()~ | ~print_latex_psl()~ | also ~str_latex_psl()~ | -| ~ltl::to_lbt_string()~ | ~print_lbt_ltl()~ | also ~str_lbt_ltl()~ | -| ~ltl::to_sclatex_string()~ | ~print_sclatex_psl()~ | also ~str_sclatex_psl()~ | -| ~ltl::to_spin_string()~ | ~print_spin_ltl()~ | also ~str_spin_ltl()~ | -| ~ltl::to_string()~ | ~print_psl()~, ~print_sere()~ | also ~str_psl()~ or ~str_sere()~ | -| ~ltl::to_ut8_string()~ | ~print_utg8_psl()~, ~print_utf8_sere()~ | also ~str_utf8_psl()~ or ~str_utf8_sere()~ | -| ~ltl::to_wring_string()~ | ~print_wring_ltl()~ | also ~str_wring_ltl()~ | -| ~neverclaim_parse()~ | ~parse_aut()~ | single parser for all automata | -| ~never_claim_reachable()~ | ~print_never_claim()~ | | -| ~print_tgba_run()~ | ~tgba_run::operator<<()~ | | -| ~reduce_run()~ | ~twa_run::reduce()~ | | -| ~replay_tgba_run()~ | ~twa_run::replay()~ | | -| ~scc_map~ | ~scc_info~ | new implementation restricted to ~twa_graph~ | -| ~ta_succ_iterator::current_acceptance_conditions()~ | ~ta_succ_iterator::acc()~ | | -| ~ta_succ_iterator::current_condition()~ | ~ta_succ_iterator::cond()~ | | -| ~ta_succ_iterator::current_state()~ | ~ta_succ_iterator::dst()~ | | -| ~tgba~ | ~twa~ | | -| ~tgba::all_acceptance_conditions()~ | | use ~tgba::acc().accepting()~ or ~tgba::acc().all_sets()~ | -| ~tgba::neg_acceptance_conditions()~ | | deleted | -| ~tgba::number_of_acceptance_conditions()~ | ~tgba::num_sets()~ | | -| ~tgba::support_conditions()~ | | deleted | -| ~tgba::support_variables()~ | | deleted | -| ~tgba_explicit_formula~ | | deleted | -| ~tgba_explicit_number~ | ~twa_graph~ | new implementation | -| ~tgba_explicit_string~ | | deleted | -| ~tgba_parse()~ | ~parse_aut()~ | single parser for all automata | -| ~tgba_run_to_tgba()~ | ~twa_run::as_twa()~ | | -| ~tgba_run~ | ~twa_run~ | | -| ~tgba_save_reachable()~ | ~print_hoa()~ | adhoc output format replaced by HOA | -| ~tgba_statistics::transitions()~ | ~twa_statistics::edges()~ | | -| ~tgba_sub_statistics::sub_transitions()~ | ~twa_sub_statistics::transitions()~ | | -| ~tgba_succ_iterator::current_acceptance_conditions()~ | ~twa_succ_iterator::acc()~ | | -| ~tgba_succ_iterator::current_condition()~ | ~twa_succ_iterator::cond()~ | | -| ~tgba_succ_iterator::current_state()~ | ~twa_succ_iterator::dst()~ | | +| old name | new name | comment | +|-------------------------------------------------------------+---------------------------------------------+-----------------------------------------------------------| +| ~dstar_parse()~ | ~parse_aut()~ | single parser for all automata | +| ~dtgba_complement()~ | ~dtwa_complement()~ | | +| ~dupexp_bfs()~ | | deleted | +| ~dupexp_dfs()~ | ~copy()~ | | +| ~format_parse_aut_errors()~ | ~parsed_aut::format_errors()~ | | +| ~emptiness_check_instantiator::construct()~ | ~make_emptiness_check_instantiator()~ | | +| ~emptiness_check_instantiator::max_acceptance_conditions()~ | ~emptiness_check_instantiator::max_sets()~ | | +| ~emptiness_check_instantiator::min_acceptance_conditions()~ | ~emptiness_check_instantiator::min_sets()~ | | +| ~hoaf_reachable()~ | ~print_hoa()~ | | +| ~is_guarantee_automaton()~ | ~is_terminal_automaton()~ | | +| ~kripke_parse()~ | ~parse_aut()~ | single parser for all automata | +| ~kripke_save_reachable()~ | ~print_hoa()~ | adhoc output format replaced by HOA | +| ~kripke_save_reachable_renumbered()~ | ~print_hoa()~ | adhoc output format replaced by HOA | +| ~lbtt_parse()~ | ~parse_aut()~ | single parser for all automata | +| ~lbtt_reachable()~ | ~print_lbtt()~ | | +| ~ltl::formula::is_X_free()~ | ~formula::is_syntactic_stutter_invariant()~ | | +| ~ltl::ltl_simplifier~ | ~tl_simplifier~ | | +| ~ltl::parse_boolean()~ | ~parse_infix_boolean()~ | | +| ~ltl::parse_lbt()~ | ~parse_prefix_ltl()~ | | +| ~ltl::parse()~ | ~parse_infix_psl()~ | | +| ~ltl::parse_sere()~ | ~parse_infix_sere()~ | | +| ~ltl::to_latex_string()~ | ~print_latex_psl()~ | also ~str_latex_psl()~ | +| ~ltl::to_lbt_string()~ | ~print_lbt_ltl()~ | also ~str_lbt_ltl()~ | +| ~ltl::to_sclatex_string()~ | ~print_sclatex_psl()~ | also ~str_sclatex_psl()~ | +| ~ltl::to_spin_string()~ | ~print_spin_ltl()~ | also ~str_spin_ltl()~ | +| ~ltl::to_string()~ | ~print_psl()~, ~print_sere()~ | also ~str_psl()~ or ~str_sere()~ | +| ~ltl::to_ut8_string()~ | ~print_utg8_psl()~, ~print_utf8_sere()~ | also ~str_utf8_psl()~ or ~str_utf8_sere()~ | +| ~ltl::to_wring_string()~ | ~print_wring_ltl()~ | also ~str_wring_ltl()~ | +| ~neverclaim_parse()~ | ~parse_aut()~ | single parser for all automata | +| ~never_claim_reachable()~ | ~print_never_claim()~ | | +| ~print_tgba_run()~ | ~tgba_run::operator<<()~ | | +| ~reduce_run()~ | ~twa_run::reduce()~ | | +| ~replay_tgba_run()~ | ~twa_run::replay()~ | | +| ~scc_map~ | ~scc_info~ | new implementation restricted to ~twa_graph~ | +| ~ta_succ_iterator::current_acceptance_conditions()~ | ~ta_succ_iterator::acc()~ | | +| ~ta_succ_iterator::current_condition()~ | ~ta_succ_iterator::cond()~ | | +| ~ta_succ_iterator::current_state()~ | ~ta_succ_iterator::dst()~ | | +| ~tgba~ | ~twa~ | | +| ~tgba::all_acceptance_conditions()~ | | use ~tgba::acc().accepting()~ or ~tgba::acc().all_sets()~ | +| ~tgba::neg_acceptance_conditions()~ | | deleted | +| ~tgba::number_of_acceptance_conditions()~ | ~tgba::num_sets()~ | | +| ~tgba::support_conditions()~ | | deleted | +| ~tgba::support_variables()~ | | deleted | +| ~tgba_explicit_formula~ | | deleted | +| ~tgba_explicit_number~ | ~twa_graph~ | new implementation | +| ~tgba_explicit_string~ | | deleted | +| ~tgba_parse()~ | ~parse_aut()~ | single parser for all automata | +| ~tgba_run_to_tgba()~ | ~twa_run::as_twa()~ | | +| ~tgba_run~ | ~twa_run~ | | +| ~tgba_save_reachable()~ | ~print_hoa()~ | adhoc output format replaced by HOA | +| ~tgba_statistics::transitions()~ | ~twa_statistics::edges()~ | | +| ~tgba_sub_statistics::sub_transitions()~ | ~twa_sub_statistics::transitions()~ | | +| ~tgba_succ_iterator::current_acceptance_conditions()~ | ~twa_succ_iterator::acc()~ | | +| ~tgba_succ_iterator::current_condition()~ | ~twa_succ_iterator::cond()~ | | +| ~tgba_succ_iterator::current_state()~ | ~twa_succ_iterator::dst()~ | | diff --git a/python/ajax/spotcgi.in b/python/ajax/spotcgi.in index 80dcdfac9..1cd1bb6e1 100755 --- a/python/ajax/spotcgi.in +++ b/python/ajax/spotcgi.in @@ -803,8 +803,8 @@ if output_type == 'r': else: ec_a = 0 n_acc = degen.acc().num_sets() - n_max = eci.max_acceptance_conditions() - n_min = eci.min_acceptance_conditions() + n_max = eci.max_sets() + n_min = eci.min_sets() if (n_acc <= n_max): if (n_acc >= n_min): ec_a = degen diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index 82b6599a9..cfa071f20 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -143,13 +143,13 @@ namespace spot } unsigned int - emptiness_check_instantiator::min_acceptance_conditions() const + emptiness_check_instantiator::min_sets() const { return static_cast(info_)->min_acc; } unsigned int - emptiness_check_instantiator::max_acceptance_conditions() const + emptiness_check_instantiator::max_sets() const { return static_cast(info_)->max_acc; } diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh index 0df56f129..4e9057b42 100644 --- a/spot/twaalgos/emptiness.hh +++ b/spot/twaalgos/emptiness.hh @@ -224,15 +224,15 @@ namespace spot } /// @} - /// \brief Minimum number of acceptance conditions supported by + /// \brief Minimum number of acceptance sets supported by /// the emptiness check. - unsigned int min_acceptance_conditions() const; + unsigned int min_sets() const; /// \brief Maximum number of acceptance conditions supported by /// the emptiness check. /// /// \return \c -1U if no upper bound exists. - unsigned int max_acceptance_conditions() const; + unsigned int max_sets() const; protected: emptiness_check_instantiator(option_map o, void* i); diff --git a/tests/core/emptchk.cc b/tests/core/emptchk.cc index de57168a8..1cac9e9df 100644 --- a/tests/core/emptchk.cc +++ b/tests/core/emptchk.cc @@ -132,7 +132,7 @@ main(int argc, char** argv) auto a = aut[j]; std::cout << "** Testing aut[" << j << "] using " << algo << '\n'; unsigned n_acc = a->acc().num_sets(); - unsigned n_max = i->max_acceptance_conditions(); + unsigned n_max = i->max_sets(); if (n_max < n_acc) { std::cout << "Skipping because automaton has " << n_acc @@ -140,7 +140,7 @@ main(int argc, char** argv) << " accepts at most " << n_max << ".\n"; continue; } - unsigned n_min = i->min_acceptance_conditions(); + unsigned n_min = i->min_sets(); if (n_min > n_acc) { std::cout << "Skipping because automaton has " << n_acc diff --git a/tests/core/ikwiad.cc b/tests/core/ikwiad.cc index 56b45ba01..f9e0146be 100644 --- a/tests/core/ikwiad.cc +++ b/tests/core/ikwiad.cc @@ -1103,7 +1103,7 @@ checked_main(int argc, char** argv) if (echeck_inst && degeneralize_opt == NoDegen && n_acc > 1 - && echeck_inst->max_acceptance_conditions() < n_acc) + && echeck_inst->max_sets() < n_acc) { degeneralize_opt = DegenTBA; assume_sba = false; @@ -1334,7 +1334,7 @@ checked_main(int argc, char** argv) if (echeck_inst && degeneralize_opt == NoDegen && n_acc > 1 - && echeck_inst->max_acceptance_conditions() < n_acc) + && echeck_inst->max_sets() < n_acc) degeneralize_opt = DegenTBA; if (degeneralize_opt == DegenTBA) { @@ -1359,13 +1359,13 @@ checked_main(int argc, char** argv) if (echeck_inst - && (a->acc().num_sets() < echeck_inst->min_acceptance_conditions())) + && (a->acc().num_sets() < echeck_inst->min_sets())) { if (!paper_opt) { std::cerr << echeck_algo << " requires at least " - << echeck_inst->min_acceptance_conditions() - << " acceptance conditions." << std::endl; + << echeck_inst->min_sets() + << " acceptance sets." << std::endl; exit(1); } else diff --git a/tests/core/randtgba.cc b/tests/core/randtgba.cc index 9066bcb69..c818f55cd 100644 --- a/tests/core/randtgba.cc +++ b/tests/core/randtgba.cc @@ -86,8 +86,7 @@ cons_emptiness_check(int num, spot::const_twa_graph_ptr a, unsigned int n_acc) { auto inst = ec_algos[num].inst; - if (n_acc < inst->min_acceptance_conditions() - || n_acc > inst->max_acceptance_conditions()) + if (n_acc < inst->min_sets() || n_acc > inst->max_sets()) a = degen; if (a) return inst->instantiate(a);