From 875846f51ff135591412069235a8bae11cb0fef8 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 16 Apr 2020 10:54:10 +0200
Subject: [PATCH] toparity: false transitions are not a problem anymore

* spot/twaalgos/toparity.cc: Do not remove false transitions.
* tests/python/toparity.py: Add a test case with false transitions.
---
 spot/twaalgos/toparity.cc | 25 ++-----------------------
 tests/python/toparity.py  | 24 +++++++++++++++++++-----
 2 files changed, 21 insertions(+), 28 deletions(-)

diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc
index 49c9d7fcb..0351e12a8 100644
--- a/spot/twaalgos/toparity.cc
+++ b/spot/twaalgos/toparity.cc
@@ -1657,7 +1657,7 @@ run()
     unsigned initial_state = aut_->get_init_state_number();
     auto initial_car_ptr = state2car.find(initial_state);
     car_state initial_car;
-    // If we take an automaton with one state and without transition, 
+    // If we take an automaton with one state and without transition,
     // the SCC was useless so state2car doesn't have initial_state
     if (initial_car_ptr == state2car.end())
     {
@@ -1703,34 +1703,13 @@ to_parity_options options;
 std::vector<std::string>* names;
 }; // car_generator
 
-  static const_twa_graph_ptr
-  remove_false_transitions(const const_twa_graph_ptr& a)
-  {
-    // Do not do anything if the automaton has no false transition
-    for (auto edge : a->edges())
-      if (edge.cond == bddfalse)
-        goto doremoval;
-    return a;
-  doremoval:
-    auto res_ = make_twa_graph(a->get_dict());
-    res_->copy_ap_of(a);
-    res_->new_states(a->num_states());
-    for (auto edge : a->edges())
-      if (edge.cond != bddfalse)
-        res_->new_edge(edge.src, edge.dst, edge.cond, edge.acc);
-    res_->set_init_state(a->get_init_state_number());
-    res_->set_acceptance(a->get_acceptance());
-    res_->prop_copy(a, twa::prop_set::all());
-    return res_;
-  }
-
 }// namespace
 
 
 twa_graph_ptr
 to_parity(const const_twa_graph_ptr &aut, const to_parity_options options)
 {
-    return car_generator(remove_false_transitions(aut), options).run();
+    return car_generator(aut, options).run();
 }
 
   // Old version of CAR.
diff --git a/tests/python/toparity.py b/tests/python/toparity.py
index d06a72206..8301789b3 100644
--- a/tests/python/toparity.py
+++ b/tests/python/toparity.py
@@ -19,7 +19,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
-import itertools
+from itertools import zip_longest
+from buddy import bddfalse
 
 # Tests for the new version of to_parity
 
@@ -91,8 +92,7 @@ options = [
 
 
 def test(aut, expected_num_states=[], full=True):
-    for (opt, expected_num) in\
-            itertools.zip_longest(options, expected_num_states):
+    for (opt, expected_num) in zip_longest(options, expected_num_states):
         p1 = spot.to_parity(aut,
                             search_ex = opt.search_ex,
                             use_last = opt.use_last,
@@ -107,8 +107,8 @@ def test(aut, expected_num_states=[], full=True):
                             pretty_print = opt.pretty_print,
                             )
         assert spot.are_equivalent(aut, p1)
-        if (expected_num != None):
-                assert(p1.num_states() == expected_num)
+        if expected_num is not None:
+                assert p1.num_states() == expected_num
         if full:
             # Make sure passing opt is the same as setting
             # each argument individually
@@ -343,6 +343,20 @@ assert p.num_states() == 22
 assert spot.are_equivalent(a, p)
 test(a, [8, 7, 8, 8, 6, 7, 6])
 
+# Force a few edges to false, to make sure to_parity() is OK with that.
+for e in a.out(2):
+    if e.dst == 1:
+        e.cond = bddfalse
+        break
+for e in a.out(3):
+    if e.dst == 3:
+        e.cond = bddfalse
+        break
+p = spot.to_parity_old(a, True)
+assert p.num_states() == 22
+assert spot.are_equivalent(a, p)
+test(a, [7, 6, 7, 7, 6, 6, 6])
+
 for f in spot.randltl(4, 400):
     d = spot.translate(f, "det", "G")
     p = spot.to_parity_old(d, True)