In [1]:
from IPython.display import display, HTML
import spot
spot.setup(size='5,4')

This shows the effect of running cleanup_acceptance() on 10 randomly generated automata.


In [2]:
txt = "<TABLE><TR><TH>before</TH><TH>after</TH>"
for a in spot.automata('randaut -A "random 4" -H -Q5 -n10 2|'):
    txt += "<TR><TD>{0}</TD><TD>{1}</TD></TR>".format(a.show('.a').data, spot.cleanup_acceptance(a).show('.a').data)
txt += ("</TABLE>")
HTML(txt)


Out[2]:
beforeafter
G Fin( ) | (Fin( ) & Fin( ) & Fin( )) 0 0 I->0 4 4 0->4 !p0 & p1 4->0 !p0 & p1 4->4 !p0 & p1 3 3 4->3 !p0 & !p1 1 1 1->0 p0 & p1 2 2 1->2 p0 & !p1 2->1 !p0 & p1 3->1 !p0 & !p1 3->3 p0 & !p1 G t [all] 0 0 I->0 4 4 0->4 !p0 & p1 4->0 !p0 & p1 4->4 !p0 & p1 3 3 4->3 !p0 & !p1 1 1 1->0 p0 & p1 2 2 1->2 p0 & !p1 2->1 !p0 & p1 3->1 !p0 & !p1 3->3 p0 & !p1
G (Fin( ) & Fin( )) | (Fin( ) & Inf( )) 0 0 I->0 1 1 0->1 !p0 & p1 1->1 !p0 & p1 4 4 1->4 !p0 & !p1 4->0 p0 & !p1 3 3 4->3 p0 & p1 2 2 2->2 p0 & p1 3->0 !p0 & !p1 3->1 !p0 & p1 3->2 p0 & p1 G (Fin( ) & Fin( )) | Inf( ) 0 0 I->0 1 1 0->1 !p0 & p1 1->1 !p0 & p1 4 4 1->4 !p0 & !p1 4->0 p0 & !p1 3 3 4->3 p0 & p1 2 2 2->2 p0 & p1 3->0 !p0 & !p1 3->1 !p0 & p1 3->2 p0 & p1
G (Inf( ) & Fin( )) | (Inf( )&Inf( )) 0 0 I->0 3 3 0->3 !p0 & p1 1 1 0->1 !p0 & p1 2 2 0->2 p0 & p1 3->3 p0 & !p1 3->2 !p0 & p1 1->3 p0 & p1 4 4 1->4 !p0 & !p1 2->2 !p0 & !p1 2->4 !p0 & p1 4->2 p0 & !p1 4->4 !p0 & !p1 G Inf( ) | (Inf( )&Inf( )) [Fin-less 3] 0 0 I->0 3 3 0->3 !p0 & p1 1 1 0->1 !p0 & p1 2 2 0->2 p0 & p1 3->3 p0 & !p1 3->2 !p0 & p1 1->3 p0 & p1 4 4 1->4 !p0 & !p1 2->2 !p0 & !p1 2->4 !p0 & p1 4->2 p0 & !p1 4->4 !p0 & !p1
G Inf( ) | Fin( ) | (Inf( )&Inf( )) 0 0 I->0 1 1 0->1 !p0 & !p1 4 4 0->4 p0 & !p1 1->0 !p0 & !p1 1->1 !p0 & p1 1->4 !p0 & p1 2 2 1->2 p0 & p1 4->2 !p0 & !p1 2->4 p0 & p1 3 3 2->3 p0 & p1 3->1 p0 & p1 3->4 !p0 & !p1 3->2 !p0 & p1 G Inf( ) | Fin( ) | (Inf( )&Inf( )) 0 0 I->0 1 1 0->1 !p0 & !p1 4 4 0->4 p0 & !p1 1->0 !p0 & !p1 1->1 !p0 & p1 1->4 !p0 & p1 2 2 1->2 p0 & p1 4->2 !p0 & !p1 2->4 p0 & p1 3 3 2->3 p0 & p1 3->1 p0 & p1 3->4 !p0 & !p1 3->2 !p0 & p1
G ((Fin( )|Fin( )) | Inf( )) & Inf( ) 0 0 I->0 0->0 !p0 & !p1 1 1 0->1 !p0 & !p1 4 4 0->4 p0 & !p1 3 3 1->3 p0 & p1 4->0 !p0 & p1 4->1 !p0 & p1 2 2 4->2 p0 & !p1 3->0 p0 & !p1 3->4 p0 & !p1 3->2 p0 & !p1 2->1 p0 & p1 2->4 !p0 & !p1 2->2 p0 & p1 G Inf( ) [Büchi] 0 0 I->0 0->0 !p0 & !p1 1 1 0->1 !p0 & !p1 4 4 0->4 p0 & !p1 3 3 1->3 p0 & p1 4->0 !p0 & p1 4->1 !p0 & p1 2 2 4->2 p0 & !p1 3->0 p0 & !p1 3->4 p0 & !p1 3->2 p0 & !p1 2->1 p0 & p1 2->4 !p0 & !p1 2->2 p0 & p1
G (Fin( ) | Inf( )) & (Inf( )&Inf( )) [gen. Streett 3] 0 0 I->0 3 3 0->3 !p0 & !p1 3->0 p0 & !p1 4 4 3->4 !p0 & p1 1 1 1->4 !p0 & p1 4->1 !p0 & p1 2 2 4->2 !p0 & p1 2->0 !p0 & !p1 2->1 !p0 & p1 G (Fin( ) | Inf( )) & (Inf( )&Inf( )) [gen. Streett 3] 0 0 I->0 3 3 0->3 !p0 & !p1 3->0 p0 & !p1 4 4 3->4 !p0 & p1 1 1 1->4 !p0 & p1 4->1 !p0 & p1 2 2 4->2 !p0 & p1 2->0 !p0 & !p1 2->1 !p0 & p1
G (Fin( ) & (Inf( )&Inf( ))) | Fin( ) [gen. Rabin 2] 0 0 I->0 0->0 p0 & p1 3 3 0->3 !p0 & !p1 3->3 p0 & !p1 1 1 3->1 !p0 & !p1 2 2 1->2 p0 & !p1 2->0 !p0 & !p1 2->2 !p0 & !p1 4 4 2->4 p0 & !p1 4->3 !p0 & !p1 4->1 p0 & p1 G (Fin( ) & (Inf( )&Inf( ))) | Fin( ) [gen. Rabin 2] 0 0 I->0 0->0 p0 & p1 3 3 0->3 !p0 & !p1 3->3 p0 & !p1 1 1 3->1 !p0 & !p1 2 2 1->2 p0 & !p1 2->0 !p0 & !p1 2->2 !p0 & !p1 4 4 2->4 p0 & !p1 4->3 !p0 & !p1 4->1 p0 & p1
G ((Fin( )|Fin( )) | Inf( )) & Inf( ) 0 0 I->0 3 3 0->3 p0 & p1 2 2 3->2 p0 & !p1 4 4 3->4 !p0 & p1 1 1 1->0 !p0 & p1 2->1 !p0 & !p1 4->3 p0 & !p1 4->1 p0 & !p1 G (Fin( )|Fin( )) & Inf( ) 0 0 I->0 3 3 0->3 p0 & p1 2 2 3->2 p0 & !p1 4 4 3->4 !p0 & p1 1 1 1->0 !p0 & p1 2->1 !p0 & !p1 4->3 p0 & !p1 4->1 p0 & !p1
G (Inf( ) | (Fin( )|Fin( ))) & Inf( ) 0 0 I->0 0->0 p0 & !p1 1 1 0->1 p0 & p1 4 4 1->4 !p0 & !p1 2 2 1->2 p0 & p1 4->0 !p0 & !p1 4->1 !p0 & p1 4->2 p0 & p1 3 3 4->3 p0 & !p1 2->0 p0 & !p1 2->3 !p0 & p1 3->0 !p0 & !p1 3->2 !p0 & !p1 G (Inf( ) | (Fin( )|Fin( ))) & Inf( ) 0 0 I->0 0->0 p0 & !p1 1 1 0->1 p0 & p1 4 4 1->4 !p0 & !p1 2 2 1->2 p0 & p1 4->0 !p0 & !p1 4->1 !p0 & p1 4->2 p0 & p1 3 3 4->3 p0 & !p1 2->0 p0 & !p1 2->3 !p0 & p1 3->0 !p0 & !p1 3->2 !p0 & !p1
G (Fin( )|Fin( )) | (Inf( ) & Fin( )) [Rabin-like 3] 0 0 I->0 1 1 0->1 p0 & p1 1->1 p0 & !p1 3 3 1->3 p0 & !p1 2 2 3->2 !p0 & !p1 2->1 !p0 & !p1 4 4 2->4 p0 & p1 4->1 p0 & !p1 G (Fin( )|Fin( )) | (Inf( ) & Fin( )) [Rabin-like 3] 0 0 I->0 1 1 0->1 p0 & p1 1->1 p0 & !p1 3 3 1->3 p0 & !p1 2 2 3->2 !p0 & !p1 2->1 !p0 & !p1 4 4 2->4 p0 & p1 4->1 p0 & !p1