GitLab

Spot knows how to highlight some specific edges in automata. For instance:

% cat >foo2.hoa <<EOF
HOA: v1.1
name: "(Gb | F!a) W c"
States: 5
Start: 1
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc !complete
properties: !deterministic stutter-invariant !terminal
spot.highlight.edges: 2 1 5 1 7 2  /* <----------- NOTE */
--BODY--
State: 0
[0] 0 {0}
State: 1
[0&1&!2] 0
[!1&!2] 1 {0}
[1&!2] 2
[2] 3
State: 2
[!1&!2] 1 {0}
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3
[t] 3 {0}
State: 4
[!1] 3
[1] 4
--END--
EOF
% autfilt foo2.hoa --dot='barf(Lato)' | dot -Tpng > foo2.png

The custom spot.highlight.edges: header is described on the HOA support page.

Highlight edges in alternating automata, this does not work as well. For instance this is ok:

% cat >foo3.hoa <<EOF
HOA: v1.1
name: "SLAA for c R (c | Gb | F!a)"
States: 4
Start: 0
AP: 3 "c" "b" "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc
properties: !complete !deterministic
spot.highlight.edges: 3 1 4 2
--BODY--
State: 0 "c R (c | Gb | F!a)"
[0] 3
[!0&!2] 0
[!0&1&2] 0&1
[!0&2] 0&2
State: 1 "Gb"
[1] 1
State: 2 "F!a"
[!2] 3
[2] 2 {0}
State: 3 "t"
[t] 3
--END--
% autfilt foo3.hoa --dot='barf(Lato)' | dot -Tpng >foo3.png
EOF

However if two edges have the same universal destination, the coloring cannot cover the entire universal edge, as the destinations are shared:

% cat >foo4.hoa <<EOF
HOA: v1.1
States: 2
Start: 0&1
AP: 3 "c" "b" "a"
Acceptance: 1 Fin(0)
spot.highlight.edges: 2 1 3 2
--BODY--
State: 0
[!0&!2] 0
[!0&1&2] 0&1
[!0&2] 0&1
State: 1
[1] 1
--END--
% autfilt foo4.hoa --dot='barf(Lato)' | dot -Tpng >foo4.png
EOF

We need an additional option to "unshare" the destinations that have different colors. Let's call this option 'y' (because it evokes the shape of the universal edges). On this example we would have this:

autfilt foo4.hoa --dot='baryf(Lato)' | dot -Tpng > foo5.png

A simple implementation, that still allows sharing destination groups for transitions that have the same color, would be to include the color number in the name the intermediate node representing destination groups.

digraph G {
  rankdir=LR
  label=<Fin(<font color="#5DA5DA">⓿</font>)>
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  I [label="", style=invis, width=0]
  I -> -1 [arrowhead=onormal]
    -1 [label=<>,shape=point]
    -1 -> 0
    -1 -> 1
  0 [label=<0>]
  0 -> 0 [label=<!a &amp; !c>]
  0 -> -1.1 [label=<a &amp; b &amp; !c>, style=bold, color="#F17CB0", arrowhead=onormal]
    -1.1 [label=<>,shape=point]
    -1.1 -> 0 [style=bold, color="#F17CB0"]
    -1.1 -> 1 [style=bold, color="#F17CB0"]
  0 -> -1.2 [label=<a &amp; !c>, style=bold, color="#FAA43A", arrowhead=onormal]
    -1.2 [label=<>,shape=point]
    -1.2 -> 0 [style=bold, color="#FAA43A"]
    -1.2 -> 1 [style=bold, color="#FAA43A"]
  1 [label=<1>]
  1 -> 1 [label=<b>]
}

Here -1 is the uncolored destination group 1, -1.1 is the same group with color 1, and -1.2 is that group with color 2.