better highlighting of SCCs in alternating automata
The problem is where to put the intermediate node relative to the SCC cluster.
Compare:
ltl3hoa -p1 -f '(Ga <-> Gb) W c' | autfilt --dot='barf(Lato)' | dot -Tpng > out1.png
which is quite readable, to this:
ltl3hoa -p1 -f '(Ga <-> Gb) W c' | autfilt --dot='sbarf(Lato)' | dot -Tpng > out2.png
which is a mess, because the intermediate nodes of universal edges are kept out of the SCC clusters.
It seems it would be more readable if, when an universal edge has a destination that is in the same SCC as its source, then we output the intermediate node in the SCC's cluster. E.g.:
Doing this, we will have a problem similar to #207 (closed), were an intermediate node may be shared by different edges, and might need to be in several clusters (or no cluster at all). We want to duplicate them in the same way. It seems it is enough to include the name of the SCC cluster in label the intermediate node, as suggested for the colors in #207 (closed).