parseaut: better merge of multiple initial states

If an initial states without incoming transition has to be merged into
another one, its outgoing edges can be reused by just changing their
source.

* spot/parseaut/parseaut.yy (fix_initial_state): Implement this here.
* tests/core/522.test: Add more tests.
* tests/core/readsave.test: Adjust one expected output.
* doc/org/hoa.org: Mention the completeness change.
* NEWS: Mention the new feature.

NEWS

@@ -9,6 +9,11 @@ New in spot 2.11.3.dev  (not yet released)
     - b:b[*i..j] = b[*max(i,1)..j]
     - b[*i..j]:b[*k..l] = b[*max(i,1)+max(k,1)-1, j+l-1]
 
+  - The HOA parser is a bit smarter when merging multiple initial
+    states into a single initial state (Spot's automaton class
+    supports only one): it now reuse the edges leaving initial states
+    without incoming transitions.
+
   Python:
 
   - spot.acd() no longer depends on jQuery for interactivity.

doc/org/hoa.org

@@ -66,7 +66,7 @@ the HOA format, the output may not be exactly the same as the input.
   sets.
 
   This hard-coded limit can be augmented at configure time
-  using option `--enable-max-accsets=N`, but doing so will consume
+  using option =--enable-max-accsets=N=, but doing so will consume
   more memory and time.
 
 - Multiple (or missing) initial states are emulated.
@@ -76,7 +76,8 @@ the HOA format, the output may not be exactly the same as the input.
   is transformed into an equivalent TωA by merging the initial states
   into a single one.  The merged state can either be one of the
   original initial states (if one of those has no incoming edge) or a
-  new state introduced for that purpose.
+  new state introduced for that purpose.  This "conversion" may change
+  the completeness property of the automaton.
 
   Similarly, when an automaton with no initial state is loaded (this
   includes the case where the automaton has no state), a disconnected

spot/parseaut/parseaut.yy

@@ -2671,14 +2671,32 @@ static void fix_initial_state(result_& r)
           for (auto& pp: start)
             {
               unsigned p = pp.front();
-              if (p != init)
+              if (p == init)
-                // FIXME: If p has no incoming we should be able to
+                continue;
-                // change the source of the edges of p instead of
+              if (!has_incoming[p])
-                // adding new edges.
+                {
+                  // If p has no incoming edge, we can simply take
+                  // out its outgoing edges and "re-source" them on init.
+                  // This will avoid creating new edges.
+                  for (auto& t: aut->out(p))
+                    t.src = init;
+                  auto& gr = aut->get_graph();
+                  auto& ps = gr.state_storage(p);
+                  auto& is = gr.state_storage(init);
+                  gr.edge_storage(is.succ_tail).next_succ = ps.succ;
+                  is.succ_tail = ps.succ_tail;
+                  ps.succ = ps.succ_tail = 0;
+                  // we just created a state without successors
+                  aut->prop_complete(false);
+                }
+              else
+                {
+                  // duplicate all edges
                   for (auto& t: aut->out(p))
                     aut->new_edge(init, t.dst, t.cond);
                 }
             }
+        }
       else
         {
           // In the alternating case, we merge outgoing transition of

tests/core/522.test

@@ -38,6 +38,40 @@ State: 0 {0} [t] 2 [t] 3 State: 1 {0} [t] 4 [t] 5 State: 2
 State: 5 {1} [t] 6 [t] 7 State: 6 [t] 6 [t] 7 State: 7 [t] 6 [t] 7
 --END--
 EOF
-# This command, even without --remove-dead, used to break during print_hoa()
+# This command used to break during print_hoa()
-autfilt --remove-dead 552.hoa > out.hoa
+autfilt 552.hoa > out.hoa
-grep 'States: 7' out.hoa
+test "8 1 16 0" = "`autfilt --stats='%[a]s %[u]s %[a]e %[u]e' out.hoa`"
+
+cat >552loop1.hoa <<EOF
+HOA: v1
+States: 8
+Start: 0
+Start: 1
+AP: 0
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+--BODY--
+State: 0 {0} [t] 2 [t] 3 [t] 0 State: 1 {0} [t] 4 [t] 5 State: 2
+{0} [t] 2 [t] 3 State: 3 {0} [t] 6 [t] 7 State: 4 {1} [t] 4 [t] 5
+State: 5 {1} [t] 6 [t] 7 State: 6 [t] 6 [t] 7 State: 7 [t] 6 [t] 7
+--END--
+EOF
+autfilt 552loop1.hoa > out.hoa
+test "8 0 20 0" = "`autfilt --stats='%[a]s %[u]s %[a]e %[u]e' out.hoa`"
+
+cat >552loop2.hoa <<EOF
+HOA: v1
+States: 8
+Start: 0
+Start: 1
+AP: 0
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+--BODY--
+State: 0 {0} [t] 2 [t] 3 [t] 0 State: 1 {0} [t] 4 [t] 5 [t] 1 State: 2
+{0} [t] 2 [t] 3 State: 3 {0} [t] 6 [t] 7 State: 4 {1} [t] 4 [t] 5
+State: 5 {1} [t] 6 [t] 7 State: 6 [t] 6 [t] 7 State: 7 [t] 6 [t] 7
+--END--
+EOF
+autfilt 552loop2.hoa > out.hoa
+test "9 0 24 0" = "`autfilt --stats='%[a]s %[u]s %[a]e %[u]e' out.hoa`"

tests/core/readsave.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012, 2014-2022 Laboratoire de
+# Copyright (C) 2009, 2010, 2012, 2014-2023 Laboratoire de
 # Recherche et Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -346,9 +346,8 @@ digraph "" {
   0 -> 0 [label="b", id="E1", tooltip="\\\\E\n#1"]
   1 -> 1 [label="a", id="E2", tooltip="\\\\E\n#2"]
   2 [label="s2"]
-  2 -> 0 [label="b", id="E3", tooltip="\\\\E\n#3"]
+  3 -> 1 [label="a", id="E3", tooltip="\\\\E\n#3"]
-  3 -> 1 [label="a", id="E4", tooltip="\\\\E\n#4"]
+  3 -> 0 [label="b", id="E4", tooltip="\\\\E\n#4"]
-  3 -> 0 [label="b", id="E5", tooltip="\\\\E\n#5"]
 }
 EOF