In [1]:

    

from IPython.display import display
import spot
spot.setup()


    

In [2]:

    

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


    

    




HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal
--BODY--
State: 0 {0}
[t] 0
State: 1
[1] 0
[0&!1] 1
--END--
never {
T0_init:
  if
  :: (b) -> goto accept_all
  :: ((a) && (!(b))) -> goto T0_init
  fi;
accept_all:
  skip
}

digraph G {
  rankdir=LR
  node [shape="circle"]
  node [style="filled", fillcolor="#ffffaa"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  size="10.2,5" edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 1
  0 [label="0", peripheries=2]
  0 -> 0 [label=<1>]
  1 [label="1"]
  1 -> 0 [label=<b>]
  1 -> 1 [label=<a &amp; !b>]
}

2 1
0 1 -1
1 "b"
0 & "a" ! "b"
-1
1 0 0 -1
1 t
-1

In [3]:

    

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


    

    
Out[3]:

In [4]:

    

!cat example.aut


    

    




HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal
--BODY--
State: 0 {0}
[t] 0
State: 1
[1] 0
[0&!1] 1
--END--
2 1
0 1 -1
1 "b"
0 & "a" ! "b"
-1
1 0 0 -1
1 t
-1

In [5]:

    

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


    

In [6]:

    

%%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--


    

    




Overwriting example.aut

In [7]:

    

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


    

In [8]:

    

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)


    

In [9]:

    

%%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--


    

    




Overwriting example.aut

In [10]:

    

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


    

    


















    




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

    

spot.automaton('example.aut', timeout=100)


    

    
Out[11]:

In [12]:

    

spot.automaton('non-existing-cmd |')


    

    




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

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

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

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

In [13]:

    

spot.automaton('sleep 3; cat example.aut |', timeout=1)


    

    




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

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

/home/adl/git/spot/python/spot/__init__.py in automata(timeout, ignore_abort, trust_hoa, debug, *sources)
    415                 else:
    416                     try:
--> 417                         out, err = proc.communicate(timeout=timeout)
    418                     except subprocess.TimeoutExpired:
    419                         # Using subprocess.check_output() with timeout

/usr/lib/python3.5/subprocess.py in communicate(self, input, timeout)
   1063 
   1064             try:
-> 1065                 stdout, stderr = self._communicate(input, endtime, timeout)
   1066             finally:
   1067                 self._communication_started = True

/usr/lib/python3.5/subprocess.py in _communicate(self, input, endtime, orig_timeout)
   1698 
   1699                     ready = selector.select(timeout)
-> 1700                     self._check_timeout(endtime, orig_timeout)
   1701 
   1702                     # XXX Rewrite these to use non-blocking I/O on the file

/usr/lib/python3.5/subprocess.py in _check_timeout(self, endtime, orig_timeout)
   1089             return
   1090         if _time() > endtime:
-> 1091             raise TimeoutExpired(self.args, orig_timeout)
   1092 
   1093 

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

In [14]:

    

rm example.aut