In [1]:
from IPython.display import display
import spot
spot.setup()

Test syntax errors


In [2]:
%%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] 1
State: 1
[t] 1
--END--
HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[a] 3
State: 1
[1] 0
[0&!1] 1
--END--


Writing _example.aut

In [3]:
for a in spot.automata('_example.aut'):
    display(a)


G 1 1 I->1 1->1 1 0 0 0->1 1
  File "<string>", line unknown
SyntaxError: 
_example.aut:20.2: syntax error, unexpected identifier
_example.aut:20.1-3: ignoring this invalid label
_example.aut:20.5: state number is larger than state count...
_example.aut:14.1-9: ... declared here.


In [4]:
spot.automaton('_example.aut', timeout=100)


Out[4]:
G 1 1 I->1 1->1 1 0 0 0->1 1

Error reading from pipe


In [5]:
spot.automaton('non-existing-cmd |')


---------------------------------------------------------------------------
CalledProcessError                        Traceback (most recent call last)
<ipython-input-5-6b4750207d55> in <module>()
----> 1 spot.automaton('non-existing-cmd |')

/home/adl/git/spot/python/spot/__init__.py in automaton(filename, **kwargs)
    479     See `spot.automata` for a list of supported formats."""
    480     try:
--> 481         return next(automata(filename, **kwargs))
    482     except StopIteration:
    483         raise RuntimeError("Failed to read automaton from {}".format(filename))

/home/adl/git/spot/python/spot/__init__.py in automata(timeout, ignore_abort, trust_hoa, no_sid, debug, *sources)
    464                 del proc
    465                 if ret:
--> 466                     raise subprocess.CalledProcessError(ret, filename[:-1])
    467     # deleting o explicitely now prevents Python 3.5 from
    468     # reporting the following error: "<built-in function

CalledProcessError: Command 'non-existing-cmd ' returned non-zero exit status 127.

In [6]:
spot.automaton('sleep 3; cat _example.aut |', timeout=1)


---------------------------------------------------------------------------
TimeoutExpired                            Traceback (most recent call last)
<ipython-input-6-e4289051db4c> in <module>()
----> 1 spot.automaton('sleep 3; cat _example.aut |', timeout=1)

/home/adl/git/spot/python/spot/__init__.py in automaton(filename, **kwargs)
    479     See `spot.automata` for a list of supported formats."""
    480     try:
--> 481         return next(automata(filename, **kwargs))
    482     except StopIteration:
    483         raise RuntimeError("Failed to read automaton from {}".format(filename))

/home/adl/git/spot/python/spot/__init__.py in automata(timeout, ignore_abort, trust_hoa, no_sid, debug, *sources)
    423                 else:
    424                     try:
--> 425                         out, err = proc.communicate(timeout=timeout)
    426                     except subprocess.TimeoutExpired:
    427                         # Using subprocess.check_output() with timeout

/usr/lib/python3.6/subprocess.py in communicate(self, input, timeout)
    841 
    842             try:
--> 843                 stdout, stderr = self._communicate(input, endtime, timeout)
    844             finally:
    845                 self._communication_started = True

/usr/lib/python3.6/subprocess.py in _communicate(self, input, endtime, orig_timeout)
   1513 
   1514                     ready = selector.select(timeout)
-> 1515                     self._check_timeout(endtime, orig_timeout)
   1516 
   1517                     # XXX Rewrite these to use non-blocking I/O on the file

/usr/lib/python3.6/subprocess.py in _check_timeout(self, endtime, orig_timeout)
    869             return
    870         if _time() > endtime:
--> 871             raise TimeoutExpired(self.args, orig_timeout)
    872 
    873 

TimeoutExpired: Command 'sleep 3; cat _example.aut ' timed out after 1 seconds

In [7]:
for a in spot.automata("ltl2tgba 'a U b'|", 'ltl2tgba "syntax U U error"|'):
    display(a)


G 1 1 I->1 1->1 a & !b 0 0 1->0 b 0->0 1
---------------------------------------------------------------------------
CalledProcessError                        Traceback (most recent call last)
<ipython-input-7-cf613d56390d> in <module>()
----> 1 for a in spot.automata("ltl2tgba 'a U b'|", 'ltl2tgba "syntax U U error"|'):
      2     display(a)

/home/adl/git/spot/python/spot/__init__.py in automata(timeout, ignore_abort, trust_hoa, no_sid, debug, *sources)
    464                 del proc
    465                 if ret:
--> 466                     raise subprocess.CalledProcessError(ret, filename[:-1])
    467     # deleting o explicitely now prevents Python 3.5 from
    468     # reporting the following error: "<built-in function

CalledProcessError: Command 'ltl2tgba "syntax U U error"' returned non-zero exit status 2.

Reading an empty file with spot.automaton() is an error.


In [8]:
spot.automaton('true|')


---------------------------------------------------------------------------
StopIteration                             Traceback (most recent call last)
/home/adl/git/spot/python/spot/__init__.py in automaton(filename, **kwargs)
    480     try:
--> 481         return next(automata(filename, **kwargs))
    482     except StopIteration:

StopIteration: 

During handling of the above exception, another exception occurred:

RuntimeError                              Traceback (most recent call last)
<ipython-input-8-139f3bb684aa> in <module>()
----> 1 spot.automaton('true|')

/home/adl/git/spot/python/spot/__init__.py in automaton(filename, **kwargs)
    481         return next(automata(filename, **kwargs))
    482     except StopIteration:
--> 483         raise RuntimeError("Failed to read automaton from {}".format(filename))
    484 
    485 

RuntimeError: Failed to read automaton from true|

In [9]:
!rm _example.aut