twaalgos: add from_finite

* spot/twaalgos/remprop.cc, spot/twaalgos/remprop.hh: add a from_finite
  function to perform the opposite operation to to_finite

spot/twaalgos/remprop.cc

@@ -245,4 +245,51 @@ namespace spot
 
   }
 
+  twa_graph_ptr from_finite(const_twa_graph_ptr aut, const char* alive)
+  {
+    twa_graph_ptr res =
+      make_twa_graph(aut,
+                     { true, false, true, false, false, false });
+
+    if (aut->get_named_prop<std::vector<std::string>>("state-names"))
+      res->copy_state_names_from(aut);
+    auto* names = res->get_named_prop<std::vector<std::string>>("state-names");
+
+    unsigned alive_sink = res->new_state();
+    if (names != nullptr)
+      names->push_back("sink");
+    auto acc = res->acc().all_sets();
+    auto alive_bdd = bdd_ithvar(res->register_ap(alive));
+    res->new_edge(alive_sink, alive_sink, !alive_bdd, acc);
+
+    unsigned ns = res->num_states();
+    for (unsigned s = 0; s < ns; ++s)
+      {
+        if (s == alive_sink)
+          continue;
+
+        bool was_acc = res->state_is_accepting(s);
+
+        // erase accepting marks, require alive on non-accepting transition,
+        // and remove self-loop edges used to mark acceptance
+        auto i = res->out_iteraser(s);
+        while (i)
+          {
+            if (i->src == i->dst && i->cond == bddfalse)
+              {
+                i.erase();
+                continue;
+              }
+
+            i->cond &= alive_bdd;
+            i->acc = {};
+            ++i;
+          }
+
+        if (was_acc)
+          res->new_edge(s, alive_sink, !alive_bdd);
+      }
+
+    return res;
+  }
 }

spot/twaalgos/remprop.hh

@@ -53,5 +53,8 @@ namespace spot
   SPOT_API twa_graph_ptr
   to_finite(const_twa_graph_ptr aut, const char* alive = "alive");
 
+  /// \brief The opposite of the to_finite operation
+  SPOT_API twa_graph_ptr
+  from_finite(const_twa_graph_ptr aut, const char* alive = "alive");
 
 }