a = spot.translate('a U b')
for fmt in ('hoa', 'spin', 'dot', 'lbtt'):
    print(a.to_str(fmt))

"""
Explanation: Converting automata to strings
Use to_str() to output a string representing the automaton in different formats.
End of explanation
"""


a.save('example.aut').save('example.aut', format='lbtt', append=True)

!cat example.aut

"""
Explanation: Saving automata to files
Use save() to save the automaton into a file.
End of explanation
"""


for a in spot.automata('example.aut'):
    display(a)

"""
Explanation: Reading automata from files
Use spot.automata() to read multiple automata from a file, and spot.automaton() to read only one.
End of explanation
"""


%%file example.aut
HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[t] 0
--ABORT--   /* the previous automaton should be ignored */
HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[t] 0
State: 1
[1] 0
[0&!1] 1
--END--

for a in spot.automata('example.aut'):
    display(a)

"""
Explanation: The --ABORT-- feature of the HOA format allows discarding the automaton being read and starting over.
End of explanation
"""


for a in spot.automata("""
HOA: v1
States: 2
Start: 1
name: "Hello world"
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[t] 0
State: 1
[1] 0
[0&!1] 1
--END--
HOA: v1
States: 1
Start: 0
name: "Hello world 2"
AP: 2 "a" "b"
Acceptance: 2 Inf(0)&Inf(1)
--BODY--
State: 0 {0}
[t] 0 {1}
[0&!1] 0
--END--
"""):
    display(a)

"""
Explanation: Reading automata from strings
Instead of passing a filename, you can also pass the contents of a file.  spot.automata() and spot.automaton() look for the absence of newline to decide if this is a filename or a string containing some actual automaton text.
End of explanation
"""


for a in spot.automata('ltl2tgba -s "a U b"; ltl2tgba --lbtt "b"|', 'ltl2tgba -H "GFa" "a & GFb"|'):
    display(a)

"""
Explanation: Reading automata output from processes
If an argument of spot.automata ends with |, then it is interpreted as a shell command that outputs one automaton or more.
End of explanation
"""


spot.automaton('ltl2tgba -s6 "a U b"|')

!rm example.aut

"""
Explanation: A single automaton can be read using spot.automaton(), with the same convention.
End of explanation
"""


