In [1]:
import spot
spot.setup()
from IPython.display import display

This notebook shows you different ways in which states or transitions can be highlighted in Spot.

It should be noted that highlighting works using some special named properties: basically, two maps that are attached to the automaton, and associated state or edge numbers to color numbers. This named properties are fragile: they will be lost if the automaton is transformed into a new automaton, and they can become meaningless of the automaton is modified in place (e.g., if the transitions or states are reordered).

Nonetheless, highlighting is OK to use right before displaying or printing the automaton. The dot and hoa printer both know how to represent highlighted states and transitions.

Manual highlighting

In [2]:
a = spot.translate('a U b U c')

The # option of print_dot() can be used to display the internal number of each transition

In [3]:
a.show('.#')
Out[3]:
[Büchi] 2 2 I->2 2->2 a & !c #6 0 0 2->0 c #4 1 1 2->1 !a & b & !c #5 0->0 1 #1 1->0 c #2 1->1 b & !c #3

Using these numbers you can selectively highlight some transitions. The second argument is a color number (from a list of predefined colors).

In [4]:
a.highlight_edges([2, 4, 5], 1)
Out[4]:
[Büchi] 2 2 I->2 2->2 a & !c 0 0 2->0 c 1 1 2->1 !a & b & !c 0->0 1 1->0 c 1->1 b & !c

Note that these highlight_ functions work for edges and states, and come with both singular (changing the color of single state or edge) and plural versions.

They modify the automaton in place.

In [5]:
a.highlight_edge(6, 2).highlight_states((0, 1), 0)
Out[5]:
[Büchi] 2 2 I->2 2->2 a & !c 0 0 2->0 c 1 1 2->1 !a & b & !c 0->0 1 1->0 c 1->1 b & !c

The plural version can take a list or tuple of state numbers (as above) or of Booleans (as below). In the latter case the indices of the True values give the states to highlight.

In [6]:
a.highlight_states([False, True, True], 5)
Out[6]:
[Büchi] 2 2 I->2 2->2 a & !c 0 0 2->0 c 1 1 2->1 !a & b & !c 0->0 1 1->0 c 1->1 b & !c

Saving to HOA 1.1

When saving to HOA format, the highlighting is only output if version 1.1 of the format is selected, because the headers spot.highlight.edges and spot.highlight.states contain dots, which are disallowed in version 1. Compare these two outputs:

In [7]:
print(a.to_str('HOA', '1'))
print()
print(a.to_str('HOA', '1.1'))

HOA: v1
States: 3
Start: 2
AP: 3 "a" "b" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal very-weak
--BODY--
State: 0 {0}
[t] 0
State: 1
[2] 0
[1&!2] 1
State: 2
[2] 0
[!0&1&!2] 1
[0&!2] 2
--END--

HOA: v1.1
States: 3
Start: 2
AP: 3 "a" "b" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: deterministic stutter-invariant terminal very-weak
spot.highlight.states: 0 0 1 5 2 5
spot.highlight.edges: 2 1 4 1 5 1 6 2
--BODY--
State: 0 {0}
[t] 0
State: 1
[2] 0
[1&!2] 1
State: 2
[2] 0
[!0&1&!2] 1
[0&!2] 2
--END--

Querying highlights

Use get_highlight_state(s) or get_highlight_edge(e) to retrieve the highlighting color of some state/edge. If no highlighting is present for this state/edge, None is returned.

In [8]:
for i in range(0, a.num_states()):
    print(f"state {i}: {a.get_highlight_state(i)}")
for i in range(1, a.num_edges() + 1):
    print(f"edge {i}: {a.get_highlight_edge(i)}")

state 0: 0
state 1: 5
state 2: 5
edge 1: None
edge 2: 1
edge 3: None
edge 4: 1
edge 5: 1
edge 6: 2

Removing highlights

Use None as the color to remove some specific highlights.

In [9]:
a.highlight_state(0, None).highlight_edges([4, 2], None)
Out[9]:
[Büchi] 2 2 I->2 2->2 a & !c 0 0 2->0 c 1 1 2->1 !a & b & !c 0->0 1 1->0 c 1->1 b & !c

Or use remove_highlight_states() or remove_highlight_edges() to remove all highlights.

In [10]:
a.remove_highlight_states().remove_highlight_edges()
Out[10]:
[Büchi] 2 2 I->2 2->2 a & !c 0 0 2->0 c 1 1 2->1 !a & b & !c 0->0 1 1->0 c 1->1 b & !c

Highlighting a run

One use of this highlighting is to highlight a run in an automaton.

The following few command generate an automaton, then an accepting run on this automaton, and highlight that accepting run on the automaton. Note that a run knows the automaton from which it was generated, so calling highlight() will directly decorate that automaton.

In [11]:
b = spot.translate('X (F(Ga <-> b) & GF!b)'); b
Out[11]:
Inf( ⓿ ) [Büchi] 4 4 I->4 0 0 4->0 1 0->0 a | b 1 1 0->1 !a & !b 2 2 0->2 a & b 3 3 0->3 a & !b 1->1 b 1->1 !b ⓿ 2->2 a & b 2->2 a & !b ⓿ 3->1 !a & b 3->3 a & b
In [12]:
r = b.accepting_run(); print(r)

Prefix:
  4
  |  1
  0
  |  !a & !b
Cycle:
  1
  |  !b	{0}
In [13]:
r.highlight(5) # the parameter is a color number

The call of highlight(5) on the accepting run r modified the original automaton b:

In [14]:
b
Out[14]:
Inf( ⓿ ) [Büchi] 4 4 I->4 0 0 4->0 1 0->0 a | b 1 1 0->1 !a & !b 2 2 0->2 a & b 3 3 0->3 a & !b 1->1 b 1->1 !b ⓿ 2->2 a & b 2->2 a & !b ⓿ 3->1 !a & b 3->3 a & b

Highlighting an accepting run in an automaton with arbitrary acceptance

This is not as easy as finding accepting runs in (generalized) Büchi automata, so let's have a few example for testing.

In [15]:
def show_accrun(string):
    aut = spot.automaton(string)
    run = aut.accepting_run()
    run.highlight(5)
    display(aut)

show_accrun("""
HOA: v1 States: 10 Start: 0 AP: 2 "a" "b" Acceptance: 5 (Inf(1) | (Fin(0)
& Inf(4)) | Fin(2)) & Fin(3) properties: trans-labels explicit-labels
trans-acc --BODY-- State: 0 [0&1] 9 {3} [!0&!1] 0 {3} [0&!1] 5 {0 1} State:
1 [0&!1] 9 {4} [0&1] 8 {3} State: 2 [!0&!1] 8 {0} [!0&1] 6 {2 4} [0&1]
2 {3} [!0&1] 7 State: 3 [0&!1] 2 {0 4} [!0&!1] 3 {1 3} [!0&1] 4 {0} State: 4
[0&!1] 5 {2} [0&1] 0 [!0&1] 1 {0} State: 5 [!0&!1] 0 {3} [!0&!1] 6 {3} State: 6
[0&1] 3 {2} [!0&1] 1 [0&1] 2 {0 1 3 4} State: 7 [0&1] 1 [!0&1] 7 {0 2}
State: 8 [!0&1] 7 [!0&!1] 9 {0} State: 9 [0&1] 8 {3} [0&!1] 5 [0&!1]
1 --END--
""")
show_accrun("""
HOA: v1 States: 10 Start: 0 AP: 2 "a" "b" Acceptance: 6 Fin(5) &
((Fin(1) & (Inf(3) | Inf(4))) | Fin(0) | Fin(2)) properties: trans-labels
explicit-labels trans-acc --BODY-- State: 0 [0&1] 8 {0} [0&!1] 6 {2}
State: 1 [!0&1] 9 {0 4 5} State: 2 [!0&1] 1 State: 3 [0&!1] 3 {2}
[0&1] 4 {3 5} State: 4 [0&1] 7 {5} [0&!1] 9 {2} [!0&1] 0 {0 2} State:
5 [!0&1] 1 [!0&1] 3 {2 3} State: 6 [0&!1] 8 {1 2 5} [!0&1] 7 {3} State:
7 [0&1] 2 {0} [!0&1] 5 State: 8 [0&!1] 3 {4 5} State: 9 [!0&1] 3 {1 2}
[0&1] 1 {4} [0&!1] 5 {2} --END--""")
show_accrun("""
HOA: v1 States: 4 properties: implicit-labels trans-labels no-univ-branch
deterministic complete tool: "ltl2dstar" "0.5.4" name: "i G F a G F b"
comment: "Union{Safra[NBA=2],Safra[NBA=2]}" acc-name: Rabin 2 Acceptance:
4 (Fin(0)&Inf(1))|(Fin(2)&Inf(3)) Start: 0 AP: 2 "a" "b" --BODY-- State:
0 {0} 1 0 3 2 State: 1 {1} 1 0 3 2 State: 2 {0 3} 1 0 3 2 State: 3 {1 3}
1 0 3 2 --END--
""")
(Inf( ❶ ) | (Fin( ⓿ ) & Inf( ❹ )) | Fin( ❷ )) & Fin( ❸ ) 0 0 I->0 0->0 !a & !b ❸ 9 9 0->9 a & b ❸ 5 5 0->5 a & !b ⓿ ❶ 9->5 a & !b 1 1 9->1 a & !b 8 8 9->8 a & b ❸ 5->0 !a & !b ❸ 6 6 5->6 !a & !b ❸ 1->9 a & !b ❹ 1->8 a & b ❸ 8->9 !a & !b ⓿ 7 7 8->7 !a & b 2 2 2->8 !a & !b ⓿ 2->2 a & b ❸ 2->6 !a & b ❷ ❹ 2->7 !a & b 6->1 !a & b 6->2 a & b ⓿ ❶ ❸ ❹ 3 3 6->3 a & b ❷ 7->1 a & b 7->7 !a & b ⓿ ❷ 3->2 a & !b ⓿ ❹ 3->3 !a & !b ❶ ❸ 4 4 3->4 !a & b ⓿ 4->0 a & b 4->5 a & !b ❷ 4->1 !a & b ⓿
Fin( ❺ ) & ((Fin( ❶ ) & (Inf( ❸ ) | Inf( ❹ ))) | (Fin( ⓿ )|Fin( ❷ ))) 0 0 I->0 8 8 0->8 a & b ⓿ 6 6 0->6 a & !b ❷ 3 3 8->3 a & !b ❹ ❺ 6->8 a & !b ❶ ❷ ❺ 7 7 6->7 !a & b ❸ 1 1 9 9 1->9 !a & b ⓿ ❹ ❺ 9->1 a & b ❹ 9->3 !a & b ❶ ❷ 5 5 9->5 a & !b ❷ 2 2 2->1 !a & b 3->3 a & !b ❷ 4 4 3->4 a & b ❸ ❺ 4->0 !a & b ⓿ ❷ 4->9 a & !b ❷ 4->7 a & b ❺ 7->2 a & b ⓿ 7->5 !a & b 5->1 !a & b 5->3 !a & b ❷ ❸
i G F a G F b (Fin( ⓿ ) & Inf( ❶ )) | (Fin( ❷ ) & Inf( ❸ )) [Rabin 2] 0 0 ⓿ I->0 0->0 a & !b 1 1 ❶ 0->1 !a & !b 3 3 ❶ ❸ 0->3 !a & b 2 2 ⓿ ❸ 0->2 a & b 1->0 a & !b 1->1 !a & !b 1->3 !a & b 1->2 a & b 3->0 a & !b 3->1 !a & !b 3->3 !a & b 3->2 a & b 2->0 a & !b 2->1 !a & !b 2->3 !a & b 2->2 a & b

Highlighting from a product

Pretty often, accepting runs are found in a product but we want to display them on one of the original automata. This can be done by projecting the runs on those automata before displaying them.

In [16]:
left = spot.translate('a U b')
right = spot.translate('GFa')
display(left, right)
[Büchi] 1 1 I->1 1->1 a & !b 0 0 1->0 b 0->0 1
Inf( ⓿ ) [Büchi] 0 0 I->0 0->0 !a 0->0 a ⓿
In [17]:
prod = spot.product(left, right); prod
Out[17]:
Inf( ⓿ ) [Büchi] 0 1,0 I->0 0->0 a & !b 1 0,0 0->1 !a & b 0->1 a & b 1->1 !a 1->1 a ⓿
In [18]:
run = prod.accepting_run(); print(run)

Prefix:
  1,0
  |  !a & b
Cycle:
  0,0
  |  a	{0}
In [19]:
run.highlight(5)
# Note that by default project() needs to know on which side you project, but it cannot 
# guess it.  The left-side is assumed unless you pass True as a second argument.
run.project(left).highlight(5)
run.project(right, True).highlight(5)
In [20]:
display(prod, left, right)
Inf( ⓿ ) [Büchi] 0 1,0 I->0 0->0 a & !b 1 0,0 0->1 !a & b 0->1 a & b 1->1 !a 1->1 a ⓿
[Büchi] 1 1 I->1 1->1 a & !b 0 0 1->0 b 0->0 1
Inf( ⓿ ) [Büchi] 0 0 I->0 0->0 !a 0->0 a ⓿

The projection also works for products generated on-the-fly, but the on-the-fly product itself cannot be highlighted (it does not store states or transitions).

In [21]:
left2 = spot.translate('!b & FG a')
right2 = spot.translate('XXXb')
prod2 = spot.otf_product(left2, right2)  # Note "otf_product()"
run2 = prod2.accepting_run()
run2.project(left2).highlight(5)
run2.project(right2, True).highlight(5)
print(run2)
display(prod2, left2, right2)

Prefix:
  0 * 3
  |  a & !b
  1 * 2
  |  a	{0}
  1 * 1
  |  a	{0}
  1 * 0
  |  a & b	{0}
Cycle:
  1 * 4
  |  a	{0}
Inf( ⓿ ) [Büchi] 0 0 * 3 I->0 1 1 * 2 0->1 a & !b 2 2 * 2 0->2 !b 3 1 * 1 1->3 a ⓿ 2->3 a 4 2 * 1 2->4 1 5 1 * 0 3->5 a ⓿ 4->5 a 6 2 * 0 4->6 1 7 1 * 4 5->7 a & b ⓿ 6->7 a & b 8 2 * 4 6->8 b 7->7 a ⓿ 8->7 a 8->8 1
[Büchi] 0 0 I->0 1 1 0->1 a & !b 2 2 0->2 !b 1->1 a 2->1 a 2->2 1
t [all] 3 3 I->3 2 2 3->2 1 0 0 4 4 0->4 b 4->4 1 1 1 1->0 1 2->1 1

Highlighting nondeterminism

Sometimes its is hard to locate non-deterministic states inside a large automaton. Here are two functions that can help for that.

In [22]:
b = spot.translate('X (F(Ga <-> b) & GF!b)')
spot.highlight_nondet_states(b, 5)
spot.highlight_nondet_edges(b, 4)
b
Out[22]:
Inf( ⓿ ) [Büchi] 4 4 I->4 0 0 4->0 1 0->0 a | b 1 1 0->1 !a & !b 2 2 0->2 a & b 3 3 0->3 a & !b 1->1 b 1->1 !b ⓿ 2->2 a & b 2->2 a & !b ⓿ 3->1 !a & b 3->3 a & b

Disappearing highlights

As explained at the top of this notebook, named properties (such as highlights) are fragile, and you should not really on them being preserved across algorithms. In-place algorithm are probably the worst, because they might modify the automaton and ignore the attached named properties.

randomize() is one such in-place algorithm: it reorder states or transitions of the automaton. By doing so it renumber the states and edges, and that process would completely invalidate the highlights information. Fortunately randomize() know about highlights: it will preserve highlighted states, but it will drop all highlighted edges.

In [23]:
spot.randomize(b); b
Out[23]:
Inf( ⓿ ) [Büchi] 3 3 I->3 4 4 3->4 1 0 0 0->0 a & b 0->0 a & !b ⓿ 1 1 1->1 b 1->1 !b ⓿ 2 2 2->1 !a & b 2->2 a & b 4->0 a & b 4->1 !a & !b 4->2 a & !b 4->4 a | b

Highlighting with partial output

For simplicity, rendering of partial automata is actually implemented by copying the original automaton and marking some states as "incomplete". This also allows the same display code to work with automata generated on-the-fly. However since there is a copy, propagating the highlighting information requires extra work. Let's make sure it has been done:

In [24]:
spot.highlight_nondet_edges(b, 4)  # let's get those highlighted edges back
display(b, b.show('.<4'), b.show('.<2'))
Inf( ⓿ ) [Büchi] 3 3 I->3 4 4 3->4 1 0 0 0->0 a & b 0->0 a & !b ⓿ 1 1 1->1 b 1->1 !b ⓿ 2 2 2->1 !a & b 2->2 a & b 4->0 a & b 4->1 !a & !b 4->2 a & !b 4->4 a | b
Inf( ⓿ ) [Büchi] 0 3 I->0 1 4 0->1 1 1->1 a | b u1 ... 1->u1 2 1 1->2 !a & !b 3 2 1->3 a & !b 2->2 b 2->2 !b ⓿ 3->2 !a & b 3->3 a & b
Inf( ⓿ ) [Büchi] 0 3 I->0 1 4 0->1 1 1->1 a | b u1 ... 1->u1

Highlighting languages

For deterministic automata, the function spot.highlight_languages() can be used to highlight states that recognize the same language. This can be a great help in reading automata. States with a colored border share their language, and states with a black border all have a language different from all other states.

In [25]:
aut = spot.translate('(b W Xa) & GF(c <-> Xb) | a', 'generic', 'det')
spot.highlight_languages(aut)
aut.show('.bas')
Out[25]:
Inf( ⓿ ) [Büchi] cluster_0 cluster_1 cluster_2 cluster_3 cluster_4 0 0 I->0 1 1 0->1 !a & !b 2 2 0->2 !a & b 3 3 0->3 a 4 4 6 6 4->6 !c 7 7 4->7 c 6->4 !b ⓿ 6->6 b & !c 6->7 b & c 7->4 b ⓿ 7->6 !b & !c 7->7 !b & c 1->4 a 2->4 a 2->1 !a & !b 2->2 !a & b & !c 5 5 2->5 !a & b & c 5->4 a 5->1 !a & !b 5->2 !a & b ⓿ 3->3 1 ⓿