Commit 9d7e6386 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

python: reduce automata width to prevent overflows with Jupyter

* python/spot/__init__.py (setup): Reduce the default maximal width of
automata so that Jupyter output does not add an horizontal scroll bar
for a few pixels.
* tests/python/automata-io.ipynb: Adjust.
parent 69c82115
Pipeline #21619 passed with stages
in 444 minutes and 58 seconds
......@@ -86,7 +86,7 @@ def setup(**kwargs):
import os
s = ('size="{}" edge[arrowhead=vee, arrowsize=.7]')
os.environ['SPOT_DOTEXTRA'] = s.format(kwargs.get('size', '10.2,5'))
os.environ['SPOT_DOTEXTRA'] = s.format(kwargs.get('size', '10.13,5'))
bullets = 'B' if kwargs.get('bullets', True) else ''
max_states = '<' + str(kwargs.get('max_states', 50))
......
%% Cell type:code id: tags:
``` python
from IPython.display import display
import spot
spot.setup()
```
%% Cell type:markdown id: tags:
# Converting automata to strings
%% Cell type:markdown id: tags:
Use `to_str()` to output a string representing the automaton in different formats.
%% Cell type:code id: tags:
``` python
a = spot.translate('a U b')
for fmt in ('hoa', 'spin', 'dot', 'lbtt'):
print(a.to_str(fmt))
```
%%%% Output: stream
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 "" {
rankdir=LR
label=<<br/>[Büchi]>
labelloc="t"
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]
size="10.13,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
%% Cell type:markdown id: tags:
# Saving automata to files
%% Cell type:markdown id: tags:
Use `save()` to save the automaton into a file.
%% Cell type:code id: tags:
``` python
a.save('example.aut').save('example.aut', format='lbtt', append=True)
```
%%%% Output: execute_result
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Pages: 1 --><svg width="171pt" height="125pt"viewBox="0.00 0.00 171.00 124.80" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 120.8)"><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-120.8 167,-120.8 167,4 -4,4"/><text text-anchor="start" x="58.5" y="-86.6" font-family="Lato" font-size="14.00" fill="#000000">[Büchi]</text><!-- I --><!-- 1 --><g id="node2" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="#000000" cx="56" cy="-22" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">1</text></g><!-- I&#45;&gt;1 --><g id="edge1" class="edge"><title>I&#45;&gt;1</title><path fill="none" stroke="#000000" d="M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22"/><polygon fill="#000000" stroke="#000000" points="37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22"/></g><!-- 1&#45;&gt;1 --><g id="edge4" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="#000000" d="M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433"/><polygon fill="#000000" stroke="#000000" points="62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373"/><text text-anchor="start" x="37.5" y="-61.8" font-family="Lato" font-size="14.00" fill="#000000">a &amp; !b</text></g><!-- 0 --><g id="node3" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="#000000" cx="141" cy="-22" rx="18" ry="18"/><ellipse fill="none" stroke="#000000" cx="141" cy="-22" rx="22" ry="22"/><text text-anchor="middle" x="141" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">0</text></g><!-- 1&#45;&gt;0 --><g id="edge3" class="edge"><title>1&#45;&gt;0</title><path fill="none" stroke="#000000" d="M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22"/><polygon fill="#000000" stroke="#000000" points="118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22"/><text text-anchor="start" x="92" y="-25.8" font-family="Lato" font-size="14.00" fill="#000000">b</text></g><!-- 0&#45;&gt;0 --><g id="edge2" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="#000000" d="M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451"/><polygon fill="#000000" stroke="#000000" points="149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808"/><text text-anchor="middle" x="141" y="-65.8" font-family="Lato" font-size="14.00" fill="#000000">1</text></g></g></svg>)
<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5770723f00> >
%% Cell type:code id: tags:
``` python
!cat example.aut
```
%%%% Output: stream
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
%% Cell type:markdown id: tags:
# Reading automata from files
%% Cell type:markdown id: tags:
Use `spot.automata()` to read multiple automata from a file, and `spot.automaton()` to read only one.
%% Cell type:code id: tags:
``` python
for a in spot.automata('example.aut'):
display(a)
```
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Pages: 1 --><svg width="171pt" height="125pt"viewBox="0.00 0.00 171.00 124.80" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 120.8)"><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-120.8 167,-120.8 167,4 -4,4"/><text text-anchor="start" x="58.5" y="-86.6" font-family="Lato" font-size="14.00" fill="#000000">[Büchi]</text><!-- I --><!-- 1 --><g id="node2" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="#000000" cx="56" cy="-22" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">1</text></g><!-- I&#45;&gt;1 --><g id="edge1" class="edge"><title>I&#45;&gt;1</title><path fill="none" stroke="#000000" d="M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22"/><polygon fill="#000000" stroke="#000000" points="37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22"/></g><!-- 1&#45;&gt;1 --><g id="edge4" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="#000000" d="M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433"/><polygon fill="#000000" stroke="#000000" points="62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373"/><text text-anchor="start" x="37.5" y="-61.8" font-family="Lato" font-size="14.00" fill="#000000">a &amp; !b</text></g><!-- 0 --><g id="node3" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="#000000" cx="141" cy="-22" rx="18" ry="18"/><ellipse fill="none" stroke="#000000" cx="141" cy="-22" rx="22" ry="22"/><text text-anchor="middle" x="141" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">0</text></g><!-- 1&#45;&gt;0 --><g id="edge3" class="edge"><title>1&#45;&gt;0</title><path fill="none" stroke="#000000" d="M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22"/><polygon fill="#000000" stroke="#000000" points="118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22"/><text text-anchor="start" x="92" y="-25.8" font-family="Lato" font-size="14.00" fill="#000000">b</text></g><!-- 0&#45;&gt;0 --><g id="edge2" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="#000000" d="M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451"/><polygon fill="#000000" stroke="#000000" points="149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808"/><text text-anchor="middle" x="141" y="-65.8" font-family="Lato" font-size="14.00" fill="#000000">1</text></g></g></svg>)
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Pages: 1 --><svg width="171pt" height="125pt"viewBox="0.00 0.00 171.00 124.80" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 120.8)"><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-120.8 167,-120.8 167,4 -4,4"/><text text-anchor="start" x="58.5" y="-86.6" font-family="Lato" font-size="14.00" fill="#000000">[Büchi]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="#000000" cx="56" cy="-22" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="#000000" d="M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22"/><polygon fill="#000000" stroke="#000000" points="37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22"/></g><!-- 0&#45;&gt;0 --><g id="edge3" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="#000000" d="M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433"/><polygon fill="#000000" stroke="#000000" points="62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373"/><text text-anchor="start" x="37.5" y="-61.8" font-family="Lato" font-size="14.00" fill="#000000">a &amp; !b</text></g><!-- 1 --><g id="node3" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="#000000" cx="141" cy="-22" rx="18" ry="18"/><ellipse fill="none" stroke="#000000" cx="141" cy="-22" rx="22" ry="22"/><text text-anchor="middle" x="141" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">1</text></g><!-- 0&#45;&gt;1 --><g id="edge2" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="#000000" d="M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22"/><polygon fill="#000000" stroke="#000000" points="118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22"/><text text-anchor="start" x="92" y="-25.8" font-family="Lato" font-size="14.00" fill="#000000">b</text></g><!-- 1&#45;&gt;1 --><g id="edge4" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="#000000" d="M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451"/><polygon fill="#000000" stroke="#000000" points="149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808"/><text text-anchor="middle" x="141" y="-65.8" font-family="Lato" font-size="14.00" fill="#000000">1</text></g></g></svg>)
%% Cell type:markdown id: tags:
The `--ABORT--` feature of the HOA format allows discarding the automaton being read and starting over.
%% Cell type:code id: tags:
``` python
%%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--
```
%%%% Output: stream
Overwriting example.aut
%% Cell type:code id: tags:
``` python
for a in spot.automata('example.aut'):
display(a)
```
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Pages: 1 --><svg width="171pt" height="125pt"viewBox="0.00 0.00 171.00 124.80" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 120.8)"><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-120.8 167,-120.8 167,4 -4,4"/><text text-anchor="start" x="58.5" y="-86.6" font-family="Lato" font-size="14.00" fill="#000000">[Büchi]</text><!-- I --><!-- 1 --><g id="node2" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="#000000" cx="56" cy="-22" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">1</text></g><!-- I&#45;&gt;1 --><g id="edge1" class="edge"><title>I&#45;&gt;1</title><path fill="none" stroke="#000000" d="M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22"/><polygon fill="#000000" stroke="#000000" points="37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22"/></g><!-- 1&#45;&gt;1 --><g id="edge4" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="#000000" d="M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433"/><polygon fill="#000000" stroke="#000000" points="62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373"/><text text-anchor="start" x="37.5" y="-61.8" font-family="Lato" font-size="14.00" fill="#000000">a &amp; !b</text></g><!-- 0 --><g id="node3" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="#000000" cx="141" cy="-22" rx="18" ry="18"/><ellipse fill="none" stroke="#000000" cx="141" cy="-22" rx="22" ry="22"/><text text-anchor="middle" x="141" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">0</text></g><!-- 1&#45;&gt;0 --><g id="edge3" class="edge"><title>1&#45;&gt;0</title><path fill="none" stroke="#000000" d="M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22"/><polygon fill="#000000" stroke="#000000" points="118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22"/><text text-anchor="start" x="92" y="-25.8" font-family="Lato" font-size="14.00" fill="#000000">b</text></g><!-- 0&#45;&gt;0 --><g id="edge2" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="#000000" d="M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451"/><polygon fill="#000000" stroke="#000000" points="149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808"/><text text-anchor="middle" x="141" y="-65.8" font-family="Lato" font-size="14.00" fill="#000000">1</text></g></g></svg>)
%% Cell type:markdown id: tags:
# Reading automata from strings
%% Cell type:markdown id: tags:
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.
%% Cell type:code id: tags:
``` python
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)
```
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Title: Hello world Pages: 1 --><svg width="171pt" height="125pt"viewBox="0.00 0.00 171.00 124.80" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 120.8)"><title>Hello world</title><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-120.8 167,-120.8 167,4 -4,4"/><text text-anchor="start" x="58.5" y="-86.6" font-family="Lato" font-size="14.00" fill="#000000">[Büchi]</text><!-- I --><!-- 1 --><g id="node2" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="#000000" cx="56" cy="-22" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">1</text></g><!-- I&#45;&gt;1 --><g id="edge1" class="edge"><title>I&#45;&gt;1</title><path fill="none" stroke="#000000" d="M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22"/><polygon fill="#000000" stroke="#000000" points="37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22"/></g><!-- 1&#45;&gt;1 --><g id="edge4" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="#000000" d="M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433"/><polygon fill="#000000" stroke="#000000" points="62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373"/><text text-anchor="start" x="37.5" y="-61.8" font-family="Lato" font-size="14.00" fill="#000000">a &amp; !b</text></g><!-- 0 --><g id="node3" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="#000000" cx="141" cy="-22" rx="18" ry="18"/><ellipse fill="none" stroke="#000000" cx="141" cy="-22" rx="22" ry="22"/><text text-anchor="middle" x="141" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">0</text></g><!-- 1&#45;&gt;0 --><g id="edge3" class="edge"><title>1&#45;&gt;0</title><path fill="none" stroke="#000000" d="M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22"/><polygon fill="#000000" stroke="#000000" points="118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22"/><text text-anchor="start" x="92" y="-25.8" font-family="Lato" font-size="14.00" fill="#000000">b</text></g><!-- 0&#45;&gt;0 --><g id="edge2" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="#000000" d="M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451"/><polygon fill="#000000" stroke="#000000" points="149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808"/><text text-anchor="middle" x="141" y="-65.8" font-family="Lato" font-size="14.00" fill="#000000">1</text></g></g></svg>)
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Title: Hello world 2 Pages: 1 --><svg width="118pt" height="174pt"viewBox="0.00 0.00 118.00 174.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 170)"><title>Hello world 2</title><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-170 114,-170 114,4 -4,4"/><text text-anchor="start" x="8" y="-151.8" font-family="Lato" font-size="14.00" fill="#000000">Inf(</text><text text-anchor="start" x="30" y="-151.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text><text text-anchor="start" x="46" y="-151.8" font-family="Lato" font-size="14.00" fill="#000000">)&amp;Inf(</text><text text-anchor="start" x="82" y="-151.8" font-family="Lato" font-size="14.00" fill="#ff4da0">❶</text><text text-anchor="start" x="98" y="-151.8" font-family="Lato" font-size="14.00" fill="#000000">)</text><text text-anchor="start" x="11" y="-137.8" font-family="Lato" font-size="14.00" fill="#000000">[gen. Büchi 2]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="#000000" cx="73.75" cy="-18" rx="18" ry="18"/><text text-anchor="middle" x="73.75" y="-14.3" font-family="Lato" font-size="14.00" fill="#000000">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="#000000" d="M18.8733,-18C21.928,-18 35.6948,-18 48.6741,-18"/><polygon fill="#000000" stroke="#000000" points="55.7307,-18 48.7308,-21.1501 52.2307,-18 48.7307,-18.0001 48.7307,-18.0001 48.7307,-18.0001 52.2307,-18 48.7307,-14.8501 55.7307,-18 55.7307,-18"/></g><!-- 0&#45;&gt;0 --><g id="edge2" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="#000000" d="M70.5143,-35.7817C69.9644,-45.3149 71.043,-54 73.75,-54 75.738,-54 76.8477,-49.3161 77.0792,-43.0521"/><polygon fill="#000000" stroke="#000000" points="76.9857,-35.7817 80.2256,-42.7406 77.0308,-39.2814 77.0758,-42.7812 77.0758,-42.7812 77.0758,-42.7812 77.0308,-39.2814 73.9261,-42.8217 76.9857,-35.7817 76.9857,-35.7817"/><text text-anchor="start" x="69.25" y="-71.8" font-family="Lato" font-size="14.00" fill="#000000">1</text><text text-anchor="start" x="57.75" y="-57.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text><text text-anchor="start" x="73.75" y="-57.8" font-family="Lato" font-size="14.00" fill="#ff4da0">❶</text></g><!-- 0&#45;&gt;0 --><g id="edge3" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="#000000" d="M68.6875,-35.5938C65.3125,-56.125 67,-82 73.75,-82 79.7354,-82 81.7402,-61.6553 79.7646,-42.7315"/><polygon fill="#000000" stroke="#000000" points="78.8125,-35.5938 82.8604,-42.1158 79.2753,-39.063 79.7381,-42.5323 79.7381,-42.5323 79.7381,-42.5323 79.2753,-39.063 76.6157,-42.9488 78.8125,-35.5938 78.8125,-35.5938"/><text text-anchor="start" x="55.25" y="-100.8" font-family="Lato" font-size="14.00" fill="#000000">a &amp; !b</text><text text-anchor="start" x="65.75" y="-85.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g></g></svg>)
%% Cell type:markdown id: tags:
# 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.
%% Cell type:code id: tags:
``` python
for a in spot.automata('ltl2tgba -s "a U b"; ltl2tgba --lbtt "b"|', 'ltl2tgba -H "GFa" "a & GFb"|'):
display(a)
```
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Pages: 1 --><svg width="171pt" height="125pt"viewBox="0.00 0.00 171.00 124.80" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 120.8)"><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-120.8 167,-120.8 167,4 -4,4"/><text text-anchor="start" x="58.5" y="-86.6" font-family="Lato" font-size="14.00" fill="#000000">[Büchi]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="#000000" cx="56" cy="-22" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="#000000" d="M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22"/><polygon fill="#000000" stroke="#000000" points="37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22"/></g><!-- 0&#45;&gt;0 --><g id="edge3" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="#000000" d="M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433"/><polygon fill="#000000" stroke="#000000" points="62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373"/><text text-anchor="start" x="37.5" y="-61.8" font-family="Lato" font-size="14.00" fill="#000000">a &amp; !b</text></g><!-- 1 --><g id="node3" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="#000000" cx="141" cy="-22" rx="18" ry="18"/><ellipse fill="none" stroke="#000000" cx="141" cy="-22" rx="22" ry="22"/><text text-anchor="middle" x="141" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">1</text></g><!-- 0&#45;&gt;1 --><g id="edge2" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="#000000" d="M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22"/><polygon fill="#000000" stroke="#000000" points="118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22"/><text text-anchor="start" x="92" y="-25.8" font-family="Lato" font-size="14.00" fill="#000000">b</text></g><!-- 1&#45;&gt;1 --><g id="edge4" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="#000000" d="M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451"/><polygon fill="#000000" stroke="#000000" points="149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808"/><text text-anchor="middle" x="141" y="-65.8" font-family="Lato" font-size="14.00" fill="#000000">1</text></g></g></svg>)
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Pages: 1 --><svg width="171pt" height="125pt"viewBox="0.00 0.00 171.00 124.80" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 120.8)"><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-120.8 167,-120.8 167,4 -4,4"/><text text-anchor="start" x="58.5" y="-86.6" font-family="Lato" font-size="14.00" fill="#000000">[Büchi]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="#000000" cx="56" cy="-22" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="#000000" d="M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22"/><polygon fill="#000000" stroke="#000000" points="37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22"/></g><!-- 1 --><g id="node3" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="#000000" cx="141" cy="-22" rx="18" ry="18"/><ellipse fill="none" stroke="#000000" cx="141" cy="-22" rx="22" ry="22"/><text text-anchor="middle" x="141" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">1</text></g><!-- 0&#45;&gt;1 --><g id="edge2" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="#000000" d="M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22"/><polygon fill="#000000" stroke="#000000" points="118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22"/><text text-anchor="start" x="92" y="-25.8" font-family="Lato" font-size="14.00" fill="#000000">b</text></g><!-- 1&#45;&gt;1 --><g id="edge3" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="#000000" d="M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451"/><polygon fill="#000000" stroke="#000000" points="149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808"/><text text-anchor="middle" x="141" y="-65.8" font-family="Lato" font-size="14.00" fill="#000000">1</text></g></g></svg>)
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Title: GFa Pages: 1 --><svg width="82pt" height="161pt"viewBox="0.00 0.00 82.00 161.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 157)"><title>GFa</title><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-157 78,-157 78,4 -4,4"/><text text-anchor="start" x="16" y="-138.8" font-family="Lato" font-size="14.00" fill="#000000">Inf(</text><text text-anchor="start" x="38" y="-138.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text><text text-anchor="start" x="54" y="-138.8" font-family="Lato" font-size="14.00" fill="#000000">)</text><text text-anchor="start" x="14" y="-124.8" font-family="Lato" font-size="14.00" fill="#000000">[Büchi]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="#000000" cx="56" cy="-18" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-14.3" font-family="Lato" font-size="14.00" fill="#000000">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="#000000" d="M1.1233,-18C4.178,-18 17.9448,-18 30.9241,-18"/><polygon fill="#000000" stroke="#000000" points="37.9807,-18 30.9808,-21.1501 34.4807,-18 30.9807,-18.0001 30.9807,-18.0001 30.9807,-18.0001 34.4807,-18 30.9807,-14.8501 37.9807,-18 37.9807,-18"/></g><!-- 0&#45;&gt;0 --><g id="edge2" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="#000000" d="M52.7643,-35.7817C52.2144,-45.3149 53.293,-54 56,-54 57.988,-54 59.0977,-49.3161 59.3292,-43.0521"/><polygon fill="#000000" stroke="#000000" points="59.2357,-35.7817 62.4756,-42.7406 59.2808,-39.2814 59.3258,-42.7812 59.3258,-42.7812 59.3258,-42.7812 59.2808,-39.2814 56.1761,-42.8217 59.2357,-35.7817 59.2357,-35.7817"/><text text-anchor="start" x="50.5" y="-57.8" font-family="Lato" font-size="14.00" fill="#000000">!a</text></g><!-- 0&#45;&gt;0 --><g id="edge3" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="#000000" d="M50.6841,-35.4203C47.6538,-52.791 49.4258,-72 56,-72 61.7011,-72 63.7908,-57.5545 62.2691,-42.3894"/><polygon fill="#000000" stroke="#000000" points="61.3159,-35.4203 65.3856,-41.9288 61.7902,-38.888 62.2646,-42.3557 62.2646,-42.3557 62.2646,-42.3557 61.7902,-38.888 59.1437,-42.7826 61.3159,-35.4203 61.3159,-35.4203"/><text text-anchor="start" x="52.5" y="-90.8" font-family="Lato" font-size="14.00" fill="#000000">a</text><text text-anchor="start" x="48" y="-75.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g></g></svg>)
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Title: a &amp; GFb Pages: 1 --><svg width="161pt" height="161pt"viewBox="0.00 0.00 161.00 161.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 157)"><title>a &amp; GFb</title><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-157 157,-157 157,4 -4,4"/><text text-anchor="start" x="55.5" y="-138.8" font-family="Lato" font-size="14.00" fill="#000000">Inf(</text><text text-anchor="start" x="77.5" y="-138.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text><text text-anchor="start" x="93.5" y="-138.8" font-family="Lato" font-size="14.00" fill="#000000">)</text><text text-anchor="start" x="53.5" y="-124.8" font-family="Lato" font-size="14.00" fill="#000000">[Büchi]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="#000000" cx="56" cy="-18" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-14.3" font-family="Lato" font-size="14.00" fill="#000000">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="#000000" d="M1.1233,-18C4.178,-18 17.9448,-18 30.9241,-18"/><polygon fill="#000000" stroke="#000000" points="37.9807,-18 30.9808,-21.1501 34.4807,-18 30.9807,-18.0001 30.9807,-18.0001 30.9807,-18.0001 34.4807,-18 30.9807,-14.8501 37.9807,-18 37.9807,-18"/></g><!-- 1 --><g id="node3" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="#000000" cx="135" cy="-18" rx="18" ry="18"/><text text-anchor="middle" x="135" y="-14.3" font-family="Lato" font-size="14.00" fill="#000000">1</text></g><!-- 0&#45;&gt;1 --><g id="edge2" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="#000000" d="M74.3228,-18C84.7921,-18 98.0794,-18 109.5495,-18"/><polygon fill="#000000" stroke="#000000" points="116.7766,-18 109.7767,-21.1501 113.2766,-18 109.7766,-18.0001 109.7766,-18.0001 109.7766,-18.0001 113.2766,-18 109.7766,-14.8501 116.7766,-18 116.7766,-18"/><text text-anchor="start" x="92" y="-21.8" font-family="Lato" font-size="14.00" fill="#000000">a</text></g><!-- 1&#45;&gt;1 --><g id="edge3" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="#000000" d="M131.5845,-35.7817C131.0041,-45.3149 132.1426,-54 135,-54 137.0984,-54 138.2698,-49.3161 138.5142,-43.0521"/><polygon fill="#000000" stroke="#000000" points="138.4155,-35.7817 141.6603,-42.7383 138.4631,-39.2814 138.5106,-42.7811 138.5106,-42.7811 138.5106,-42.7811 138.4631,-39.2814 135.3609,-42.8239 138.4155,-35.7817 138.4155,-35.7817"/><text text-anchor="start" x="128.5" y="-57.8" font-family="Lato" font-size="14.00" fill="#000000">!b</text></g><!-- 1&#45;&gt;1 --><g id="edge4" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="#000000" d="M129.4406,-35.1418C126.1703,-52.585 128.0234,-72 135,-72 141.05,-72 143.2471,-57.3996 141.5913,-42.146"/><polygon fill="#000000" stroke="#000000" points="140.5594,-35.1418 144.6961,-41.6079 141.0696,-38.6044 141.5798,-42.067 141.5798,-42.067 141.5798,-42.067 141.0696,-38.6044 138.4634,-42.5262 140.5594,-35.1418 140.5594,-35.1418"/><text text-anchor="start" x="130.5" y="-90.8" font-family="Lato" font-size="14.00" fill="#000000">b</text><text text-anchor="start" x="127" y="-75.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g></g></svg>)
%% Cell type:markdown id: tags:
A single automaton can be read using `spot.automaton()`, with the same convention.
%% Cell type:code id: tags:
``` python
spot.automaton('ltl2tgba -s6 "a U b"|')
```
%%%% Output: execute_result
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Pages: 1 --><svg width="171pt" height="125pt"viewBox="0.00 0.00 171.00 124.80" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 120.8)"><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-120.8 167,-120.8 167,4 -4,4"/><text text-anchor="start" x="58.5" y="-86.6" font-family="Lato" font-size="14.00" fill="#000000">[Büchi]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="#000000" cx="56" cy="-22" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="#000000" d="M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22"/><polygon fill="#000000" stroke="#000000" points="37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22"/></g><!-- 0&#45;&gt;0 --><g id="edge3" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="#000000" d="M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433"/><polygon fill="#000000" stroke="#000000" points="62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373"/><text text-anchor="start" x="37.5" y="-61.8" font-family="Lato" font-size="14.00" fill="#000000">a &amp; !b</text></g><!-- 1 --><g id="node3" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="#000000" cx="141" cy="-22" rx="18" ry="18"/><ellipse fill="none" stroke="#000000" cx="141" cy="-22" rx="22" ry="22"/><text text-anchor="middle" x="141" y="-18.3" font-family="Lato" font-size="14.00" fill="#000000">1</text></g><!-- 0&#45;&gt;1 --><g id="edge2" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="#000000" d="M74.0263,-22C84.9439,-22 99.13,-22 111.634,-22"/><polygon fill="#000000" stroke="#000000" points="118.7644,-22 111.7645,-25.1501 115.2644,-22 111.7644,-22.0001 111.7644,-22.0001 111.7644,-22.0001 115.2644,-22 111.7644,-18.8501 118.7644,-22 118.7644,-22"/><text text-anchor="start" x="92" y="-25.8" font-family="Lato" font-size="14.00" fill="#000000">b</text></g><!-- 1&#45;&gt;1 --><g id="edge4" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="#000000" d="M132.9937,-42.5808C131.8859,-52.8447 134.5547,-62 141,-62 145.834,-62 148.5437,-56.8502 149.129,-49.9451"/><polygon fill="#000000" stroke="#000000" points="149.0063,-42.5808 152.2726,-49.5273 149.0647,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.0647,-46.0803 145.9735,-49.6324 149.0063,-42.5808 149.0063,-42.5808"/><text text-anchor="middle" x="141" y="-65.8" font-family="Lato" font-size="14.00" fill="#000000">1</text></g></g></svg>)
<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f577072d060> >
%% Cell type:code id: tags:
``` python
!rm example.aut
```
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment