notebook.community
Edit and run
In [1]: from IPython.display import display, HTML import spot spot.setup(size='5,4')
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.
cleanup_acceptance()
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)
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