Improve decomposition
For Tacas 13 (as for STTT'16) the automaton is splitted only by 3 (terminal, weak strong). This decomposition can be obtained through the autfilt decomposestrength
tool. For instance ltl2tgba '(Ga > G b) W c'  autfilt decomposestrength=t
allows to keep only behaviors that are in the terminal Strongly Connected Components (SCC) of the automaton produced by ltl2tgba '(Ga > G b) W c'
. This decomposition is highly documented here: https://spot.lrde.epita.fr/ipynb/decompose.html
We can decompose further the input automaton, i.e., build one automaton for each accepting SCC of the input automaton.
Let us consider the attached example.hoa
For this example, we have an automaton with 4 SCCs:
 C1 which is rejecting. C1 is composed of states 0 and 1
 C2 which is rejecting. C2 is composed of state 7
 C3 which is accepting. C3 is composed of states 2, 3, and 4
 C4 which is accepting. C4 is composed of states 6 and 5.
And we have the following transitions between SCCs:
 C1 > C2
 C2 > C4
 C1 > C3
 C3 > C4
For this example, we want to build two automata:
 One automaton composed of C1 and C3. In this decomposition, only C3 is accepting.
 One automaton composed of C1, C2, C3, and C4. In this decomposition, only C4 is accepting.
Basically, in this decomposition, we want to
 choose an accepting SCC
 grab all its parents
 remove all acceptance marks from these parents
 and the return the automaton only composed of the accepting SCC and the parents
This decomposition can be achieved in three steps (at least):

Write the decomposition function. Have a look to the file
spot/twaalgos/strength.hh
andspot/twaalgos/strength.cc
to explore prior work (especiallydecompose_strength
function). The prototype of this function should be:twa_graph_ptr decompose_scc(const const_twa_graph_ptr& aut, scc_info* sm, unsigned scc_num);
withaut
the input automaton,sm
the map of all the SCCs of this automaton, andscc_num
the only accepting SCC we want in the resulting automaton. Have a look tosccinfo.hh
to know how we can compute the SCCs of an automaton. Two functions are of interrest:is_accepting
andis_rejecting
that indicate whether an SCC is accepting or rejecting. 
Add an option to
autfilt
likeautfilt decompose_scc=n
where n is the number of the only accepting SCC we want to keep. Note that the number of accepting SCC can be obtained usingstats='%[a]c'

Add tests in the
test/core
directory 
write python bindings and test them