From 2e165f188dacc2a72f5516bf18f424e25d542918 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 24 May 2018 17:52:42 +0200 Subject: [PATCH] rename SPOT_NB_ACC to SPOT_MAX_ACCSETS * NEWS, bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc, configure.ac, spot/parseaut/parseaut.yy, spot/twa/acc.cc, spot/twa/acc.hh, tests/core/acc.cc, .gitlab-ci.yml: Here. --- .gitlab-ci.yml | 2 +- NEWS | 4 ++-- bin/autcross.cc | 2 +- bin/autfilt.cc | 6 +++--- bin/ltlcross.cc | 2 +- configure.ac | 18 ++++++++++-------- spot/parseaut/parseaut.yy | 2 +- spot/twa/acc.cc | 2 +- spot/twa/acc.hh | 15 ++++++++------- tests/core/acc.cc | 10 +++++----- 10 files changed, 33 insertions(+), 30 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 4dc978c85..8c572b356 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -11,7 +11,7 @@ debian-stable-gcc: image: registry.lrde.epita.fr/spot-debuild:stable script: - autoreconf -vfi - - ./configure --enable-nb-acc=256 + - ./configure --enable-max-accsets=256 - make - make distcheck artifacts: diff --git a/NEWS b/NEWS index 7728469e8..494b62e79 100644 --- a/NEWS +++ b/NEWS @@ -26,8 +26,8 @@ New in spot 2.5.3.dev (not yet released) - You can now specify to Spot the number of acceptance marks you wish to use. This is a compile-time option, accessible through - option --with-nb-acc of the configure script. The default is - still 32, but this limit is no longer hardcoded. + option --enable-max-accsets of the configure script. The default + is still 32, but this limit is no longer hardcoded. - Option "a" of print_dot(), for printing the acceptance condition, is now enabled by default. Option "A", introduced in Spot 2.4, diff --git a/bin/autcross.cc b/bin/autcross.cc index 137966342..95b02b258 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -509,7 +509,7 @@ namespace const spot::const_twa_graph_ptr& aut_j, size_t i, size_t j) { - if (aut_i->num_sets() + aut_j->num_sets() > SPOT_NB_ACC) + if (aut_i->num_sets() + aut_j->num_sets() > SPOT_MAX_ACCSETS) { std::cerr << "info: building " << autname(i) << '*' << autname(j, true) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 9890bd579..e34d59323 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -649,7 +649,7 @@ static spot::twa_graph_ptr product(spot::twa_graph_ptr left, spot::twa_graph_ptr right) { if ((type == spot::postprocessor::BA) - && (left->num_sets() + right->num_sets() > SPOT_NB_ACC)) + && (left->num_sets() + right->num_sets() > SPOT_MAX_ACCSETS)) { left = ensure_tba(left); right = ensure_tba(right); @@ -661,7 +661,7 @@ static spot::twa_graph_ptr product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right) { if ((type == spot::postprocessor::BA) - && (left->num_sets() + right->num_sets() > SPOT_NB_ACC)) + && (left->num_sets() + right->num_sets() > SPOT_MAX_ACCSETS)) { left = ensure_tba(left); right = ensure_tba(right); @@ -965,7 +965,7 @@ parse_opt(int key, char* arg, struct argp_state*) if (res < 0) error(2, 0, "acceptance sets should be non-negative:" " --mask-acc=%ld", res); - if (static_cast(res) > SPOT_NB_ACC) + if (static_cast(res) > SPOT_MAX_ACCSETS) error(2, 0, "this implementation does not support that many" " acceptance sets: --mask-acc=%ld", res); opt_mask_acc.set(res); diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 4706d2f6b..2e226ea97 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -691,7 +691,7 @@ namespace const spot::const_twa_graph_ptr& aut_j, size_t i, size_t j, bool icomp, bool jcomp) { - if (aut_i->num_sets() + aut_j->num_sets() > SPOT_NB_ACC) + if (aut_i->num_sets() + aut_j->num_sets() > SPOT_MAX_ACCSETS) { // Report the skipped test if both automata are not // complemented, or the --verbose option is used, diff --git a/configure.ac b/configure.ac index 623d4bee8..5d99a6d41 100644 --- a/configure.ac +++ b/configure.ac @@ -60,16 +60,18 @@ AC_ARG_ENABLE([doxygen], AM_CONDITIONAL([ENABLE_DOXYGEN], [test "x${enable_doxygen:-no}" = xyes]) # Option to indicate the maximal number of acceptance marks -AC_COMPUTE_INT([default_nb_acc], [8*sizeof(unsigned)]) -AC_ARG_ENABLE([nb-acc], - [AC_HELP_STRING([--enable-nb-acc=N], - [Use up to N acceptance marks])], - [enable_nb_acc=$enableval], [enable_nb_acc=$default_nb_acc]) -if test 0 = `expr $enable_nb_acc % $default_nb_acc` +AC_COMPUTE_INT([default_max_accsets], [8*sizeof(unsigned)]) +AC_ARG_ENABLE([max-accsets], + [AC_HELP_STRING([--enable-max-accsets=N], + [Support up to N acceptance sets])], + [enable_max_accsets=$enableval], + [enable_max_accsets=$default_max_accsets]) +if test 0 -eq `expr $enable_max_accsets % $default_max_accsets` then - AC_DEFINE_UNQUOTED([NB_ACC], [$enable_nb_acc], [The number of acceptance marks]) + AC_DEFINE_UNQUOTED([MAX_ACCSETS], [$enable_max_accsets], + [The maximal number of acceptance sets supported (also known as acceptance marks)]) else - AC_ERROR([The argument of --enable-nb-acc must be a multiple of $default_nb_acc]) + AC_ERROR([The argument of --enable-max-accsets must be a multiple of $default_nb_acc]) fi # Activate C11 for gnulib tests diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index a4a0db623..6239bbaa0 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -772,7 +772,7 @@ header-item: "States:" INT "acceptance condition..."); error(res.accset_loc, "... previously defined here."); } - else if ($2 > SPOT_NB_ACC) + else if ($2 > SPOT_MAX_ACCSETS) { error(@1 + @2, "this implementation cannot support such a large " diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 87aab2f83..210bc4721 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -37,7 +37,7 @@ namespace spot #define STR(x) #x #define VALUESTR(x) STR(x) throw std::runtime_error("Too many acceptance sets used. " - "The limit is " VALUESTR(SPOT_NB_ACC) "."); + "The limit is " VALUESTR(SPOT_MAX_ACCSETS) "."); } std::ostream& operator<<(std::ostream& os, spot::acc_cond::mark_t m) diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index eb93cbc92..28e4b439e 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -52,11 +52,12 @@ namespace spot [[noreturn]] static void report_too_many_sets(); #endif public: - struct mark_t : public internal::_32acc + struct mark_t : + public internal::_32acc { private: - // configure guarantees that SPOT_NB_ACC % (8*sizeof(unsigned)) == 0 - typedef bitset _value_t; + // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0 + typedef bitset _value_t; _value_t id; mark_t(_value_t id) noexcept @@ -564,7 +565,7 @@ namespace spot if (n == 0) return inf({}); acc_cond::mark_t m = mark_t::all(); - m >>= (SPOT_NB_ACC - n); + m >>= (SPOT_MAX_ACCSETS - n); return inf(m); } @@ -573,7 +574,7 @@ namespace spot if (n == 0) return fin({}); acc_cond::mark_t m = mark_t::all(); - m >>= (SPOT_NB_ACC - n); + m >>= (SPOT_MAX_ACCSETS - n); return fin(m); } @@ -1245,7 +1246,7 @@ namespace spot return -1U; unsigned j = num_; num_ += num; - if (num_ > SPOT_NB_ACC) + if (num_ > SPOT_MAX_ACCSETS) report_too_many_sets(); all_ = all_sets_(); return j; @@ -1383,7 +1384,7 @@ namespace spot protected: mark_t all_sets_() const { - return mark_t::all() >> (SPOT_NB_ACC - num_); + return mark_t::all() >> (SPOT_MAX_ACCSETS - num_); } unsigned num_; diff --git a/tests/core/acc.cc b/tests/core/acc.cc index 24443a1dd..8e5d694da 100644 --- a/tests/core/acc.cc +++ b/tests/core/acc.cc @@ -64,8 +64,8 @@ int main() auto m1 = spot::acc_cond::mark_t({0, 2}); auto m2 = spot::acc_cond::mark_t({0, 3}); auto m3 = spot::acc_cond::mark_t({2, 1}); - auto m4 = spot::acc_cond::mark_t({0, SPOT_NB_ACC-2}); - if (!(m4.min_set() == 1 && m4.max_set() == SPOT_NB_ACC-1)) + auto m4 = spot::acc_cond::mark_t({0, SPOT_MAX_ACCSETS - 2}); + if (!(m4.min_set() == 1 && m4.max_set() == SPOT_MAX_ACCSETS - 1)) return 1; spot::acc_cond::mark_t m0 = {}; @@ -185,7 +185,7 @@ int main() try { - spot::acc_cond a{SPOT_NB_ACC+1}; + spot::acc_cond a{SPOT_MAX_ACCSETS + 1}; } catch (const std::runtime_error& e) { @@ -195,7 +195,7 @@ int main() try { spot::acc_cond::mark_t m{0}; - m <<= SPOT_NB_ACC + 1; + m <<= SPOT_MAX_ACCSETS + 1; } catch (const std::runtime_error& e) { @@ -205,7 +205,7 @@ int main() try { spot::acc_cond::mark_t m{0}; - m >>= SPOT_NB_ACC + 1; + m >>= SPOT_MAX_ACCSETS + 1; } catch (const std::runtime_error& e) {