From 396009c014beb3437508dd1ec1cc2a625c68081f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Jan 2023 15:09:26 +0100 Subject: [PATCH] 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 | 5 +++++ doc/org/hoa.org | 5 +++-- spot/parseaut/parseaut.yy | 30 +++++++++++++++++++++++------ tests/core/522.test | 40 ++++++++++++++++++++++++++++++++++++--- tests/core/readsave.test | 7 +++---- 5 files changed, 72 insertions(+), 15 deletions(-) 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