Commit 5d143cc1 authored by Clément Gillard's avatar Clément Gillard

decompose_scc: factor autfilt into decompose_acc_scc

Put what is done by `autfilt` in a new function, `decompose_acc_scc`.

* bin/autfilt.cc: Move code from here...
* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: To here.
* tests/python/decompose_scc.py: Test python binding.
parent c0eeea2c
......@@ -1197,20 +1197,7 @@ namespace
if (opt_decompose_scc != -1)
{
spot::scc_info si(aut);
unsigned scc_num = 0;
for (; scc_num < si.scc_count(); ++scc_num)
{
if (si.is_accepting_scc(scc_num))
{
if (!opt_decompose_scc)
break;
--opt_decompose_scc;
}
}
aut = decompose_scc(si, scc_num);
aut = decompose_acc_scc(aut, opt_decompose_scc);
if (!aut)
return 0;
}
......
......@@ -391,4 +391,23 @@ namespace spot
return res;
}
twa_graph_ptr
decompose_acc_scc(const const_twa_graph_ptr& aut, int scc_index)
{
scc_info si(aut);
unsigned scc_num = 0;
for (; scc_num < si.scc_count(); ++scc_num)
{
if (si.is_accepting_scc(scc_num))
{
if (!scc_index)
break;
--scc_index;
}
}
return decompose_scc(si, scc_num);
}
}
......@@ -181,4 +181,14 @@ namespace spot
/// \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);
/// \brief Extract a sub-automaton of an accepting SCC
///
/// This algorithm returns a subautomaton that contains the `scc_index'th
/// accepting SCC, plus any upstream SCC (but adjusted not to be accepting).
///
/// \param aut the automaton to decompose
/// \param scc_index the ID of the accepting SCC to keep
SPOT_API twa_graph_ptr
decompose_acc_scc(const const_twa_graph_ptr& aut, int scc_index);
}
......@@ -49,3 +49,52 @@ except ValueError:
pass
else:
raise AssertionError
assert (spot.decompose_acc_scc(aut, 1).to_str('hoa', '1.1') == """HOA: v1.1
States: 4
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
[2] 2
State: 1
[!1&!2] 0
[1&!2] 1
[!1&2] 2
[1&2] 3
State: 2 {0}
[t] 2
State: 3
[!1] 2
[1] 3
--END--""")
assert (spot.decompose_acc_scc(aut, 2).to_str('hoa', '1.1') == """HOA: v1.1
States: 2
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc !complete
properties: deterministic
--BODY--
State: 0
[!1&!2] 0 {0}
[1&!2] 1
State: 1
[!1&!2] 0 {0}
[1&!2] 1
--END--""")
try:
spot.decompose_acc_scc(aut, 3)
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