diff --git a/NEWS b/NEWS index 3a950996a..d6f6a702b 100644 --- a/NEWS +++ b/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. diff --git a/doc/org/hoa.org b/doc/org/hoa.org index 26969e4ed..6994abdc5 100644 --- a/doc/org/hoa.org +++ b/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 diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 7d5fac361..5b8792e96 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -2671,12 +2671,30 @@ static void fix_initial_state(result_& r) for (auto& pp: start) { unsigned p = pp.front(); - if (p != init) - // FIXME: If p has no incoming we should be able to - // change the source of the edges of p instead of - // adding new edges. - for (auto& t: aut->out(p)) - aut->new_edge(init, t.dst, t.cond); + if (p == init) + continue; + if (!has_incoming[p]) + { + // 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 diff --git a/tests/core/522.test b/tests/core/522.test index 5fe6ba945..3f1596514 100755 --- a/tests/core/522.test +++ b/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() -autfilt --remove-dead 552.hoa > out.hoa -grep 'States: 7' out.hoa +# This command used to break during print_hoa() +autfilt 552.hoa > out.hoa +test "8 1 16 0" = "`autfilt --stats='%[a]s %[u]s %[a]e %[u]e' out.hoa`" + +cat >552loop1.hoa < out.hoa +test "8 0 20 0" = "`autfilt --stats='%[a]s %[u]s %[a]e %[u]e' out.hoa`" + +cat >552loop2.hoa < out.hoa +test "9 0 24 0" = "`autfilt --stats='%[a]s %[u]s %[a]e %[u]e' out.hoa`" diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 3780b4766..cf6f43b89 100755 --- a/tests/core/readsave.test +++ b/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="E4", tooltip="\\\\E\n#4"] - 3 -> 0 [label="b", id="E5", tooltip="\\\\E\n#5"] + 3 -> 1 [label="a", id="E3", tooltip="\\\\E\n#3"] + 3 -> 0 [label="b", id="E4", tooltip="\\\\E\n#4"] } EOF