From d7ee23ed2f3a1663055fffa1a52a76d6ef2c76c4 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Tue, 6 Mar 2018 15:06:26 +0100 Subject: [PATCH] acc_cond::mark_t now relies on bitset This allows to represent more than 32 acceptance marks. * configure.ac: add an option to specify the number of marks * spot/twa/acc.hh: implement it * tests/python/acc_cond.ipynb, tests/core/acc.cc, tests/core/ltlcross3.test: update tests * NEWS: document it * bin/randltl.cc: fix an include --- NEWS | 5 +++ bin/randltl.cc | 1 + configure.ac | 13 +++++++ spot/twa/acc.hh | 67 ++++++++++++------------------------- tests/core/acc.cc | 11 ++++++ tests/core/ltlcross3.test | 60 --------------------------------- tests/python/acc_cond.ipynb | 66 ------------------------------------ 7 files changed, 51 insertions(+), 172 deletions(-) diff --git a/NEWS b/NEWS index cd454c433..0c8c59540 100644 --- a/NEWS +++ b/NEWS @@ -17,6 +17,11 @@ New in spot 2.5.3.dev (not yet released) Library: + - 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 "a" of print_dot(), for printing the acceptance condition, is now enabled by default. Option "A", introduced in Spot 2.4, can be used to hide the acceptance condition in case you do not diff --git a/bin/randltl.cc b/bin/randltl.cc index d35871151..dd6bce180 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -34,6 +34,7 @@ #include "common_cout.hh" #include +#include #include #include #include diff --git a/configure.ac b/configure.ac index 9e1f20337..606af1816 100644 --- a/configure.ac +++ b/configure.ac @@ -59,6 +59,19 @@ AC_ARG_ENABLE([doxygen], [enable_doxygen=yes], [enable_doxygen=no]) 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 (( $enable_nb_acc % $default_nb_acc == 0 )) +then + AC_DEFINE_UNQUOTED([NB_ACC], [$enable_nb_acc], [The number of acceptance marks]) +else + AC_ERROR([The argument of --enable-nb-acc must be a multiple of $default_nb_acc]) +fi + # Activate C11 for gnulib tests AX_CHECK_COMPILE_FLAG([-std=c11], [CFLAGS="$CFLAGS -std=c11"]) diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 933b6a30a..0d911fe36 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -20,13 +20,14 @@ #pragma once #include -#include #include #include -#include -#include #include +#include +#include +#include + namespace spot { namespace internal @@ -39,19 +40,22 @@ namespace spot public: struct mark_t { - typedef unsigned value_t; + // configure guarantees that SPOT_NB_ACC % (8*sizeof(unsigned)) == 0 + typedef bitset value_t; value_t id; - mark_t() = default; - + private: mark_t(value_t id) noexcept : id(id) { } + public: + mark_t() = default; + template mark_t(const iterator& begin, const iterator& end) noexcept - : mark_t(0U) + : mark_t(value_t::zero()) { for (iterator i = begin; i != end; ++i) set(*i); @@ -123,12 +127,12 @@ namespace spot void set(unsigned u) { - id |= (1U << u); + id |= (value_t::one() << u); } void clear(unsigned u) { - id &= ~(1U << u); + id &= ~(value_t::one() << u); } mark_t& operator&=(mark_t r) @@ -238,18 +242,7 @@ namespace spot // Number of bits sets. unsigned count() const { -#ifdef __GNUC__ - return __builtin_popcount(id); -#else - unsigned c = 0U; - auto v = id; - while (v) - { - ++c; - v &= v - 1; - } - return c; -#endif + return id.count(); } // Return the number of the highest set used plus one. @@ -257,18 +250,10 @@ namespace spot // If the sets {1,3,8} are used, this returns 9. unsigned max_set() const { -#ifdef __GNUC__ - return (id == 0) ? 0 : (sizeof(unsigned) * 8 - __builtin_clz(id)); -#else - auto i = id; - int res = 0; - while (i) - { - ++res; - i >>= 1; - } - return res; -#endif + if (id) + return id.highest()+1; + else + return 0; } // Return the number of the lowest set used plus one. @@ -276,20 +261,10 @@ namespace spot // If the sets {1,3,8} are used, this returns 2. unsigned min_set() const { - if (id == 0) + if (id) + return id.lowest()+1; + else return 0; -#ifdef __GNUC__ - return __builtin_ctz(id) + 1; -#else - auto i = id; - int res = 1; - while ((i & 1) == 0) - { - ++res; - i >>= 1; - } - return res; -#endif } // Return the lowest acceptance mark diff --git a/tests/core/acc.cc b/tests/core/acc.cc index 572e01074..c33417b76 100644 --- a/tests/core/acc.cc +++ b/tests/core/acc.cc @@ -23,6 +23,7 @@ #include #include #include +#include #include static void check(spot::acc_cond& ac, spot::acc_cond::mark_t m) @@ -178,4 +179,14 @@ int main() std::cout << c1 << '\n'; std::cout << c2 << '\n'; assert(c1 == c2); + + try + { + spot::acc_cond a{SPOT_NB_ACC+1}; + } + catch (const std::runtime_error& e) + { + return std::strcmp(e.what(), "Too many acceptance sets used."); + } + return 1; } diff --git a/tests/core/ltlcross3.test b/tests/core/ltlcross3.test index 16182cbd7..749e38077 100755 --- a/tests/core/ltlcross3.test +++ b/tests/core/ltlcross3.test @@ -318,63 +318,3 @@ ltlcross --color --products=0 ltl2tgba -f GFa -f FGa --csv=out.csv grep product out.csv && exit 1 check_csv out.csv -# -cat >fake <<\EOF -case $1 in -"foo") -cat <<\END -HOA: v1 -name: "foo" -States: 1 -Start: 0 -AP: 5 "p0" "p1" "p2" "p3" "p4" -acc-name: parity min odd 32 -Acceptance: 32 Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | (Fin(4) & -(Inf(5) | (Fin(6) & (Inf(7) | (Fin(8) & (Inf(9) | (Fin(10) & (Inf(11) -| (Fin(12) & (Inf(13) | (Fin(14) & (Inf(15) | (Fin(16) & (Inf(17) | -(Fin(18) & (Inf(19) | (Fin(20) & (Inf(21) | (Fin(22) & (Inf(23) | -(Fin(24) & (Inf(25) | (Fin(26) & (Inf(27) | (Fin(28) & (Inf(29) | -(Fin(30) & Inf(31))))))))))))))))))))))))))))))) ---BODY-- -State: 0 -0 { 0} 0 { 1} 0 { 2} 0 { 3} 0 { 4} 0 { 5} 0 { 6} 0 { 7} 0 { 8} 0 { 9} -0 {10} 0 {11} 0 {12} 0 {13} 0 {14} 0 {15} 0 {16} 0 {17} 0 {18} 0 {19} -0 {20} 0 {21} 0 {22} 0 {23} 0 {24} 0 {25} 0 {26} 0 {27} 0 {28} 0 {29} -0 {30} 0 {31} ---END-- -END -;; -"!(foo)") -cat <<\END -HOA: v1 -name: "foo" -States: 1 -Start: 0 -AP: 5 "p0" "p1" "p2" "p3" "p4" -acc-name: parity min even 32 -Acceptance: 32 Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & (Inf(4) | -(Fin(5) & (Inf(6) | (Fin(7) & (Inf(8) | (Fin(9) & (Inf(10) | (Fin(11) -& (Inf(12) | (Fin(13) & (Inf(14) | (Fin(15) & (Inf(16) | (Fin(17) & -(Inf(18) | (Fin(19) & (Inf(20) | (Fin(21) & (Inf(22) | (Fin(23) & -(Inf(24) | (Fin(25) & (Inf(26) | (Fin(27) & (Inf(28) | (Fin(29) & -(Inf(30) | Fin(31))))))))))))))))))))))))))))))) ---BODY-- -State: 0 -0 { 0} 0 { 1} 0 { 2} 0 { 3} 0 { 4} 0 { 5} 0 { 6} 0 { 7} 0 { 8} 0 { 9} -0 {10} 0 {11} 0 {12} 0 {13} 0 {14} 0 {15} 0 {16} 0 {17} 0 {18} 0 {19} -0 {20} 0 {21} 0 {22} 0 {23} 0 {24} 0 {25} 0 {26} 0 {27} 0 {28} 0 {29} -0 {30} 0 {31} ---END-- -END -;; -esac -EOF - -chmod +x fake -ltlcross './fake %f >%O' -f foo --verbose --csv=out.csv 2>stderr -cat stderr -test 2 = `grep -c 'info:.*-> failed (Too many .* used.)' stderr` -check_csv out.csv -ltlcross --color=never './fake %f >%O' -f foo --csv=out.csv 2>stderr -cat stderr -test 2 = `grep -c 'info: preproc.* failed (Too many .* used.)' stderr` diff --git a/tests/python/acc_cond.ipynb b/tests/python/acc_cond.ipynb index 5d15e63fc..7300e516b 100644 --- a/tests/python/acc_cond.ipynb +++ b/tests/python/acc_cond.ipynb @@ -245,72 +245,6 @@ "x << 2" ] }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Internally, the `mark_t` stores the bit-vector as an integer. This implies that we currently do not support more than 32 acceptance sets. The underlying integer can be retrieved using `.id`. Note that this implementation may evolve in the future, so relying on it is not recommended." - ] - }, - { - "cell_type": "code", - "execution_count": 10, - "metadata": { - "collapsed": false - }, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "{0,2,5}\n", - "37\n", - "0b100101\n" - ] - } - ], - "source": [ - "print(x)\n", - "print(x.id)\n", - "print(bin(x.id))" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "`mark_t` can also be initialized using an integer: in that case the integer is interpreted as a bit vector.\n", - "\n", - "A frequent error is to use `mark_t(n)` when we really mean `mark_t([n])` or `mark_t((n,))`.\n", - "\n", - "As the underlying implementation of `mark_t` may change in the future, it is not recommended to rely on this interface." - ] - }, - { - "cell_type": "code", - "execution_count": 11, - "metadata": { - "collapsed": false - }, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "{5}\n", - "{0,2}\n", - "{0,2,4}\n" - ] - } - ], - "source": [ - "# compare\n", - "print(spot.mark_t([5]))\n", - "# with\n", - "print(spot.mark_t(5))\n", - "print(spot.mark_t(0b10101))" - ] - }, { "cell_type": "markdown", "metadata": {},