tooltips for "..." in dot output
When the dot output of an automaton is shortened with option <N
, we display ...
to indicate that successors have been removed. It would be nice if the SVG tooltip for such node would display something informative (as opposed to some random node name like u48
).