These examples are tests for scc_info on alternating automata.



In [1]:

    
import spot
spot.setup(show_default='.bas')



In [2]:

    
spot.automaton('''
HOA: v1
States: 2
Start: 0&1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
--BODY--
State: 0
[0] 0
[!0] 1
State: 1
[1] 1 {0}
--END--
''')









    Out[2]:

universal edges are handled as if they were many distinct existencial edges from the point of view of scc_info, so the acceptance / rejection status is not always meaningful.



In [3]:

    
spot.automaton('''
HOA: v1
States: 2
Start: 0&1
AP: 2 "a" "b"
Acceptance: 1 Fin(0)
--BODY--
State: 0
[0] 0&1 {0}
State: 1
[1] 1
--END--
''')









    Out[3]:



In [5]:

    
spot.automaton('''
HOA: v1
States: 2
Start: 0&1
AP: 2 "a" "b"
Acceptance: 1 Fin(0)
--BODY--
State: 0
[0] 0 {0}
[!0] 1
State: 1
[1] 1&0
--END--
''')









    Out[5]:



In [6]:

    
spot.automaton('''
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
Acceptance: 1 Fin(0)
--BODY--
State: 0
[0] 0
[!0] 1 {0}
State: 1
[1] 1&0
--END--
''')









    Out[6]:



In [7]:

    
spot.automaton('''
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
Acceptance: 1 Fin(0)
--BODY--
State: 0
[0] 0 {0}
[!0] 1 
State: 1
[1] 1&0 {0}
--END--
''')









    Out[7]:



In [ ]: