From 543e0db9a059d1344bdd646250a832a6a650e070 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 22 Dec 2016 19:39:03 +0100
Subject: [PATCH] stats: add a variant for twa_graph_ptr

This is faster than using the abstract interface, and it also supports
alternating automata.  (This will be tested in the tests for
ltlcross's support for alternating automata.)

* spot/twaalgos/stats.cc (stats_reachable, sub_stats_reachable):
Add code specific to twa_graph_ptr.
---
 spot/twaalgos/stats.cc | 78 +++++++++++++++++++++++++++++++++++++++---
 1 file changed, 74 insertions(+), 4 deletions(-)

diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc
index e0ec92e3d..60461c86d 100644
--- a/spot/twaalgos/stats.cc
+++ b/spot/twaalgos/stats.cc
@@ -84,6 +84,48 @@ namespace spot
       twa_sub_statistics& s_;
       bdd seen_;
     };
+
+
+    template<typename SU, typename EU>
+    void dfs(const const_twa_graph_ptr& ge, SU state_update, EU edge_update)
+    {
+      unsigned init = ge->get_init_state_number();
+      unsigned num_states = ge->num_states();
+      // The TODO vector serves two purposes:
+      // - it is a stack of states to process,
+      // - it is a set of processed states.
+      // The lower 31 bits of each entry is a state on the stack. (The
+      // next usable entry on the stack is indicated by todo_pos.)  The
+      // 32th bit (i.e., the sign bit) of todo[x] indicates whether
+      // states number x has been seen.
+      std::vector<unsigned> todo(num_states, 0);
+      const unsigned seen = 1 << (sizeof(unsigned)*8-1);
+      const unsigned mask = seen - 1;
+      unsigned todo_pos = 0;
+      for (unsigned i: ge->univ_dests(init))
+        {
+          todo[todo_pos++] = i;
+          todo[i] |= seen;
+        }
+      do
+        {
+          state_update();
+          unsigned cur = todo[--todo_pos] & mask;
+          todo[todo_pos] ^= cur;        // Zero the state
+          for (auto& t: ge->out(cur))
+            {
+              edge_update(t.cond);
+              for (unsigned dst: ge->univ_dests(t.dst))
+                if (!(todo[dst] & seen))
+                  {
+                    todo[dst] |= seen;
+                    todo[todo_pos++] |= dst;
+                  }
+            }
+        }
+      while (todo_pos > 0);
+    };
+
   } // anonymous
 
 
@@ -105,8 +147,18 @@ namespace spot
   stats_reachable(const const_twa_ptr& g)
   {
     twa_statistics s;
-    stats_bfs d(g, s);
-    d.run();
+    auto ge = std::dynamic_pointer_cast<const twa_graph>(g);
+    if (!ge)
+      {
+        stats_bfs d(g, s);
+        d.run();
+      }
+    else
+      {
+        dfs(ge,
+            [&s](){ ++s.states; },
+            [&s](bdd){ ++s.edges; });
+      }
     return s;
   }
 
@@ -114,8 +166,26 @@ namespace spot
   sub_stats_reachable(const const_twa_ptr& g)
   {
     twa_sub_statistics s;
-    sub_stats_bfs d(g, s);
-    d.run();
+    auto ge = std::dynamic_pointer_cast<const twa_graph>(g);
+    if (!ge)
+      {
+        sub_stats_bfs d(g, s);
+        d.run();
+      }
+    else
+      {
+        dfs(ge,
+            [&s](){ ++s.states; },
+            [&s, &ge](bdd cond)
+            {
+              ++s.edges;
+              while (cond != bddfalse)
+                {
+                  cond -= bdd_satoneset(cond, ge->ap_vars(), bddtrue);
+                  ++s.transitions;
+                }
+            });
+      }
     return s;
   }