fix "requires separate Inf and Fin sets" error from ltl2tgba -G

Report from David Müller.

* spot/twaalgos/simulation.cc: Add wrapper to deal with automata
sharing Fin/Inf sets.
* tests/core/ltl2tgba2.test: New test cases.
* NEWS: Mention the change.

NEWS

@@ -51,6 +51,11 @@ New in spot 2.7.3.dev (not yet released)
   - separate_sets_here() (and therefore autfilt --separate-sets) could
     loop infinitely on some inputs.
 
+  - In some situation, ltl2tgba -G could abort with
+    "direct_simulation() requires separate Inf and Fin sets".  This
+    was fixed by teaching simulation-based reductions how to deal
+    with such cases.
+
 New in spot 2.7.3 (2019-04-19)
 
   Bugs fixed:

spot/twaalgos/simulation.cc

@@ -30,7 +30,7 @@
 #include <spot/twaalgos/sepsets.hh>
 #include <spot/twaalgos/isdet.hh>
 #include <spot/misc/bddlt.hh>
-#include <spot/twaalgos/hoa.hh>
+#include <spot/twaalgos/cleanacc.hh>
 
 //  Simulation-based reduction, implemented using bdd-based signatures.
 //
@@ -803,43 +803,70 @@ namespace spot
       std::vector<bdd>* record_implications_;
     };
 
+    template<typename Fun, typename Aut>
+    twa_graph_ptr
+    wrap_simul(Fun f, const Aut& a)
+    {
+      if (has_separate_sets(a))
+        return f(a);
+      // If the input has acceptance sets common to Fin and Inf,
+      // separate them before doing the simulation, and merge them
+      // back afterwards.  Doing will temporarily introduce more sets
+      // and may exceed the number of sets we support.  But it's
+      // better than refusing to apply simulation-based reductions to
+      // automata sharing Fin/Inf sets.
+      auto b = make_twa_graph(a, twa::prop_set::all());
+      separate_sets_here(b);
+      return simplify_acceptance_here(f(b));
+    }
+
   } // End namespace anonymous.
 
 
   twa_graph_ptr
   simulation(const const_twa_graph_ptr& t)
   {
-    direct_simulation<false, false> simul(t);
+    return wrap_simul([](const const_twa_graph_ptr& t) {
-    return simul.run();
+                        direct_simulation<false, false> simul(t);
+                        return simul.run();
+                      }, t);
   }
 
   twa_graph_ptr
   simulation(const const_twa_graph_ptr& t,
              std::vector<bdd>* implications)
   {
-    direct_simulation<false, false> simul(t, implications);
+    return wrap_simul([implications](const const_twa_graph_ptr& t) {
-    return simul.run();
+                        direct_simulation<false, false> simul(t, implications);
+                        return simul.run();
+                      }, t);
   }
 
   twa_graph_ptr
   simulation_sba(const const_twa_graph_ptr& t)
   {
-    direct_simulation<false, true> simul(t);
+    return wrap_simul([](const const_twa_graph_ptr& t) {
-    return simul.run();
+                        direct_simulation<false, true> simul(t);
+                        return simul.run();
+                      }, t);
   }
 
   twa_graph_ptr
   cosimulation(const const_twa_graph_ptr& t)
   {
-    direct_simulation<true, false> simul(t);
+    return wrap_simul([](const const_twa_graph_ptr& t) {
-    return simul.run();
+                        direct_simulation<true, false> simul(t);
+                        return simul.run();
+                      }, t);
   }
 
   twa_graph_ptr
   cosimulation_sba(const const_twa_graph_ptr& t)
   {
-    direct_simulation<true, true> simul(t);
+    return wrap_simul([](const const_twa_graph_ptr& t) {
-    return simul.run();
+                        direct_simulation<true, true> simul(t);
+                        return simul.run();
+                      }, t);
   }
 
 
@@ -876,13 +903,13 @@ namespace spot
   twa_graph_ptr
   iterated_simulations(const const_twa_graph_ptr& t)
   {
-    return iterated_simulations_<false>(t);
+    return wrap_simul(iterated_simulations_<false>, t);
   }
 
   twa_graph_ptr
   iterated_simulations_sba(const const_twa_graph_ptr& t)
   {
-    return iterated_simulations_<true>(t);
+    return wrap_simul(iterated_simulations_<true>, t);
   }
 
 } // End namespace spot.

tests/core/ltl2tgba2.test

@@ -409,3 +409,16 @@ f='(a R !b) & (c R !d) & G((!b | !d) & (!a | Fb) & (!c | Fd) '
 f=$f'& (!b | X(b | (a R !b))) & (!d | X(d | (c R !d))) & F(a | !b) & F(c | !d))'
 test '8,1' = `ltl2tgba "$f" --stats=%s,%d`
 test '8,1' = `ltl2tgba -GD "$f" --stats=%s,%d`
+
+
+# Two formulas for which ltl2tgba 2.7.3 was raising an error with -GDS
+# Reported by David Müller.
+cat >in <<EOF
+& | G F p0 F G p1 | G F ! p1 F G p2
+& & | G F p0 F G p1 | G F ! p1 F G p2 | G F ! p2 F G ! p0
+EOF
+ltl2tgba --lbt-input -GDS -Fin --stats='%s,%g' >out
+cat >expected <<EOF
+8,(Fin(1) | Inf(0)) & (Fin(2) | Inf(1))
+8,(Fin(1) | Inf(0)) & (Fin(2) | Inf(1)) & (Fin(0) | Inf(2))
+EOF