diff --git a/NEWS b/NEWS index f91290f26..26f45d376 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 2.10.1.dev (not yet released) - Nothing yet. + Bugs fixed: + + - twa_graph::purge_dead_states() now also removes edges labeled by + bddfalse. New in spot 2.10.1 (2021-11-19) diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 6bd3f04de..1fbe76f77 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -618,7 +618,7 @@ namespace spot auto& t = g_.edge_storage(tid); todo.back().second = t.next_succ; unsigned dst = t.dst; - if (useful[dst] != 1) + if (useful[dst] != 1 && t.cond != bddfalse) { todo.emplace_back(dst, g_.state_storage(dst).succ); useful[dst] = 1; @@ -674,9 +674,12 @@ namespace spot } unsigned dst = *begin++; if (begin == end) + // that was the last destination, update the stack for + // the next edge. { - if (tid != 0) + do tid = g_.edge_storage(tid).next_succ; + while (tid && g_.edge_storage(tid).cond == bddfalse); if (tid != 0) beginend(g_.edge_storage(tid).dst, begin, end); } @@ -684,6 +687,8 @@ namespace spot { auto& ss = g_.state_storage(dst); unsigned succ = ss.succ; + while (succ && g_.edge_storage(succ).cond == bddfalse) + succ = g_.edge_storage(succ).next_succ; if (succ == 0U) continue; useful[dst] = 1; diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index bc2c23230..683fa32c8 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -611,7 +611,8 @@ namespace spot /// Dead states are all the states that cannot be part of /// an infinite run of the automaton. This includes /// states without successors, unreachable states, and states - /// that only have dead successors. + /// that only have dead successors. Transition labeled + /// by bddfalse are also removed. /// /// This function runs in linear time on non-alternating automata, /// but its current implementation can be quadratic when removing diff --git a/tests/python/alternating.py b/tests/python/alternating.py index 8092917e3..7b3a5d713 100755 --- a/tests/python/alternating.py +++ b/tests/python/alternating.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2016, 2017, 2021 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -207,3 +207,10 @@ State: 2 desalt = spot.remove_univ_otf(aut) assert(desalt.to_str('hoa') == out) + +assert aut.num_states() == 3 +assert aut.num_edges() == 3 +aut.edge_storage(3).cond = buddy.bddfalse +aut.purge_dead_states() +assert aut.num_states() == 1 +assert aut.num_edges() == 0 diff --git a/tests/python/twagraph.py b/tests/python/twagraph.py index 6e2593f4a..b8834b211 100644 --- a/tests/python/twagraph.py +++ b/tests/python/twagraph.py @@ -21,7 +21,7 @@ # This file tests various error conditions on the twa API import spot -from buddy import bddtrue +from buddy import bddtrue, bddfalse aut = spot.make_twa_graph(spot.make_bdd_dict()) @@ -113,3 +113,14 @@ aut.release_iter(it) aut.purge_dead_states() i = aut.get_init_state() assert aut.state_is_accepting(i) == False + +aut = spot.translate('FGa') +# Kill the edge between state 0 and 1 +assert aut.edge_storage(2).src == 0 +assert aut.edge_storage(2).dst == 1 +aut.edge_data(2).cond = bddfalse +assert aut.num_edges() == 3 +assert aut.num_states() == 2 +aut.purge_dead_states() +assert aut.num_edges() == 1 +assert aut.num_states() == 1