In [1]:

    

import spot
spot.setup()


    

In [2]:

    

c = spot.acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); c


    

    
Out[2]:





(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))

In [3]:

    

c.to_dnf()


    

    
Out[3]:





(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))

In [4]:

    

c.to_cnf()


    

    
Out[4]:





(Inf(0) | Inf(2)) & (Fin(3) | Inf(0)) & (Fin(1) | Inf(2)) & (Fin(1)|Fin(3))

In [5]:

    

for acc in ['all', 't', 
            'Buchi', 'generalized-Buchi 3', 'generalized-Buchi 0',
            'co-Buchi', 'generalized-co-Buchi 3', 'generalized-co-Buchi 0',
            'Rabin 2', 'Rabin 0',
            'Streett 2', 'Streett 0',
            'generalized-Rabin 3 1 2 3', 'generalized-Rabin 0',
            'parity min even 6', 'parity max odd 6', 'parity max even 6', 'parity min odd 6',
            'parity min even 5', 'parity max odd 5', 'parity max even 5', 'parity min odd 5',
            'parity min even 2', 'parity max odd 2', 'parity max even 2', 'parity min odd 2',
            'parity min even 1', 'parity max odd 1', 'parity max even 1', 'parity min odd 1',
            'parity min even 0', 'parity max odd 0', 'parity max even 0', 'parity min odd 0',
            ]:
    print(acc, ': ', spot.acc_code(acc), sep='')


    

    




all: t
t: t
Buchi: Inf(0)
generalized-Buchi 3: Inf(0)&Inf(1)&Inf(2)
generalized-Buchi 0: t
co-Buchi: Fin(0)
generalized-co-Buchi 3: Fin(0)|Fin(1)|Fin(2)
generalized-co-Buchi 0: f
Rabin 2: (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
Rabin 0: f
Streett 2: (Fin(0) | Inf(1)) & (Fin(2) | Inf(3))
Streett 0: t
generalized-Rabin 3 1 2 3: (Fin(0) & Inf(1)) | (Fin(2) & (Inf(3)&Inf(4))) | (Fin(5) & (Inf(6)&Inf(7)&Inf(8)))
generalized-Rabin 0: f
parity min even 6: Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & (Inf(4) | Fin(5)))))
parity max odd 6: Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))))
parity max even 6: Fin(5) & (Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))))
parity min odd 6: Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | (Fin(4) & Inf(5)))))
parity min even 5: Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & Inf(4))))
parity max odd 5: Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0))))
parity max even 5: Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0))))
parity min odd 5: Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))
parity min even 2: Inf(0) | Fin(1)
parity max odd 2: Inf(1) | Fin(0)
parity max even 2: Fin(1) & Inf(0)
parity min odd 2: Fin(0) & Inf(1)
parity min even 1: Inf(0)
parity max odd 1: Fin(0)
parity max even 1: Inf(0)
parity min odd 1: Fin(0)
parity min even 0: t
parity max odd 0: t
parity max even 0: f
parity min odd 0: f

In [5]: