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:
- 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.ccto explore prior work (especially
decompose_strengthfunction). 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
autthe input automaton,
smthe map of all the SCCs of this automaton, and
scc_numthe only accepting SCC we want in the resulting automaton. Have a look to
sccinfo.hhto know how we can compute the SCCs of an automaton. Two functions are of interrest:
is_rejectingthat indicate whether an SCC is accepting or rejecting.
Add an option to
autfilt --decompose_scc=nwhere n is the number of the only accepting SCC we want to keep. Note that the number of accepting SCC can be obtained using
Add tests in the
write python bindings and test them