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
2018-03-06 15:06:26 +01:00 · 2018-03-06 15:06:26 +01:00 · d7ee23ed2f
commit d7ee23ed2f
parent d77d046d26
7 changed files with 51 additions and 172 deletions
--- a/5
+++ b/5
@ -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
--- a/bin/randltl.cc
+++ b/bin/randltl.cc
@ -34,6 +34,7 @@
 #include "common_cout.hh"

 #include <sstream>
+#include <spot/tl/defaultenv.hh>
 #include <spot/tl/randomltl.hh>
 #include <spot/tl/simplify.hh>
 #include <spot/misc/random.hh>
--- 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"])

--- a/spot/twa/acc.hh
+++ b/spot/twa/acc.hh
@ -20,13 +20,14 @@
 #pragma once

 #include <functional>
-#include <unordered_map>
 #include <sstream>
 #include <vector>
-#include <spot/tl/defaultenv.hh>
-#include <spot/misc/trival.hh>
 #include <iostream>

+#include <spot/misc/_config.h>
+#include <spot/misc/bitset.hh>
+#include <spot/misc/trival.hh>
+
 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<SPOT_NB_ACC / (8*sizeof(unsigned))> value_t;
      value_t id;

-      mark_t() = default;
-
+    private:
      mark_t(value_t id) noexcept
        : id(id)
      {
      }

+    public:
+      mark_t() = default;
+
      template<class iterator>
      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
--- a/tests/core/acc.cc
+++ b/tests/core/acc.cc
@ -23,6 +23,7 @@
 #include <vector>
 #include <cassert>
 #include <cstdlib>
+#include <cstring>
 #include <spot/twa/acc.hh>

 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;
 }
--- 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`
--- 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": {},