twagraph: remove bddfalse edges in purge_dead_states

* spot/twa/twagraph.cc (purge_dead_states): Be bddfalse-aware!
* spot/twa/twagraph.hh, NEWS: Document this.
* tests/python/alternating.py, tests/python/twagraph.py: Add some
test cases.

NEWS

@@ -1,6 +1,9 @@
 New in spot 2.10.1.dev  (not yet released)
 
-  Nothing yet.
+  Bugs fixed:
+
+  - twa_graph::purge_dead_states() now also removes edges labeled by
+    bddfalse.
 
 New in spot 2.10.1  (2021-11-19)
 

spot/twa/twagraph.cc

@@ -618,7 +618,7 @@ namespace spot
             auto& t = g_.edge_storage(tid);
             todo.back().second = t.next_succ;
             unsigned dst = t.dst;
-            if (useful[dst] != 1)
+            if (useful[dst] != 1 && t.cond != bddfalse)
               {
                 todo.emplace_back(dst, g_.state_storage(dst).succ);
                 useful[dst] = 1;
@@ -674,9 +674,12 @@ namespace spot
               }
             unsigned dst = *begin++;
             if (begin == end)
+              // that was the last destination, update the stack for
+              // the next edge.
               {
-                if (tid != 0)
+                do
                   tid = g_.edge_storage(tid).next_succ;
+                while (tid && g_.edge_storage(tid).cond == bddfalse);
                 if (tid != 0)
                   beginend(g_.edge_storage(tid).dst, begin, end);
               }
@@ -684,6 +687,8 @@ namespace spot
               {
                 auto& ss = g_.state_storage(dst);
                 unsigned succ = ss.succ;
+                while (succ && g_.edge_storage(succ).cond == bddfalse)
+                  succ = g_.edge_storage(succ).next_succ;
                 if (succ == 0U)
                   continue;
                 useful[dst] = 1;

spot/twa/twagraph.hh

@@ -611,7 +611,8 @@ namespace spot
     /// Dead states are all the states that cannot be part of
     /// an infinite run of the automaton.  This includes
     /// states without successors, unreachable states, and states
-    /// that only have dead successors.
+    /// that only have dead successors.  Transition labeled
+    /// by bddfalse are also removed.
     ///
     /// This function runs in linear time on non-alternating automata,
     /// but its current implementation can be quadratic when removing

tests/python/alternating.py

@@ -1,6 +1,6 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de
+# Copyright (C) 2016, 2017, 2021 Laboratoire de Recherche et Développement de
 # l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -207,3 +207,10 @@ State: 2
 
 desalt = spot.remove_univ_otf(aut)
 assert(desalt.to_str('hoa') == out)
+
+assert aut.num_states() == 3
+assert aut.num_edges() == 3
+aut.edge_storage(3).cond = buddy.bddfalse
+aut.purge_dead_states()
+assert aut.num_states() == 1
+assert aut.num_edges() == 0

tests/python/twagraph.py

@@ -21,7 +21,7 @@
 # This file tests various error conditions on the twa API
 
 import spot
-from buddy import bddtrue
+from buddy import bddtrue, bddfalse
 
 aut = spot.make_twa_graph(spot.make_bdd_dict())
 
@@ -113,3 +113,14 @@ aut.release_iter(it)
 aut.purge_dead_states()
 i = aut.get_init_state()
 assert aut.state_is_accepting(i) == False
+
+aut = spot.translate('FGa')
+# Kill the edge between state 0 and 1
+assert aut.edge_storage(2).src == 0
+assert aut.edge_storage(2).dst == 1
+aut.edge_data(2).cond = bddfalse
+assert aut.num_edges() == 3
+assert aut.num_states() == 2
+aut.purge_dead_states()
+assert aut.num_edges() == 1
+assert aut.num_states() == 1