diff --git a/NEWS b/NEWS index a9504c67ab4cb76d18bb15f667393d353672c924..c2a08072e4aa5ad838f471c30cc439cc2de18a3c 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,9 @@ New in spot 2.3.2.dev (not yet released) the output is "terminal" because dtwa_complement() failed to reset that property. + - spot::twa_graph::purge_unreachable_states() was misbehaving on + alternating automata. + New in spot 2.3.2 (2017-03-15) Tools: diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 28733cab6ebd5a8fff99ae3f7f63930029ec20bf..69f5da01d4e271860f3f54c7525097da6356504c 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -245,6 +245,8 @@ namespace spot std::vector order; order.reserve(num_states); + bool purge_unreachable_needed = false; + if (is_existential()) { std::vector> todo; // state, edge @@ -307,13 +309,16 @@ namespace spot const unsigned*& end = std::get<3>(todo.back()); if (tid == 0U && begin == end) { + unsigned src = std::get<0>(todo.back()); todo.pop_back(); + // Last transition from a state? + if ((int)src >= 0 && (todo.empty() + || src != std::get<0>(todo.back()))) + order.emplace_back(src); if (todo.empty()) break; - unsigned src = std::get<0>(todo.back()); - if ((int)src >= 0) - order.emplace_back(src); - continue; + else + continue; } unsigned dst = *begin++; if (begin == end) @@ -338,53 +343,76 @@ namespace spot } } - // Process states in topological order - for (auto s: order) + // At this point, all reachable states with successors are marked + // as useful. + for (;;) { - auto t = g_.out_iteraser(s); - bool useless = true; - while (t) + bool univ_edge_erased = false; + // Process states in topological order to mark those without + // successors as useless. + for (auto s: order) { - bool usefuldst = false; - for (unsigned d: univ_dests(t->dst)) - if (useful[d]) - { - usefuldst = true; - break; - } - // Erase any edge to a useless state. - if (!usefuldst) + auto t = g_.out_iteraser(s); + bool useless = true; + while (t) { - t.erase(); - continue; + // An edge is useful if all its + // destinations are useful. + bool usefuledge = true; + for (unsigned d: univ_dests(t->dst)) + if (!useful[d]) + { + usefuledge = false; + break; + } + // Erase any useless edge + if (!usefuledge) + { + if (is_univ_dest(t->dst)) + univ_edge_erased = true; + t.erase(); + continue; + } + // if we have a edge to a useful state, then the + // state is useful. + useless = false; + ++t; } - // if we have a edge to a useful state, then the - // state is useful. - useless = false; - ++t; + if (useless) + useful[s] = 0; } - if (useless) - useful[s] = 0; + // If we have erased any universal destination, it is possible + // that we have have created some new dead states, so we + // actually need to redo the whole thing again until there is + // no more universal edge to remove. Also we might have + // created some unreachable states, so we will simply call + // purge_unreachable_states() later to clean this. + if (!univ_edge_erased) + break; + else + purge_unreachable_needed = true; } - // Make sure at least one initial destination is useful (even if - // it has been marked as useless by the previous loop because it - // has no successor). - bool usefulinit = false; + // Is the initial state actually useful? If not, make this an + // empty automaton by resetting the graph. + bool usefulinit = true; for (unsigned d: univ_dests(init_number_)) - if (useful[d]) + if (!useful[d]) { - usefulinit = true; + usefulinit = false; break; } if (!usefulinit) - for (unsigned d: univ_dests(init_number_)) - { - useful[d] = true; - break; - } + { + g_ = graph_t(); + init_number_ = new_state(); + prop_deterministic(true); + prop_stutter_invariant(true); + prop_weak(true); + return; + } - // Now renumber each used state. + // Renumber each used state. unsigned current = 0; for (unsigned s = 0; s < num_states; ++s) if (useful[s]) @@ -394,6 +422,9 @@ namespace spot if (current == num_states) return; // No useless state. defrag_states(std::move(useful), current); + + if (purge_unreachable_needed) + purge_unreachable_states(); } void twa_graph::defrag_states(std::vector&& newst, @@ -401,14 +432,46 @@ namespace spot { if (!is_existential()) { + // Running defrag_states() on alternating automata is tricky, + // because we want to + // #1 rename the regular states + // #2 rename the states in universal destinations + // #3 get rid of the unused universal destinations + // #4 merge identical universal destinations + // + // graph::degrag_states() actually does only #1. It it could + // do #2, but that would prevent use from doing #3 and #4. It + // cannot do #3 and #4 because the graph object does not know + // what an initial state is, and our initial state might be + // universal. + // + // As a consequence this code preforms #2, #3, and #4 before + // calling graph::degrag_states() to finish with #1. We clear + // the "dests vector" of the current automaton, recreate all + // the new destination groups using a univ_dest_mapper to + // simplify an unify them, and extend newst with some new + // entries that will point the those new universal destination + // so that graph::defrag_states() does not have to deal with + // universal destination in any way. auto& g = get_graph(); auto& dests = g.dests_vector(); + // Clear the destination vector, saving the old one. std::vector old_dests; std::swap(dests, old_dests); - std::vector seen(old_dests.size(), -1U); + // dests will be updated as a side effect of declaring new + // destination groups to uniq. internal::univ_dest_mapper uniq(g); + // The newst entry associated to each of the old destination + // group. + std::vector seen(old_dests.size(), -1U); + + // Rename a state if it denotes a universal destination. This + // function has to be applied to the destination of each edge, + // as well as to the initial state. The need to work on the + // initial state is the reason it cannot be implemented in + // graph::defrag_states(). auto fixup = [&](unsigned& in_dst) { unsigned dst = in_dst; @@ -416,8 +479,9 @@ namespace spot return; dst = ~dst; unsigned& nd = seen[dst]; - if (nd == -1U) + if (nd == -1U) // An unprocessed destination group { + // store all renamed destination states in tmp std::vector tmp; auto begin = old_dests.data() + dst + 1; auto end = begin + old_dests[dst]; @@ -430,10 +494,17 @@ namespace spot } if (tmp.empty()) { + // All destinations of this group were marked for + // removal. Mark this universal transition for + // removal as well. Is this really what we expect? nd = -1U; } else { + // register this new destination group, add et two + // newst, and use the index in newst to relabel + // the state so that graph::degrag_states() will + // eventually update it to the correct value. nd = newst.size(); newst.emplace_back(uniq.new_univ_dests(tmp.begin(), tmp.end())); diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 0594ab0924071eb09b4eb78ad09049aa8c598b7c..43e1e6bc28696365bf656e4069b7a0bd5e5069ed 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -541,18 +541,26 @@ namespace spot /// states without successors, unreachable states, and states /// that only have dead successors. /// + /// This function runs in linear time on non-alternating automata, + /// but its current implementation can be quadratic when removing + /// dead states from alternating automata. (In the latter case, a + /// universal edge has to be remove when any of its destination is + /// dead, but this might cause the other destinations to become + /// dead or unreachable themselves.) + /// /// \see purge_unreachable_states void purge_dead_states(); /// \brief Remove all unreachable states. /// - /// A state is unreachable if it cannot be reached from the initial state. + /// A state is unreachable if it cannot be reached from the + /// initial state. /// /// Use this function if you have declared more states than you - /// actually need in the automaton. + /// actually need in the automaton. It runs in linear time. /// /// purge_dead_states() will remove more states than - /// purge_unreachable_states(). + /// purge_unreachable_states(), but it is more costly. /// /// \see purge_dead_states void purge_unreachable_states(); diff --git a/tests/core/alternating.test b/tests/core/alternating.test index d8c0f36051f5f030e679c3b82d4fb2d88d81f140..6b51c42a561c45f4c879f670f7cb4971f0da78c2 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -276,6 +276,27 @@ autfilt -q --intersect=ex1 ex3 cat >ex4<expect4<expect4d< out4 diff expect4 out4 run 0 autfilt --remove-dead-states ex4 > out4 -diff ex2 out4 +diff expect4d out4 cat >ex5< out5 @@ -347,6 +445,31 @@ AP: 1 "a" acc-name: co-Buchi Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc deterministic +properties: stutter-invariant weak +--BODY-- +State: 0 +--END-- +HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[!0] 1 +State: 1 +[!0] 1 +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 1 "a" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +properties: stutter-invariant weak --BODY-- State: 0 --END-- diff --git a/tests/python/twagraph.py b/tests/python/twagraph.py index b87cfdb45e8090f0621803c44d659b4ab89b96e5..d6eec94f74f64b415147390a0751cf1701954c62 100644 --- a/tests/python/twagraph.py +++ b/tests/python/twagraph.py @@ -87,4 +87,5 @@ assert aut.edge_data(1).cond == bddtrue aut.release_iter(it) aut.purge_dead_states() +i = aut.get_init_state() assert aut.state_is_accepting(i) == False