From a102fdb2a74799a919eca4459a28aa1c821937b8 Mon Sep 17 00:00:00 2001
From: Antoine Martin <amartin@lrde.epita.fr>
Date: Mon, 14 Mar 2022 15:17:51 +0100
Subject: [PATCH] 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 | 47 ++++++++++++++++++++++++++++++++++++++++
 spot/twaalgos/remprop.hh |  3 +++
 2 files changed, 50 insertions(+)

diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc
index 942a1b4b5..b693015fd 100644
--- a/spot/twaalgos/remprop.cc
+++ b/spot/twaalgos/remprop.cc
@@ -244,4 +244,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;
+  }
 }
diff --git a/spot/twaalgos/remprop.hh b/spot/twaalgos/remprop.hh
index 09d75ffac..4b496e65a 100644
--- a/spot/twaalgos/remprop.hh
+++ b/spot/twaalgos/remprop.hh
@@ -54,5 +54,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");
 
 }