These examples are tests for scc_info on alternating automata.



In [1]:

    
from IPython.display import display
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 [4]:

    
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[4]:



In [5]:

    
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[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}
[!0] 1 
State: 1
[1] 1&0 {0}
--END--
''')









    Out[6]:

A corner case for the dot printer



In [7]:

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

a = spot.automaton('''
HOA: v1
States: 3
Start: 0&2
AP: 2 "a" "b"
Acceptance: 1 Fin(0)
spot.highlight.edges: 2 2
--BODY--
State: 0
[0] 1&2
State: 1
[1] 1&2 {0}
State: 2
[1] 1&2
--END--
''')
display(a, a.show('.basy'))