From 5384a3b89ad123ec80f137df38ec9c43bec54c35 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 18 Oct 2016 17:37:55 +0200 Subject: [PATCH] is_unambiguous: rewrite more efficiently Avoid calling scc_info::determine_unknown_acceptance on the product, as suggested in #188. * spot/twaalgos/isunamb.cc (is_unambiguous): Rewrite. * tests/core/unambig.test: Add the automaton from #188. * NEWS: Mention the improved function. * spot/twaalgos/mask.cc, spot/twaalgos/mask.hh (mask_keep_accessible_states): New function. --- NEWS | 4 +- spot/twaalgos/isunamb.cc | 105 ++++++++++++++++++++++++++++++++++++--- spot/twaalgos/mask.cc | 24 ++++++++- spot/twaalgos/mask.hh | 23 ++++++++- tests/core/unambig.test | 44 ++++++++++++++++ 5 files changed, 188 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index d5cfb18de..11d405955 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,8 @@ New in spot 2.1.2.dev (not yet released) - Nothing yet. + Library: + + * is_unambiguous() was rewritten in a more efficient way. New in spot 2.1.2 (2016-10-14) diff --git a/spot/twaalgos/isunamb.cc b/spot/twaalgos/isunamb.cc index 4a5adc2ff..8a6073160 100644 --- a/spot/twaalgos/isunamb.cc +++ b/spot/twaalgos/isunamb.cc @@ -19,25 +19,114 @@ #include #include -#include +#include +#include #include #include namespace spot { + // Conceptually, aut is unambiguous if the useful part of aut has + // the same size as the useful part of aut*aut. + // + // However calling scc_info::determine_unknown_acceptance(), which + // is needed to decide which states are actually useless, is costly. + // We do it on aut, but we avoid doing it on prod. + // + // This optimization, which requires much more code than what + // we used to have, was motivated by issue #188. bool is_unambiguous(const const_twa_graph_ptr& aut) { trival u = aut->prop_unambiguous(); if (u.is_known()) return u.is_true(); - - auto clean_a = scc_filter_states(aut); - if (clean_a->num_edges() == 0) + if (aut->num_edges() == 0) return true; - auto prod = product(clean_a, clean_a); - auto clean_p = scc_filter_states(prod); - return (clean_a->num_states() == clean_p->num_states() - && clean_a->num_edges() == clean_p->num_edges()); + + scc_info sccmap(aut); + sccmap.determine_unknown_acceptance(); + unsigned autsz = aut->num_states(); + std::vector v; + v.reserve(autsz); + bool all_useful = true; + for (unsigned n = 0; n < autsz; ++n) + { + bool useful = sccmap.is_useful_state(n); + all_useful &= useful; + v.push_back(useful); + } + + // If the input automaton comes from any /decent/ source, it is + // unlikely that it has some useless states, so do not bother too + // much optimizing this case. + if (!all_useful) + return is_unambiguous(mask_keep_accessible_states + (aut, v, aut->get_init_state_number())); + + // Reuse v to remember which states are in an accepting SCC. + for (unsigned n = 0; n < autsz; ++n) + v[n] = sccmap.is_accepting_scc(sccmap.scc_of(n)); + + auto prod = product(aut, aut); + auto sprod = + prod->get_named_prop>>("product-states"); + assert(sprod); + + // What follow is a way to compute whether an SCC is useless in + // prod, without having to call + // scc_map::determine_unknown_acceptance() on scc_map(prod), + // because prod has potentially a large acceptance condition. + // + // We know that an SCC of the product is accepting iff it is the + // combination of two accepting SCCs of the original automaton. + // + // So we can just compute the acceptance of each SCC this way, and + // derive the usefulness from that. + scc_info sccmap_prod(prod); + unsigned psc = sccmap_prod.scc_count(); + std::vector useful; + useful.reserve(psc); + for (unsigned n = 0; n < psc; ++n) + { + unsigned one_state = sccmap_prod.states_of(n).front(); + bool accepting = + v[(*sprod)[one_state].first] && v[(*sprod)[one_state].second]; + if (accepting) + { + useful[n] = true; + continue; + } + bool uf = false; + for (unsigned j: sccmap_prod.succ(n)) + if (useful[j]) + { + uf = true; + break; + } + useful[n] = uf; + } + + // Now we just have to count the number of states && edges that + // belong to the useful part of the automaton. + unsigned np = prod->num_states(); + v.resize(np); + unsigned useful_states = 0; + for (unsigned n = 0; n < np; ++n) + { + bool uf = useful[sccmap_prod.scc_of(n)]; + v[n] = uf; + useful_states += uf; + } + + if (aut->num_states() != useful_states) + return false; + + unsigned useful_edges = 0; + for (const auto& e: prod->edges()) + useful_edges += v[e.src] && v[e.dst]; + + return aut->num_edges() == useful_edges; } bool check_unambiguous(const twa_graph_ptr& aut) diff --git a/spot/twaalgos/mask.cc b/spot/twaalgos/mask.cc index c23a618a5..dcbbb19f8 100644 --- a/spot/twaalgos/mask.cc +++ b/spot/twaalgos/mask.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -67,4 +67,26 @@ namespace spot return res; } + twa_graph_ptr mask_keep_accessible_states(const const_twa_graph_ptr& in, + std::vector& to_keep, + unsigned int init) + { + if (to_keep.size() < in->num_states()) + to_keep.resize(in->num_states(), false); + + auto res = make_twa_graph(in->get_dict()); + res->copy_ap_of(in); + res->prop_copy(in, { true, true, true, false }); + res->copy_acceptance_of(in); + transform_accessible(in, res, [&](unsigned src, + bdd& cond, + acc_cond::mark_t&, + unsigned dst) + { + if (!to_keep[src] || !to_keep[dst]) + cond = bddfalse; + }, init); + return res; + } + } diff --git a/spot/twaalgos/mask.hh b/spot/twaalgos/mask.hh index 048a02152..b5a1aa1b4 100644 --- a/spot/twaalgos/mask.hh +++ b/spot/twaalgos/mask.hh @@ -140,10 +140,29 @@ namespace spot /// \brief Keep only the states as specified by \a to_keep. /// - /// Each index in the vector \a to_keep specifies wether or not to keep that - /// state. The initial state will be set to \a init. + /// Each index in the vector \a to_keep specifies wether or not to + /// keep the transition that exit this state. The initial state + /// will be set to \a init. + /// + /// Note that the number of states in the result automaton is the + /// same as in the input: only transitions have been removed. + /// + /// \see mask_keep_accessible_states SPOT_API twa_graph_ptr mask_keep_states(const const_twa_graph_ptr& in, std::vector& to_keep, unsigned int init); + + /// \brief Keep only the states specified by \a to_keep that are accessible. + /// + /// Each index in the vector \a to_keep specifies wether or not to + /// keep the transition that exit this state. The initial state + /// will be set to \a init. Only states that are accessible from \a + /// init via states in \a to_keep will be preserved. + /// + /// \see mask_keep_states + SPOT_API + twa_graph_ptr mask_keep_accessible_states(const const_twa_graph_ptr& in, + std::vector& to_keep, + unsigned int init); } diff --git a/tests/core/unambig.test b/tests/core/unambig.test index 1ae48d5ae..2ba0d3bfc 100755 --- a/tests/core/unambig.test +++ b/tests/core/unambig.test @@ -244,3 +244,47 @@ cat >expected <smaller.hoa<