diff --git a/spot/twaalgos/mask.hh b/spot/twaalgos/mask.hh index 3ce03b700..52f0fdcc3 100644 --- a/spot/twaalgos/mask.hh +++ b/spot/twaalgos/mask.hh @@ -29,7 +29,7 @@ namespace spot /// \a cpy, creating new states at the same time. The argument \a /// trans should behave as a function with the following prototype: /// - /// void (*trans) (unsigned srcbdd& cond, acc_cond::mark_t& acc, + /// void (*trans) (unsigned src, bdd& cond, acc_cond::mark_t& acc, /// unsigned dst) /// /// It can modify either the condition or the acceptance sets of diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 8826ee92d..82ea1140c 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -21,7 +21,6 @@ #include #include #include -#include namespace spot { @@ -338,4 +337,58 @@ namespace spot } return res; } + + twa_graph_ptr + decompose_scc(scc_info& sm, unsigned scc_num) + { + unsigned n = sm.scc_count(); + + if (n <= scc_num) + throw std::invalid_argument + (std::string("decompose_scc(): requested SCC index is out of bounds")); + + std::vector want(n, false); + want[scc_num] = true; + + // mark all the SCCs that can reach scc_num as wanted + for (unsigned i = scc_num + 1; i < n; ++i) + for (unsigned succ : sm.succ(i)) + if (want[succ]) + { + want[i] = true; + break; + } + + const_twa_graph_ptr aut = sm.get_aut(); + twa_graph_ptr res = make_twa_graph(aut->get_dict()); + res->copy_ap_of(aut); + res->prop_copy(aut, { true, false, false, true, false }); + res->copy_acceptance_of(aut); + + auto um = aut->acc().unsat_mark(); + + // If aut has an unsatisfying mark, we are going to use it to remove the + // acceptance of some transitions. If it doesn't, we make res a rejecting + // Büchi automaton, and get back an accepting mark that we are going to set + // on the transitions of the SCC we selected. + auto new_mark = um.first ? um.second : res->set_buchi(); + auto fun = [sm, &want, um, new_mark, scc_num] + (unsigned src, bdd& cond, acc_cond::mark_t& acc, unsigned dst) + { + if (!want[sm.scc_of(dst)]) + { + cond = bddfalse; + return; + } + // no need to check if src is wanted, we already know dst is. + // if res is accepting, make only the upstream SCCs rejecting + // if res is rejecting, make only the requested SCC accepting + if (um.first != (sm.scc_of(src) == scc_num)) + acc = new_mark; + }; + + transform_accessible(aut, res, fun); + + return res; + } } diff --git a/spot/twaalgos/strength.hh b/spot/twaalgos/strength.hh index 550c1815e..1f5b8713f 100644 --- a/spot/twaalgos/strength.hh +++ b/spot/twaalgos/strength.hh @@ -171,4 +171,14 @@ namespace spot /// \param keep a string specifying the strengths to keep: it should SPOT_API twa_graph_ptr decompose_strength(const const_twa_graph_ptr& aut, const char* keep); + + /// \brief Extract a sub-automaton of a SCC + /// + /// This algorithm returns a subautomaton that contains the requested SCC, + /// plus any upstream SCC (but adjusted not to be accepting). + /// + /// \param sm the SCC info map of the automaton + /// \param scc_num the index in the map of the SCC to keep + SPOT_API twa_graph_ptr + decompose_scc(scc_info& sm, unsigned scc_num); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 5e04bb9c5..03a3be83f 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -332,6 +332,7 @@ TESTS_python = \ python/bddnqueen.py \ python/bugdet.py \ python/sccinfo.py \ + python/decompose_scc.py \ python/implies.py \ python/interdep.py \ python/ltl2tgba.test \ diff --git a/tests/python/decompose_scc.py b/tests/python/decompose_scc.py new file mode 100644 index 000000000..a0bae10d4 --- /dev/null +++ b/tests/python/decompose_scc.py @@ -0,0 +1,51 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 Laboratoire de Recherche et +# Développement de l'Epita +# +# 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 . + +import spot + +aut = spot.translate('(Ga -> Gb) W c') + +si = spot.scc_info(aut) + +assert (spot.decompose_scc(si, 2).to_str('hoa', '1.1') == """HOA: v1.1 +States: 3 +Start: 0 +AP: 3 "b" "a" "c" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc !complete +properties: deterministic +--BODY-- +State: 0 +[!1&!2] 0 +[1&!2] 1 +State: 1 +[!1&!2] 0 +[1&!2] 1 +[1&2] 2 +State: 2 +[1] 2 +--END--""") + +try: + spot.decompose_scc(si, 4) +except ValueError: + pass +else: + raise AssertionError