Commit 164135d3 authored by Clément Gillard's avatar Clément Gillard

Add a decompose_scc() function

See #172.
While at it, fix typo in doxygen comment.

* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: New function.
* tests/python/decompose_scc.py, tests/Makefile.am: Test python
binding.

* spot/twaalgos/mask.hh: Fix typo.
parent 289b2383
......@@ -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:
/// <code>
/// void (*trans) (unsigned srcbdd& cond, acc_cond::mark_t& acc,
/// void (*trans) (unsigned src, bdd& cond, acc_cond::mark_t& acc,
/// unsigned dst)
/// </code>
/// It can modify either the condition or the acceptance sets of
......
......@@ -21,7 +21,6 @@
#include <spot/misc/hash.hh>
#include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/mask.hh>
#include <deque>
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<bool> 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;
}
}
......@@ -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);
}
......@@ -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 \
......
# -*- 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 <http://www.gnu.org/licenses/>.
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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment