Skip to content

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

out1

which is quite readable, to this:

ltl3hoa -p1 -f '(Ga <-> Gb) W c' | autfilt --dot='sbarf(Lato)' | dot -Tpng > out2.png

out2

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.:

out3

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).