In [1]:

    

import spot
spot.setup()


    

In [2]:

    

print(spot.parse_word('a; b&!a; b'))


    

    




  File "<string>", line unknown
SyntaxError: 
>>> a; b&!a; b
              ^
A twa_word must contain a cycle

In [3]:

    

print(spot.parse_word('a; b; c}'))


    

    




  File "<string>", line unknown
SyntaxError: 
>>> a; b; c}
           ^
Expected ';' delimiter: '}' stands for ending a cycle

In [4]:

    

print(spot.parse_word('a; cycle{}'))


    

    




  File "<string>", line unknown
SyntaxError: 
>>> a; cycle{}
             ^
empty input

In [5]:

    

print(spot.parse_word('a; cycle{!a}; a'))


    

    




  File "<string>", line unknown
SyntaxError: 
>>> a; cycle{!a}; a
                ^
Input should be finished after cycle

In [6]:

    

# Creating an empty word is OK...
w = spot.twa_word(spot._bdd_dict)


    

In [7]:

    

# ... as long as this word is not printed.
print(w)


    

    




---------------------------------------------------------------------------
RuntimeError                              Traceback (most recent call last)
<ipython-input-7-9968db49e707> in <module>()
      1 # ... as long as this word is not printed.
----> 2 print(w)

/home/adl/git/spot/python/spot/impl.py in __str__(self)
   4922 
   4923     def __str__(self) -> "std::string":
-> 4924         return _impl.twa_word___str__(self)
   4925 twa_word_swigregister = _impl.twa_word_swigregister
   4926 twa_word_swigregister(twa_word)

RuntimeError: a twa_word may not have an empty cycle