From 602aad013f6ee16f3ec0112a4a2bb3f93a43d932 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 4 Feb 2025 21:08:01 +0100
Subject: [PATCH] aiger: never use state names for encoding

* spot/twaalgos/aiger.cc (mealy_machine_to_aig): Remove the code that
attempted to convert state names to integer, throwing exceptions on
failure.  That code was not exercised anywhere, but it caused failure
in the implementation of an LTLf->AIG pipeline in which LTLf formulas
that label states are preserved.
---
 spot/twaalgos/aiger.cc | 59 ++++++++++++++----------------------------
 1 file changed, 20 insertions(+), 39 deletions(-)

diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc
index 8c29dfe41..c3359fe72 100644
--- a/spot/twaalgos/aiger.cc
+++ b/spot/twaalgos/aiger.cc
@@ -1503,7 +1503,7 @@ namespace
   state_to_vec(std::vector<unsigned>& v, unsigned s,
                unsigned offset)
   {
-    assert(s != -1u && "-1u is not a valid sstate");
+    assert(s != -1u && "-1u is not a valid state");
     v.clear();
     unsigned i = offset;
     while (s > 0)
@@ -1553,7 +1553,7 @@ namespace
                 const std::vector<std::string>& unused_outs = {},
                 const realizability_simplifier* rs = nullptr)
   {
-    // The aiger circuit can currently noly encode separated mealy machines
+    // The aiger circuit can currently only encode separated mealy machines
 
     for (const auto& astrat : strat_vec)
       if (!astrat.first->acc().is_t())
@@ -1681,49 +1681,30 @@ namespace
         state_numbers.emplace_back(N, -1u);
         auto& sn = state_numbers.back();
         unsigned max_index = 0;
-        // Check if named
-        auto sp_ptr = astrat.first->get_named_prop<region_t>("state-player");
-        if (const auto* s_names =
-                astrat.first->
-                  get_named_prop<std::vector<std::string>>("state-names"))
+        if (auto sp_ptr =
+            astrat.first->get_named_prop<region_t>("state-player"))
           {
+            const region_t& sp = *sp_ptr;
+            // Split
+            unsigned n_next = 0;
+            // Player -1u
+            // Env: Succesively numbered according to appearance
             for (unsigned n = 0; n < N; ++n)
-              {
-                if (sp_ptr && (*sp_ptr)[n])
-                  continue;
-                // Remains -1u
-                unsigned su = std::stoul((*s_names)[n]);
-                max_index = std::max(max_index, su);
-                sn[n] = su;
-              }
-            ++max_index;
+              if (!sp[n])
+                sn[n] = n_next++;
+            max_index = n_next;
           }
         else
           {
-            if (sp_ptr)
-              {
-                auto sp = *sp_ptr;
-                // Split
-                unsigned n_next = 0;
-                // Player -1u
-                // Env: Succesively numbered according to appearance
-                for (unsigned n = 0; n < N; ++n)
-                  if (!sp[n])
-                    sn[n] = n_next++;
-                max_index = n_next;
-              }
-            else
-              {
-                std::iota(state_numbers.back().begin(),
-                          state_numbers.back().end(), 0);
-                max_index = N;
-              }
-
-            // Ensure 0 <-> init state
-            std::swap(state_numbers.back()[0],
-                      state_numbers.back()[astrat.first->
-                                             get_init_state_number()]);
+            std::iota(state_numbers.back().begin(),
+                      state_numbers.back().end(), 0);
+            max_index = N;
           }
+        // Ensure 0 <-> init state
+        std::swap(state_numbers.back()[0],
+                  state_numbers.back()[astrat.first->
+                                       get_init_state_number()]);
+
         // Largest index to encode -> num_states()-1
         log2n.push_back(std::ceil(std::log2(max_index)));
         latch_offset.push_back(n_latches);