diff --git a/NEWS b/NEWS index 5f513f974..a19408a5c 100644 --- a/NEWS +++ b/NEWS @@ -228,6 +228,8 @@ New in spot 2.9.7.dev (not yet released) before attempting to detect mergeable states. When merging states with identical outgoing transitions, it will now also consider self-looping transitions has having identical destinations. + Additionally, this function now returns the number of states that + have been merged (and therefore removed from the automaton). Python: diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index d6d16da06..dbe710d5f 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -289,7 +289,7 @@ namespace spot g_.chain_edges_(); } - void twa_graph::merge_states() + unsigned twa_graph::merge_states() { if (!is_existential()) throw std::runtime_error( @@ -379,7 +379,10 @@ namespace spot else s = -1U; - defrag_states(remap, st); + unsigned merged = num_states() - st; + if (merged) + defrag_states(remap, st); + return merged; } void twa_graph::purge_unreachable_states(shift_action* f, void* action_data) diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index cd0bbe592..11a7165cf 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -579,8 +579,19 @@ namespace spot /// /// The implementation will sort the edges of the automaton to /// ease the comparison between two states. This may miss some - /// self-loop based in non-deterministic automata. - void merge_states(); + /// self-loop equivalences in non-deterministic automata. + /// + /// States whose input have been redirected as a consequence of a + /// merge are removed from the automaton. This procedure + /// therefore renumber states. + /// + /// Merging states might create duplicate transitions in the + /// automaton. For instance (1)-a->(2) and (1)-a->(3) will become + /// (1)-a->(1) and (1)-a->(1) if (1), (2) and (3) are merged into + /// (1). + /// + /// \return the number of states that have been merged and removed. + unsigned merge_states(); /// \brief Remove all dead states /// diff --git a/tests/core/tgbagraph.test b/tests/core/tgbagraph.test index 17b8bf00c..737fa9638 100755 --- a/tests/core/tgbagraph.test +++ b/tests/core/tgbagraph.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et +# Copyright (C) 2014-2018, 2020, 2021 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -291,16 +291,20 @@ State: 2 [t] 0&1 --END-- HOA: v1 -States: 1 -Start: 0 +States: 2 +Start: 1 AP: 0 acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc complete -properties: deterministic --BODY-- State: 0 [t] 0 +State: 1 +[t] 0 +[t] 0 +[t] 0 +[t] 0 --END-- EOF diff --git a/tests/core/twagraph.cc b/tests/core/twagraph.cc index f7a04d60b..39a2dc946 100644 --- a/tests/core/twagraph.cc +++ b/tests/core/twagraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2019, 2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -167,14 +167,22 @@ static void f5() auto s1 = tg->new_state(); auto s2 = tg->new_state(); auto s3 = tg->new_state(); + auto s4 = tg->new_state(); + auto s5 = tg->new_state(); - tg->set_init_state(s3); + tg->set_init_state(s5); tg->new_edge(s1, s2, bddtrue); tg->new_edge(s2, s2, bddtrue); tg->new_edge(s3, s2, bddtrue); + tg->new_edge(s4, s4, bddtrue); + tg->new_edge(s5, s1, bddtrue); + tg->new_edge(s5, s2, bddtrue); + tg->new_edge(s5, s3, bddtrue); + tg->new_edge(s5, s4, bddtrue); - tg->merge_states(); - + unsigned out = tg->merge_states(); + std::cerr << out << '\n'; + assert(out == 3); spot::print_hoa(std::cout, tg) << '\n'; }