Commit ad08a585 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent cf79cefd
......@@ -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:
......
......@@ -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()~ | |
......@@ -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
......
......@@ -143,13 +143,13 @@ namespace spot
}
unsigned int
emptiness_check_instantiator::min_acceptance_conditions() const
emptiness_check_instantiator::min_sets() const
{
return static_cast<ec_algo*>(info_)->min_acc;
}
unsigned int
emptiness_check_instantiator::max_acceptance_conditions() const
emptiness_check_instantiator::max_sets() const
{
return static_cast<ec_algo*>(info_)->max_acc;
}
......
......@@ -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);
......
......@@ -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
......
......@@ -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
......
......@@ -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);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment