This improves gf_guarantee_to_ba() on formulas GF(φ) where the
automaton for F(φ) as several leading transiant SCCs.  E.g.,
GF(a <-> XXXa) where we know get results that are as good as
those of delag without loosing on the cases where delag's technique
would actually produce two big automata.

* spot/twaalgos/gfguarantee.cc: Implement this.
* spot/twaalgos/gfguarantee.hh, NEWS: Document it.
* tests/core/ltl2tgba2.test, tests/core/ltl3ba.test: Add test cases.