stats: speed up the computation of transitions

Juraj Major reported a case with 32 APs where ltlcross would take
forever to gather statistics.  It turns out that for each edge,
twa_sub_statistics was enumerating all compatible assignments of 32
APs.  This uses bdd_satcountset() instead, and also store the result
in a long long to avoid overflows.

* spot/twaalgos/stats.cc (twa_sub_statistics): Improve the code for
counting transitions.
* bin/common_aoutput.hh, bin/ltlcross.cc, spot/twaalgos/stats.hh:
Store transition counts are long long.
* tests/core/readsave.test: Add test case.
* NEWS: Mention the bug.

NEWS

@@ -21,6 +21,14 @@ New in spot 2.9.0.dev (not yet released)
     spot::translator class when creating deterministic automata with
     generic acceptance.
 
+  Bugs fixed:
+
+  - spot::twa_sub_statistics was very slow at computing the number of
+    transitons, and could overflow.  It is now avoiding some costly
+    loop of BDD operations, and storing the result using at least 64
+    bits.  This affects the output of "ltlcross --csv" and
+    "--stats=%t" for many tools.
+
 New in spot 2.9 (2020-04-30)
 
   Command-line tools:

bin/common_aoutput.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -167,7 +167,7 @@ private:
   spot::printable_acc_cond haut_gen_acc_;
   spot::printable_value<unsigned> haut_states_;
   spot::printable_value<unsigned> haut_edges_;
-  spot::printable_value<unsigned> haut_trans_;
+  spot::printable_value<unsigned long long> haut_trans_;
   spot::printable_value<unsigned> haut_acc_;
   printable_varset haut_ap_;
   printable_varset aut_ap_;

bin/ltlcross.cc

@@ -296,7 +296,7 @@ struct statistics
   double time;
   unsigned states;
   unsigned edges;
-  unsigned transitions;
+  unsigned long long transitions;
   unsigned acc;
   unsigned scc;
   unsigned nonacc_scc;

spot/twaalgos/stats.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2011-2018 Laboratoire de Recherche et
+// Copyright (C) 2008, 2011-2018, 2020 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -64,7 +64,7 @@ namespace spot
     {
     public:
       sub_stats_bfs(const const_twa_ptr& a, twa_sub_statistics& s)
-        : stats_bfs(a, s), s_(s), seen_(a->ap_vars())
+        : stats_bfs(a, s), s_(s), apvars_(a->ap_vars())
       {
       }
 
@@ -73,17 +73,12 @@ namespace spot
                    const twa_succ_iterator* it) override
       {
         ++s_.edges;
-        bdd cond = it->cond();
-        while (cond != bddfalse)
-          {
-            cond -= bdd_satoneset(cond, seen_, bddtrue);
-            ++s_.transitions;
-          }
+        s_.transitions += bdd_satcountset(it->cond(), apvars_);
       }
 
     private:
       twa_sub_statistics& s_;
-      bdd seen_;
+      bdd apvars_;
     };
 
 
@@ -180,11 +175,7 @@ namespace spot
             [&s, &ge](bdd cond)
             {
               ++s.edges;
-              while (cond != bddfalse)
-                {
-                  cond -= bdd_satoneset(cond, ge->ap_vars(), bddtrue);
-                  ++s.transitions;
-                }
+              s.transitions += bdd_satcountset(cond, ge->ap_vars());
             });
       }
     return s;

spot/twaalgos/stats.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2011-2017 Laboratoire de Recherche et
+// Copyright (C) 2008, 2011-2017, 2020 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -44,7 +44,7 @@ namespace spot
 
   struct SPOT_API twa_sub_statistics: public twa_statistics
   {
-    unsigned transitions;
+    unsigned long long transitions;
 
     twa_sub_statistics() { transitions = 0; }
     std::ostream& dump(std::ostream& out) const;
@@ -125,7 +125,7 @@ namespace spot
     printable_formula form_;
     printable_value<unsigned> states_;
     printable_value<unsigned> edges_;
-    printable_value<unsigned> trans_;
+    printable_value<unsigned long long> trans_;
     printable_value<unsigned> acc_;
     printable_scc_info scc_;
     printable_value<unsigned> nondetstates_;

tests/core/readsave.test

@@ -1119,3 +1119,28 @@ f="{{!a;!b}:{{c <-> d} && {e xor f} && {m | {l && {k | {j <-> {i xor {g && h}"
 f="$f}}}}} && {{n && o} | {!n && p}} && {q -> {r <-> s}}}:{[*0..1];t}}[]-> u"
 ltl2tgba -f "$f" --dot=bar > out.dot
 grep 'label too long' out.dot
+
+
+# genltl --and-fg=32 | ltlfilt --relabel=abc | ltldo ltl3ba produces a
+# few edges equivalent to a lot of transitions.  The code used to
+# count those transitions used to be very inefficient.
+cat >andfg32.hoa <<EOF
+HOA: v1
+States: 2
+Start: 0
+AP: 32 "a" "ab" "b" "bb" "c" "cb" "d" "db" "e" "eb" "f" "fb" "g" "h"
+"i" "j" "k" "l" "m" "n" "o" "p" "q" "r" "s" "t" "u" "v" "w" "x" "y" "z"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+[t] 0
+[0&1&2&3&4&5&6&7&8&9&10&11&12&13&14&15&16&17
+&18&19&20&21&22&23&24&25&26&27&28&29&30&31] 1
+State: 1 {0}
+[0&1&2&3&4&5&6&7&8&9&10&11&12&13&14&15&16&17
+&18&19&20&21&22&23&24&25&26&27&28&29&30&31] 1
+--END--
+EOF
+test `autfilt andfg32.hoa --stats=%t` = 4294967298 # 2^32 + 2