twagraph: improve copy of kripke_graph

Fix #505, Reported by Edmond Irani Liu.

* spot/twa/twagraph.cc (copy): Deal with kripke_graph in a better way.
* spot/twaalgos/hoa.cc: Do not force the use of named-states since
when the input is a kripke_graph.
* tests/python/kripke.py: Adjust test cases.
* NEWS: Mention the change.
* THANKS: Add Edmund.

NEWS

@@ -2,6 +2,11 @@ New in spot 2.10.5.dev  (not yet released)
 
   Nothing yet.
 
+  - make_twa_graph() will now preserve state number when copying a
+    kripke_graph object.  As a consequence, print_dot() and
+    print_hoa() will now use state numbers matching those of the
+    kripke_graph (issue #505).
+
 New in spot 2.10.5  (2022-05-03)
 
   Bugs fixed:

THANKS

@@ -11,6 +11,7 @@ Christian Dax
 Christopher Ziegler
 Clément Tamines
 David Müller
+Edmond Irani Liu
 Ernesto Posse
 Étienne Renault
 Fabrice Kordon

spot/twa/twagraph.cc

@@ -22,6 +22,7 @@
 #include <spot/tl/print.hh>
 #include <spot/misc/bddlt.hh>
 #include <spot/twa/bddprint.hh>
+#include <spot/kripke/kripkegraph.hh>
 #include <spot/misc/escape.hh>
 #include <vector>
 #include <deque>
@@ -1275,6 +1276,17 @@ namespace spot
           return p.first->second;
         };
 
+      // If the input is a kripke_graph and the number of states is
+      // not restricted, predeclare all states to keep their
+      // numbering, and also copy unreachable states.
+      if (max_states == -1U)
+        if (auto kg = std::dynamic_pointer_cast<const kripke_graph>(aut))
+          {
+            unsigned ns = kg->num_states();
+            for (unsigned s = 0; s < ns; ++s)
+              new_state(kg->state_from_number(s));
+          }
+
       out->set_init_state(new_state(aut->get_init_state()));
       while (!todo.empty())
         {
@@ -1313,7 +1325,6 @@ namespace spot
             }
         }
 
-
       auto s = seen.begin();
       while (s != seen.end())
         {

spot/twaalgos/hoa.cc

@@ -31,6 +31,7 @@
 #include <spot/twa/formula2bdd.hh>
 #include <spot/tl/formula.hh>
 #include <spot/kripke/fairkripke.hh>
+#include <spot/kripke/kripkegraph.hh>
 
 using namespace std::string_literals;
 
@@ -771,7 +772,11 @@ namespace spot
           strcpy(tmpopt, opt);
         tmpopt[n] = 'k';
         tmpopt[n + 1] = 0;
-        preserve_names = true;
+        // Preserve names if we have some state names, or if we are
+        // not a kripke_graph.
+        auto sn = aut->get_named_prop<std::vector<std::string>>("state-names");
+        preserve_names =
+          !!sn || !std::dynamic_pointer_cast<const kripke_graph>(aut);
       }
 
     auto a = std::dynamic_pointer_cast<const twa_graph>(aut);

tests/python/kripke.py

@@ -26,35 +26,53 @@ p2 = buddy.bdd_ithvar(k.register_ap("p2"))
 cond1 = p1 & p2
 cond2 = p1 & -p2
 cond3 = -p1 & -p2
-s2 = k.new_state(cond1)
+s0 = k.new_state(cond1)
 s1 = k.new_state(cond2)
-s3 = k.new_state(cond3)
+s2 = k.new_state(cond3)
+k.new_edge(s1, s0)
+k.new_edge(s0, s0)
 k.new_edge(s1, s2)
 k.new_edge(s2, s2)
-k.new_edge(s1, s3)
-k.new_edge(s3, s3)
-k.new_edge(s3, s2)
+k.new_edge(s2, s0)
 k.set_init_state(s1)
 
 hoa = """HOA: v1
 States: 3
-Start: 0
+Start: 1
 AP: 2 "p1" "p2"
 acc-name: all
 Acceptance: 0 t
 properties: state-labels explicit-labels state-acc
 --BODY--
-State: [0&!1] 0 "1"
-1 2
-State: [0&1] 1 "0"
-1
-State: [!0&!1] 2 "2"
-2 1
+State: [0&1] 0
+0
+State: [0&!1] 1
+0 2
+State: [!0&!1] 2
+2 0
 --END--"""
 assert hoa == k.to_str('HOA')
 assert k.num_states() == 3
 assert k.num_edges() == 5
 
+k.set_state_names(["s0", "s1", "s2"])
+hoa = """HOA: v1
+States: 3
+Start: 1
+AP: 2 "p1" "p2"
+acc-name: all
+Acceptance: 0 t
+properties: state-labels explicit-labels state-acc
+--BODY--
+State: [0&1] 0 "s0"
+0
+State: [0&!1] 1 "s1"
+0 2
+State: [!0&!1] 2 "s2"
+2 0
+--END--"""
+assert hoa == k.to_str('HOA')
+
 res = []
 for e in k.out(s1):
     res.append((e.src, e.dst))