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 --decompose-strength tool. For instance ltl2tgba '(Ga -> G b) W c' | autfilt --decompose-strength=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:

1. One automaton composed of C1 and C3. In this decomposition, only C3 is accepting.
2. 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 and spot/twaalgos/strength.cc to explore prior work (especially decompose_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); with aut the input automaton, sm the map of all the SCCs of this automaton, and scc_num the only accepting SCC we want in the resulting automaton. Have a look to sccinfo.hh to know how we can compute the SCCs of an automaton. Two functions are of interrest: is_accepting and is_rejecting that indicate whether an SCC is accepting or rejecting.

• Add an option to autfilt like autfilt --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 using --stats='%[a]c'

• Add tests in the test/core directory

• write python bindings and test them