diff --git a/NEWS b/NEWS index c6dd244df..cb068bce8 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,11 @@ New in spot 2.5.1.dev (not yet released) remove from the acceptance condition the parity colors that are not used in the automaton. + - twa_graph::purge_unreachable_states() now takes a function which + is called with the new numbering of states. This is useful to + update an external structure that references states of the twa + that we want to purge. + New in spot 2.5.1 (2018-02-20) Library: diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index c3d2671d7..d48261a57 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -231,7 +231,7 @@ namespace spot g_.chain_edges_(); } - void twa_graph::purge_unreachable_states() + void twa_graph::purge_unreachable_states(shift_action* f, void* action_data) { unsigned num_states = g_.num_states(); // The TODO vector serves two purposes: @@ -280,6 +280,9 @@ namespace spot if (prop_complete().is_false()) prop_complete(trival::maybe()); + if (f) + (*f)(todo, action_data); + defrag_states(std::move(todo), current); } diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 46d4d506b..9a62564a1 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -576,8 +576,16 @@ namespace spot /// purge_dead_states() will remove more states than /// purge_unreachable_states(), but it is more costly. /// + /// You can pass a function to this method, which will be invoked + /// with a vector indicating the renumbering of states. + /// newst[i] == -1U means that state i is unreachable and thus deleted. + /// Otherwise, state i is renumbered newst[i]. + /// /// \see purge_dead_states - void purge_unreachable_states(); + typedef void (*shift_action)(const std::vector& newst, + void* action_data); + void purge_unreachable_states(shift_action* f = nullptr, + void* action_data = nullptr); /// \brief Remove unused atomic propositions /// diff --git a/tests/core/tgbagraph.test b/tests/core/tgbagraph.test index 7f2d73893..3e2e5c873 100755 --- a/tests/core/tgbagraph.test +++ b/tests/core/tgbagraph.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2014-2018 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -230,6 +230,9 @@ digraph G { 1 [label="s2"] 2 [label="s3", style="bold", color="#505050"] } +0 -> deleted +1 -> deleted +2 -> 0 digraph G { rankdir=LR node [shape="circle"] diff --git a/tests/core/twagraph.cc b/tests/core/twagraph.cc index 4a34535f0..a7eae696e 100644 --- a/tests/core/twagraph.cc +++ b/tests/core/twagraph.cc @@ -105,7 +105,19 @@ static void f2() } tg->set_init_state(s3); spot::print_dot(std::cout, tg); - tg->purge_unreachable_states(); + void (*action)(const std::vector&, void*) = + [](const std::vector& newst, void*) + { + for (unsigned i = 0; i != newst.size(); ++i) + { + std::cout << i << " -> "; + if (newst[i] == -1U) + std::cout << "deleted" << std::endl; + else + std::cout << newst[i] << std::endl; + } + }; + tg->purge_unreachable_states(&action); spot::print_dot(std::cout, tg); }