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:
- 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 using--stats='%[a]c'
-
Add tests in the test/core
directory -
write python bindings and test them