From 425620150a5db96ea79d6ea4362bf0c019a6b1d5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 20 May 2017 11:14:39 +0200 Subject: [PATCH] scc_info: make it possible to ignore or cut edges * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Take a filter function as optional argument. * tests/core/sccif.cc, tests/core/sccif.test: New files. * tests/Makefile.am, tests/core/.gitignore: Adjust. * NEWS: Mention the new feature. --- NEWS | 3 ++ spot/twaalgos/sccinfo.cc | 53 ++++++++++++++++++-- spot/twaalgos/sccinfo.hh | 45 +++++++++++++++-- tests/Makefile.am | 3 ++ tests/core/.gitignore | 1 + tests/core/sccif.cc | 101 +++++++++++++++++++++++++++++++++++++++ tests/core/sccif.test | 87 +++++++++++++++++++++++++++++++++ 7 files changed, 287 insertions(+), 6 deletions(-) create mode 100644 tests/core/sccif.cc create mode 100755 tests/core/sccif.test diff --git a/NEWS b/NEWS index 8a3d8754c..8ab1a2bc8 100644 --- a/NEWS +++ b/NEWS @@ -76,6 +76,9 @@ New in spot 2.3.4.dev (not yet released) - spot::scc_info has two new methods to easily iterate over the edges of an SCC: edges_of() and inner_edges_of(). + - spot::scc_info can now be passed a filter function to ignore + or cut some edges. + Python: - The 'spot.gen' package exports the functions from libspotgen. diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 1f9c81328..03600684a 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -47,8 +47,12 @@ namespace spot }; } - scc_info::scc_info(const_twa_graph_ptr aut) - : aut_(aut) + scc_info::scc_info(const_twa_graph_ptr aut, + unsigned initial_state, + edge_filter filter, + void* filter_data) + : aut_(aut), initial_state_(initial_state), + filter_(filter), filter_data_(filter_data) { unsigned n = aut->num_states(); sccof_.resize(n, -1U); @@ -74,10 +78,28 @@ namespace spot std::stack todo_; auto& gr = aut->get_graph(); + + std::deque init_states; + std::vector init_seen(n, false); + auto push_init = [&](unsigned s) + { + if (h_[s] != 0 || init_seen[s]) + return; + init_seen[s] = true; + init_states.push_back(s); + }; + // Setup depth-first search from the initial state. But we may // have a conjunction of initial state in alternating automata. - for (unsigned init: aut->univ_dests(aut->get_init_state_number())) + if (initial_state_ == -1U) + initial_state_ = aut->get_init_state_number(); + for (unsigned init: aut->univ_dests(initial_state_)) + push_init(init); + + while (!init_states.empty()) { + unsigned init = init_states.front(); + init_states.pop_front(); int spi = h_[init]; if (spi > 0) continue; @@ -133,6 +155,17 @@ namespace spot for (auto& t: aut->out(s)) for (unsigned d: aut->univ_dests(t)) { + // If edges are cut, we are not able to + // maintain proper successor information. + if (filter_) + switch (filter_(t, d, filter_data_)) + { + case edge_filter_choice::keep: + break; + case edge_filter_choice::ignore: + case edge_filter_choice::cut: + continue; + } unsigned n = sccof_[d]; assert(n != -1U); if (n == num) @@ -179,6 +212,7 @@ namespace spot // We have a successor to look at. // Fetch the values we are interested in... auto& e = gr.edge_storage(tr_succ); + unsigned dest = e.dst; if ((int) dest < 0) { @@ -203,6 +237,19 @@ namespace spot todo_.top().out_edge = e.next_succ; } + // Do we really want to look at this + if (filter_) + switch (filter_(e, dest, filter_data_)) + { + case edge_filter_choice::keep: + break; + case edge_filter_choice::ignore: + continue; + case edge_filter_choice::cut: + push_init(e.dst); + continue; + } + auto acc = e.acc; // Are we going to a new state? diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index d00023f9b..c688f582b 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -277,12 +277,45 @@ namespace spot // support that yet. typedef scc_info_node scc_node; typedef scc_info_node::scc_succs scc_succs; + /// @{ + /// \brief An edge_filter may be called on each edge to decide what + /// to do with it. + /// + /// The edge filter is called with an edge and a destination. (In + /// existential automata the destination is already given by the + /// edge, but in alternating automata, one edge may have several + /// destinations, and in this case the filter will be called for + /// each destination.) The filter should return a value from + /// edge_filter_choice. + /// + /// \c keep means to use the edge normally, as if no filter had + /// been given. \c ignore means to pretend the edge does not + /// exist (if the destination is only reachable through this edge, + /// it will not be visited). \c cut also ignores the edge, but + /// it remembers to visit the destination state (as if it were an + /// initial state) in case it is not reachable otherwise. + /// + /// Note that successors between SCCs can only be maintained for + /// edges that are kept. If some edges are ignored or cut, the + /// SCC graph that you can explore with scc_info::initial() and + /// scc_info::succ() will be restricted to the portion reachable + /// with "keep" edges. Additionally SCCs might be created when + /// edges are cut, but those will not be reachable from + /// scc_info::initial().. + enum class edge_filter_choice { keep, ignore, cut }; + typedef edge_filter_choice + (*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst, + void* filter_data); + /// @} protected: std::vector sccof_; std::vector node_; const_twa_graph_ptr aut_; + unsigned initial_state_; + edge_filter filter_; + void* filter_data_; // Update the useful_ bits. Called automatically. void determine_usefulness(); @@ -293,7 +326,13 @@ namespace spot } public: - scc_info(const_twa_graph_ptr aut); + + // Use ~0U instead of -1U to work around a bug in Swig. + // See https://github.com/swig/swig/issues/993 + scc_info(const_twa_graph_ptr aut, + unsigned initial_state = ~0U, + edge_filter filter = nullptr, + void* filter_data = nullptr); const_twa_graph_ptr get_aut() const { @@ -389,8 +428,8 @@ namespace spot /// \brief Get number of the SCC containing the initial state. unsigned initial() const { - SPOT_ASSERT(scc_count() - 1 == scc_of(aut_->get_init_state_number())); - return scc_count() - 1; + SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_)); + return scc_of(initial_state_); } const scc_succs& succ(unsigned scc) const diff --git a/tests/Makefile.am b/tests/Makefile.am index a4b6b7b39..234a8a3e3 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -88,6 +88,7 @@ check_PROGRAMS = \ core/reduceu \ core/reductaustr \ core/safra \ + core/sccif \ core/syntimpl \ core/taatgba \ core/trival \ @@ -134,6 +135,7 @@ core_reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV core_reductaustr_SOURCES = core/equalsf.cc core_reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR core_safra_SOURCES = core/safra.cc +core_sccif_SOURCES = core/sccif.cc core_syntimpl_SOURCES = core/syntimpl.cc core_tostring_SOURCES = core/tostring.cc core_trival_SOURCES = core/trival.cc @@ -245,6 +247,7 @@ TESTS_twa = \ core/lbttparse.test \ core/scc.test \ core/sccdot.test \ + core/sccif.test \ core/sccsimpl.test \ core/sepsets.test \ core/split.test \ diff --git a/tests/core/.gitignore b/tests/core/.gitignore index fcf1a1cbc..8e6b5f689 100644 --- a/tests/core/.gitignore +++ b/tests/core/.gitignore @@ -58,6 +58,7 @@ reductau reductaustr reduccmp reductgba +sccif stdout spotlbtt syntimpl diff --git a/tests/core/sccif.cc b/tests/core/sccif.cc new file mode 100644 index 000000000..4947e9da9 --- /dev/null +++ b/tests/core/sccif.cc @@ -0,0 +1,101 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + + +#include +#include +#include +#include + +static void display(spot::scc_info& si) +{ + unsigned ns = si.scc_count(); + for (unsigned n = 0; n < ns; ++n) + { + std::cout << "SCC#" << n << "\n states:"; + for (unsigned s: si.states_of(n)) + std::cout << ' ' << s; + std::cout << '\n'; + std::cout << " edges:"; + for (auto& e: si.inner_edges_of(n)) + std::cout << ' ' << e.src << "->" << e.dst; + std::cout << '\n'; + std::cout << " succs:"; + for (unsigned s: si.succ(n)) + std::cout << ' ' << s; + std::cout << '\n'; + } + std::cout << '\n'; +} + +int main() +{ + auto d = spot::make_bdd_dict(); + auto tg = make_twa_graph(d); + bdd p1 = bdd_ithvar(tg->register_ap("p1")); + bdd p2 = bdd_ithvar(tg->register_ap("p2")); + tg->set_generalized_buchi(2); + + auto s1 = tg->new_state(); + auto s2 = tg->new_state(); + auto s3 = tg->new_state(); + tg->set_init_state(s1); + tg->new_edge(s1, s1, bddfalse); + tg->new_edge(s1, s2, p1); + tg->new_edge(s1, s3, p2, {1}); + tg->new_edge(s2, s3, p1 & p2, {0}); + tg->new_edge(s3, s1, p1 | p2, {0, 1}); + tg->new_edge(s3, s2, p1 >> p2); + tg->new_edge(s3, s3, bddtrue, {0, 1}); + + spot::print_hoa(std::cout, tg) << '\n'; + + { + std::cout << "** default\n"; + spot::scc_info si(tg); + display(si); + } + { + std::cout << "** ignore edges to 2\n"; + auto filter = [](const spot::twa_graph::edge_storage_t&, + unsigned dst, void*) + { + if (dst == 2) + return spot::scc_info::edge_filter_choice::ignore; + else + return spot::scc_info::edge_filter_choice::keep; + }; + spot::scc_info si(tg, s1, filter, nullptr); + display(si); + } + { + std::cout << "** cut edges to 2\n"; + auto filter = [](const spot::twa_graph::edge_storage_t&, + unsigned dst, void* val) + { + if (dst == *static_cast(val)) + return spot::scc_info::edge_filter_choice::cut; + else + return spot::scc_info::edge_filter_choice::keep; + }; + unsigned ignore = 2; + spot::scc_info si(tg, s1, filter, &ignore); + display(si); + } +} diff --git a/tests/core/sccif.test b/tests/core/sccif.test new file mode 100755 index 000000000..2ee7f314c --- /dev/null +++ b/tests/core/sccif.test @@ -0,0 +1,87 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +# While running some benchmark, Tomáš Babiak found that Spot took too +# much time (i.e. >1h) to translate those six formulae. It turns out +# that the WDBA minimization was performed after the degeneralization +# algorithm, while this is not necessary (WDBA will produce a BA, so +# we may as well skip degeneralization). Translating these formulae +# in the test-suite ensure that they don't take too much time (the +# buildfarm will timeout if it does). + +. ./defs + +set -e + +run 0 ../sccif > stdout + +cat >expected <0 0->1 0->2 1->2 2->0 2->1 2->2 + succs: + +** ignore edges to 2 +SCC#0 + states: 1 + edges: + succs: +SCC#1 + states: 0 + edges: 0->0 + succs: 0 + +** cut edges to 2 +SCC#0 + states: 1 + edges: + succs: +SCC#1 + states: 0 + edges: 0->0 + succs: 0 +SCC#2 + states: 2 + edges: 2->2 + succs: 0 1 + +EOF + +diff expected stdout