

In [1]:

    
import spot
from spot.seminator import seminator
from spot.jupyter import display_inline
spot.setup(show_default=".ns")

The level-skipping and jump-to-bottommost options

When running the breakpoint construction with multiple acceptance sets, we have to order these sets and after we finish a breakpoint for sets $i$, we start a breakpoint for set $i+1$. We the skip_levels option if a transition is labeled by multiple consecutive sets (say $i$, $i+1$, $i+2$) we will start the breakpoint a the next absent level ($i+3$). This trick is well-know from the degenerazation algorithms.

Looking at the second and third automata in the following example, you can see that skip_level merges the states ({1},∅,0) and ({1},∅,1), and it also reduce the larger bottom component, while creating a trivial SCC ({2},∅,1) above it. This kind of trivial SCC can be removed by the jump_to_bottommost option.

With the jump_to_bottommost option, any state of the form (X,Y,z) can be merged into another state (X,Y',z') that is in a lower SCC of the automaton (the notion of "lower" is here a total order based on a topological ordering of the SCCs). Compare the last two automata of the following example. All edges going to state ({3},∅,0) in the third automaton have been redirected to state ({3},∅,1) instead. Similarly, ({2},∅,1) is fused with ({2},∅,0), and ({1},∅,1) is fused with ({1},∅,0).



In [2]:

    
in_a = spot.translate("FG(a | XF(a & XFb))")
in_a.set_name("input")
out_a = seminator(in_a, highlight=True, pure=True)
out_a.set_name("without skip-levels")
skip_a = seminator(in_a, highlight=True, pure=True, skip_levels=True)
skip_a.set_name("with skip-levels")
rem_a = seminator(in_a, highlight=True, pure=True, skip_levels=True, jump_to_bottommost=True)
rem_a.set_name("with skip-levels + jump-to-bottommost")
display_inline(in_a, out_a, skip_a, rem_a)