honor ap() when counting transitions

Fixing this bug alone revealed another bug: parsing never claim or LBTT
automata did not register APs.  So this fixes both bugs.

This is the first part of #170.

* spot/twa/twa.hh (register_aps_from_dict): New method.
* spot/parseaut/parseaut.yy: Call it for never claim and LBTT files.
* spot/twaalgos/stats.cc: Simplify using ap_vars().
* tests/core/ltl2tgba.test: Add a test case.
* NEWS: Mention the bugs.

NEWS

@@ -36,6 +36,12 @@ New in spot 2.0a (not yet released)
   * Fix autfilt to apply --simplify-exclusive-ap only after
     the simplifications of (--small/--deterministic) have
     been performed.
+  * The automaton parser did not fully register atomic propositions
+    for automata read from never claim or as LBTT.
+  * The sub_stats_reachable() function used to count the number
+    of transitions based on the number of atomic propositions
+    actually *used* by the automaton instead of using the number
+    of AP declared.
 
 New in spot 2.0 (2016-04-11)
 

spot/parseaut/parseaut.yy

@@ -1529,6 +1529,7 @@ never: "never"
 	 // Pretend that we have declared all states.
 	 for (auto& p: res.info_states)
 	   p.declared = true;
+         res.h->aut->register_aps_from_dict();
        }
 
 nc-states:
@@ -1750,6 +1751,7 @@ lbtt: lbtt-header lbtt-body ENDAUT
 	 res.info_states.resize(res.h->aut->num_states());
 	 for (auto& s: res.info_states)
 	   s.declared = true;
+         res.h->aut->register_aps_from_dict();
       }
     | lbtt-header-states LBTT_EMPTY
       {

spot/twa/twa.hh

@@ -738,6 +738,34 @@ namespace spot
     }
     ///@}
 
+
+    /// \brief Register all atomic propositions that have
+    /// already be register by the bdd_dict for this automaton.
+    ///
+    /// This method may only be called on an automaton with an empty
+    /// list of AP.  It will fetch all atomic proposition that have
+    /// been set in the bdd_dict for this particular automaton.
+    ///
+    /// The typical use-case for this function is when the labels of
+    /// an automaton are created by functions such as
+    /// formula_to_bdd().  This is for instance done in the parser
+    /// for never claims or LBTT.
+    void register_aps_from_dict()
+    {
+      if (!aps_.empty())
+        throw std::runtime_error("register_ap_from_dict() may not be"
+                                 " called on an automaton that has already"
+                                 " registered some AP");
+      auto& m = get_dict()->bdd_map;
+      unsigned s = m.size();
+      for (unsigned n = 0; n < s; ++n)
+        if (m[n].refs.find(this) != m[n].refs.end())
+          {
+            aps_.push_back(m[n].f);
+            bddaps_ &= bdd_ithvar(n);
+          }
+    }
+
     /// \brief The vector of atomic propositions registered by this
     /// automaton.
     const std::vector<formula>& ap() const

spot/twaalgos/stats.cc

@@ -62,7 +62,7 @@ namespace spot
     {
     public:
       sub_stats_bfs(const const_twa_ptr& a, twa_sub_statistics& s)
-        : stats_bfs(a, s), s_(s), seen_(bddtrue)
+        : stats_bfs(a, s), s_(s), seen_(a->ap_vars())
       {
       }
 
@@ -71,24 +71,7 @@ namespace spot
                    const twa_succ_iterator* it) override
       {
         ++s_.edges;
-
         bdd cond = it->cond();
-        bdd newvars = bdd_exist(bdd_support(cond), seen_);
-        if (newvars != bddtrue)
-          {
-            seen_ &= newvars;
-            int count = 0;
-            while (newvars != bddtrue)
-              {
-                ++count;
-                newvars = bdd_high(newvars);
-              }
-            // If we discover one new variable, that means that all
-            // transitions we counted so far are actually double
-            // subtransitions.  If we have two new variables, they where
-            // quadruple transitions, etc.
-            s_.transitions <<= count;
-          }
         while (cond != bddfalse)
           {
             cond -= bdd_satoneset(cond, seen_, bddtrue);

tests/core/ltl2tgba.test

@@ -221,3 +221,6 @@ ltlfilt -q -r -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b'
 # test unknown dot options
 ltl2tgba --dot=@ a 2>stderr && exit 1
 grep 'ltl2tgba: unknown option.*@' stderr
+
+# Make sure the count of AP is correct through never claims or LBTT
+ltl2tgba -f a -s | autfilt -q --ap=1 --lbtt | autfilt -q --ap=1